Interactive Markov chains. And the quest for quantified quality (Q701689)

To give methods for the construction of high quality information processing systems is a main challenge of computer science. The quality may be interpreted on two different ways: as correctness and as performance. The first interpretation shows it formally, the second determines it on a continuous scale. In the first case only the complete solution is accepted, the second is not so rigid, but it cannot handle well system properties that are not directly related to repeatable events, e.g. absence of deadlock, reachability of system states, etc. In order to handle these problems it is necessary to combine the two approaches. The first step in this direction was the use of stochastic Petri nets, in the 1990s appeared the stochastic process algebras. The stochastic process algebra poses the question: how best to add stochastic features combining stochastic expressivity with compatibility with existing process algebra theory. The book is the author's answer to this question. Earlier one treated delays as attributes of system actions, the author uses another approach: delays are actions in their own right that silently consume exponentially distributed amounts of time and system actions are instantaneous, so the synchronization as a by-product of synchronizing actions is completely avoided. Another advantage of the decoupling of system actions and delays is that there can be more than one delay preceding an action, this extends the class of action delays to the class of phase type distributions. Based on the principles from process algebra, the book develops an algebra of Interactive Markov Chains (IMC), they are the proper extension of both non-stochastic algebras and continuous time Markov chains. To represent the basic ideas of this calculus it is convenient to use a graphical notation that resembles Petri nets. By using the notions of strong and weak bisimilarity, weak congruence there are laws allowing to transform IMC into equivalent ones. By representing each class by a single state it is possible to construct a quotient, an aggregated IMC equivalent to the original one. This fact has a great practical significance since the aggregation is bisimilarity preserving, so the hierarchical system can be reduced to a smaller one. Chapter 1 is an introduction, Chapter 2 gives an intuitive view into the basic concepts of process algebra: a calculus of interactive processes and strong and weak bisimilarity. Chapter 3 focuses on Markov chains, touches the notion of lumpability. Chapter 4 introduces IMC, Chapter 5 develops an algebra of IMC. Chapter 6 discusses the achievements of previous chapters by means of small case studies. Chapter 7 considers the challenge of compositional performance and dependability estimation. The book is an important, step in integrated modelling and analysis of functional and performance properties of information processing systems.