In: Bulletin of the Novosibirsk Computing Center, Series Computer Science, IIS Special Issue 24, pages 129-148. 2006. http://www.iis.nsk.su/persons/itar/dtsitncc.pdf.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was constructed to specify stochastic processes within the well-developed framework of algebraic calculi. In 2001, H.S. Maci`a, V.R. Valero and D.E. de Frutos proposed a continuous time stochastic extension of finite Petri box calculus (PBC) called sPBC. The algebra sPBC has interleaving semantics due to the properties of continuous time distributions. The iteration operator was added to sPBC in 2004 by H.S. Maci`a, V.R. Valero, D.L. Cazorla and F.G. Cuartero to specify infinite processes. Since PBC has step semantics, it could be more natural to propose its concurrent stochastic enrichment based on discrete time distributions. In 2005, I.V. Tarasyuk constructed a discrete time stochastic extension dtsPBC of finite PBC. In this paper, we construct an enrichment of dtsPBC with iteration. A step operational semantics is defined in terms of labeled transition systems based on action and ina ction 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). Consistency of both semantics is demonstrated.
Keywords: stochastic Petri nets; stochastic process algebras; Petri box calculus; iteration; discrete time; transition systems; operational semantics; dts-boxes; denotational semantics.