Iteration in discrete time stochastic Petri box calculus

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 [26], a continuous time stochastic extension of finite Petri box calculus (PBC) was proposed and called sPBC. The algebra sPBC has interleaving semantics due to the properties of continuous time distributions. The iteration operator was added to sPBC in [24] 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 [28], a discrete time stochastic extension dtsPBC of finite PBC was constructed. 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 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). Consistency of both semantics is demonstrated.