In: Vestnik, Quartal Journal of Novosibirsk State University, Series: Mathematics, Mechanics and Informatics 6(1), Novosibirsk State University, Novosibirsk, Russia, pages 14-42. 2006. In Russian, http://www.iis.nsk.su/persons/itar/vestnik.pd.
Abstract: 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 (LDTSPNs). 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 LDTSPNs. A stochastic process algebra is proposed with formulas specifying a special subclass of LDTSPNs.
Keywords: stochastic Petri nets; discrete time; labeling; equivalences; bisimulation; modal logics; stationary behavior; stochastic process algebras.