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.

Abstract

Keywords

File

tarasyuk.pdf226.8 KB

Pages

129-148