Equivalences for stochastic Petri nets and stochastic process algebras

A new class of stochastic Petri nets (SPNs) is proposed that is a modification of discrete time SPNs (DTSPNs) by transition labeling. The class is called labeled DTSPNs (LDT- SPNs). The observable behavior of a LDTSPN is described by labeling of transitions with actions that represent elementary activities. The dynamic behavior of LDTSPNs is defined, and the corresponding discrete time Markov chain (DTMC) is constructed. Behavioural equivalences of LDTSPNs are introduced as variants of well-known trace and bisimulation relations. Interrelations of all the mentioned equivalence relations are investigated. A logical characterization of the equivalences is presented via formulas of probabilistic modal logics. It is demonstrated how the equivalences can be used to compare stationary behavior of LDT-SPNs. A stochastic process algebra is proposed with formulas specifying a special subclass of LDTSPNs.