On the solution of cooperating stochastic models

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) \cite{plateau:san}, Communicating Markov Processes \cite{buchholz:approximation}, Interactive Markov chains \cite{hermanns:interactive} and the labelled transition systems derived from PEPA models \cite{hillston:thesis}. 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 \cite{harrison:rcat} for the product-form detection or the Strong Equivalence relation of PEPA \cite{hillston:thesis} to aggregate states in a component-wise fashion. This thesis 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 \cite{marin:tool,marin:inap,barbierato:multi.inap}, in components-wise lumping of forward and reversed processes \cite{marin:asmta12,marin:iscis12} and in showing that those two problems are indeed related, introducing the concept of \emph{conditional product-forms} \cite{marin:rr.lumping}. \emph{Structure of the thesis}\quad This work is divided in three parts. The first one gives to the reader a general introduction to stochastic modelling, with a particular focus on Markovian models, and to the formalisms that will appear throughout the thesis. Moreover it gives some basic notions about product-form solutions and an overview of available tools for multiformalism modelling, which is needed in order to understand some of the applications that appear later in the thesis. Part 2 deals with the main contributions of the thesis. First, it introduces algorithmic product form detection and solution techniques, and a tool for designing, detecting and solving product-form stochastic models in a compositional and modular way. It then presents a new criterion for component-wise state space reduction, in a way similar to PEPA's strong equivalence. Finally, it introduces the concept of \emph{conditional product form}, and it shows the relation between this notion and the lumpability, according to our criterion, of reversed processes, thus linking the two main topics of this work. This research has both a theoretical significance and a practical impact, since all the aforementioned contributions allows for the efficient solution of stochastic models for which an analysis was previously unfeasible. Part 3 shows some applications of the aforementioned techniques to the analysis of complex models, with a particular emphasis on heterogeneous models, i.e., models whose components exhibit different behaviours and can even be expressed using different higher level formalisms. An application of product-form theory to some classes of stochastic Petri nets is also given. The conclusion recapitulates the results of the thesis and analyses the impact of the work on the performance evaluation community. Finally, a forecast on possible future developments is discussed.