Algebra of Interactive Markov Chains

Abstract

In this chapter we will develop an algebra of Interactive Markov Chains. What turns Interactive Markov Chains into an algebra? An algebra usually consists of a set of operations on a given carrier set together with equational laws that characterise these operations. A well-know algebra is the algebra of natural numbers where addition and multiplication satisfy associativity and commutativity laws.

To begin with, we show how to specify IMC in a purely syntactic way by means of a language, and this language shall be the carrier set of our algebra of Interactive Markov Chains. We will investigate strong and weak bisimilarity in this context, introducing the notion of weak congruence, a slight refinement of weak bisimilarity. Then, we tackle the issue of a sound and complete equational theory for strong bisimilarity and weak congruence. Nontrivial problems will have to be solved in order to establish an equational treatment of time-divergence and maximal progress. Indeed, our solution solves an open problem for timed process calculi in general, and we highlight that it can be adapted to solve a similar open problem for process calculi with priority.

In addition, we introduce further operators that exemplify two different directions of extensions to Interactive Markov Chains. One operator is introduced to enhance specification convenience. A second operator is introduced for more pragmatic reasons, namely to diminish the infamous state space explosion problem for specifications that exhibit symmetries.