Interactive Markov Chains

Abstract

This chapter introduces the central formalism of this book, Interactive Markov Chains1 (IMC). It arises as an integration of interactive processes and continuous-time Markov chains. There are different ways to combine both formalisms, and some of them have appeared in the literature. We therefore begin with a detailed discussion of the different integration possibilities and argue why we take which decision. As a result IMC combine the different ingredients as orthogonal to each other as possible. We proceed by defining composition operators for IMC. Wethen focus our attention on the discussion of strong and weak bisimilarity, incorporating the notion of maximal progress into the definitions. In order to efficiently compute these relations we develop algorithms that are more involved than the ones presented in earlier chapters. Anyhow, we prove that their computational complexity is not increased. A small example of using IMC to compositionally specify and aggregate the leaky bucket principle concludes this chapter.