This paper presents a class of Stochastic Petri Nets with concurrent transition firings. It is assumed that transitions occur in steps and for every step each enabled transition decides probabilistically whether it wants to participate in the step or not. Among the transitions which want to participate in a step, a maximal number is chosen to perform the firing step. The observable behavior of a net is described by labels associated with transitions. For this class of nets the dynamic behavior is defined and equivalence relations are introduced. These equivalences extend the well-known trace and bisimulation ones for systems with step semantics onto Stochastic Petri Nets with concurrent transition firing. It is shown that the equivalence notions form a lattice of interrelations. We demonstrate how the equivalences can be used to compare stationary behavior of nets. In addition, we propose a stochastic process algebra that describes a subclass of the nets we introduced.

buchholz.pdf267.98 KB