Lumping and Reversed Processes in Cooperating Automata

Performance evaluation of computer software or hardware architectures may rely on the analysis of a complex stochastic model whose specification is usually given in terms of a high level formalism such as queueing networks, stochastic Petri nets, stochastic Automata or Markovian process algebras. Compositionality is a key-feature of many of these formalisms and allows the modeller to combine several (simple) components to form a complex architecture. However, although these formalisms allow for relative compact specifications of possibly complex models, the derivation of the interested performance indices may be very time and space consuming since the set of possible states of the model tends to grow exponentially with the number of components. In this paper we focus on models with underlying continuous time Markov chains and we show sufficient conditions under which exact lumping of the forward or the reversed process can be derived, allowing the exact computation of marginal stationary probabilities of the cooperating components. The peculiarity of our method relies on the fact that lumping is applied at component-level rather than to the CTMC of the joint process, thus reducing both the memory requirement and the computational cost of the subsequent solution of the model.