Stochastic models are widely used in the performance evaluation community. In particular, Markov processes, and more precisely, Continuous Time Markov Chains (CTMCs), often serve as underlying stochastic processes for models written in higher-level formalisms, such as Queueing Networks, Stochastic Petri Nets and Stochastic Process Algebras.. While compositionality, i.e., the ability to express a complex model as a combination of simpler components, is a key feature of most of those formalisms, CTMCs, by themselves, don’t allow for mechanisms to express the interaction with other CTMCs. In order to mitigate this problem various lower-level formalisms have been proposed in literature, e.g., Stochastic Automata Networks (SANs), Communicating Markov Processes, Interactive Markov chains and the labelled transition systems derived from PEPA models.
However, while the compositionality of those formalism is a useful property which makes the modelling phase easier, exploiting it to get solutions more efficiently is a non-trivial task. Ideally one should be able to either detect a product-form solution and analyse the components in isolation or, if a product form cannot be detected, use other techniques to reduce the complexity of the solution, e.g., reducing the state space of either the single components or the joint process. Both tasks raised considerable interest in the literature, e.g., the RCAT theorem for the product-form detection or the Strong Equivalence relation of PEPA to aggregate states in a component-wise fashion.This talk deals with the aforementioned problem of efficiently solving complex Markovian models expressed in term of multiple components. We restrict our analysis to models in which components interact using an active-passive semantics. The main contributions rely on automatic product-forms detection, in components-wise lumping of forward and reversed processes and in showing that those two problems are indeed related, introducing the concept of conditional product-forms.