Logics and Models for Stochastic Analysis Beyond Markov Chains

Within the last twenty years, logics and models for stochastic analysis of information systems have been widely studied in both theory and practice. The quantitative properties, such as performance and reliability, are evaluated over discrete–time and continuous–time Markov chains. This thesis lifts the stochastic analysis techniques from the class of Markov chains to the more general classes of stochastic processes having PHase–type (PH) distributions and Matrix–Exponential (ME) distributions, such that a Markov renewal process with ME kernels that cannot be formulated as a Markov process with finite or countable state space.

PH distributions are known for many explicit analytic properties, such that systems having PH distributed components can still be formulated as Markov chains. This thesis presents several results related to PH distributions. We first show how to use the explicit analytic form of discrete PH distributions as computational vehicle on measuring the performance of concurrent wireless sensor networks. Secondly, choosing stochastic process algebras as a widely accepted formalism, we study the compositionality of continuous PH distributions in order to support modelling concurrent stochastic systems having PH representations as building blocks. At last, we consider discrete–time point processes having PH distributed interarrival times with multiple marks, we propose time-lapse bisimulation, a state-based characterisation of the equivalence relation between the point processes. We clarify that time-lapse bisimulation is a new contribution to the existing bisimulation family, which captures probabilistic behaviour
over time for labelled discrete–time Markov chains.

ME distributions is a strictly larger class than PH distributions, such that many results from PH distributions also are valid for ME distributions. ME distributions have a very appealing property, called minimality property: generally a ME representation of a PH distribution will be of lower dimension than PH representations, and one can always find a ME representation with the minimal dimension. However, because of the generality of ME distributions, we have to leave the world of Markov chains. To support ME distributions with multiple exits, we introduce a multi-exits ME distribution together with a process algebra MEME to express the systems having the semantics as Markov renewal processes with ME kernels. The most appealing feature is that all the components before and after compositions are secured to have a minimal state space representation. To support quantitative verification, we also propose stochastic model checking algorithms to our problem.