Performance preserving equivalence for stochastic process algebra dtsdPBC

Petri box calculus (PBC) of E. Best, R. Devillers, J.G. Hall and M. Koutny is a well-known algebra of parallel processes with a Petri net semantics. Discrete time stochastic and deterministic PBC (dtsdPBC) of the author extends PBC with discrete time stochastic and deterministic delays. dtsdPBC has a step operational semantics via labeled probabilistic transition systems and a Petri net denotational semantics via dtsd-boxes, a subclass of labeled discrete time stochastic and deterministic Petri nets (LDTSDPNs). To evaluate performance in dtsdPBC, the underlying semi-Markov chains (SMCs) and (reduced) discrete time Markov chains (DTMCs and RDTMCs) of the process expressions are analyzed. Step stochastic bisimulation equivalence is used in dtsdPBC as to compare the qualitative and quantitative behaviour, as to establish consistency of the operational and denotational semantics.
We demonstrate how to apply step stochastic bisimulation equivalence of the process expressions for quotienting their transition systems, SMCs, DTMCs and RDTMCs while preserving the stationary behaviour and residence time properties. We also prove that the quotient behavioural structures (transition systems, reachability graphs and SMCs) of the process expressions and their dtsd-boxes are isomorphic. Since the equivalence guarantees identity of the functional and performance characteristics in the equivalence classes, it can be used to simplify performance analysis within dtsdPBC due to the quotient minimization of the state space.