Exploiting Symmetries in Stochastic Process Algebras

Stochastic Process Algebras have been introduced to enable compositional performance analysis of parallel and distributed systems. As with other high level modelling formalisms, state space explosion is a frequently observed problem, especially if the system consists of many cooperating components. However, if the components are identical replicas of each others, the state space can be reduced by means of equivalence preserving aggregation. This paper introduces symmetric parallel composition, an operator to specify sets of identical replicas cooperating in parallel. Its operational semantics is consistent with usual parallel composition whereas the state space explosion problem is drastically reduced. We illustrate this beneficial effect, and provide an interpretation of symmetric parallel composition in terms of Petri Nets.