In: 05, Carl von Ossietzky Universitaet Oldenburg, Oldenburg, Germany: Berichte aus dem Department fuer Informatik 3, pages 1-25. November 2005. http://www.iis.nsk.su/persons/itar/dtspbcib.pdf.
Abstract: Last decade, a number of stochastic enrichments of process algebras was constructed to facilitate the specification of stochastic processes based on the the well-developed framework of algebraic calculi. In 2001, H.S. Macia, V.R. Valero and D.E. de Frutos proposed a continuous time stochastic extension of the finite subset of Petri Box Calculus (PBC) constructed by E. Best, R. Devillers and J.G. Hall. The resulting algebra called sPBC has an interleaving semantics due to the properties of continuous time distributions. At the same time, PBC has a step semantics, and it could be natural to propose its concurrent stochastic enrichment. We construct a discrete time stochastic extension dtsPBC of finite PBC. A step operational semantics is defined in terms of labeled transition systems based on action and inaction rules. A denotational semantics is defined in terms of a subclass of labeled discrete time stochastic Petri nets (LDTSPNs) called discrete time stochastic Petri boxes (dts-boxes). A consistency of both the semantics is demonstrated. In addition, we define a variety of probabilistic equivalences that allow one to identify stochastic processes with similar behaviour that are differentiated by too strict notion of the semantic equivalence. The interrelations of all the introduced equivalences are investigated. Some of the relations could be later considered as candidates for the role of congruence.
Keywords: Stochastic Petri nets; stochastic process algebras; Petri box calculus; discrete time; transition.