Branching Time Equivalences for Interactive Markov Chains

摘要

Interactive Markov chains (IMCs) are powerful models of concurrent systems, and branching time equivalences are useful to compare the behaviour of concurrent systems. In this paper we define various branching time relations on IMCs, including strong and weak (bi)simula-tions, and investigate connections among these relations. These relations are defined as an orthogonal extensions of classical labelled transition systems and pure stochastic settings. The logical characterizations of them are also studied by using an action-based logic aCSL. We show that for IMCs, bisimulation equivalence coincides with aCSL-equivalence, and simulation preorder weakly preserves aCSL safety and liveness formulae.