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)simulations, 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. © Springer-Verlag 2004.
CITATION STYLE
Qin, G., & Wu, J. (2004). Branching time equivalences for interactive markov chains. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3236, 156–169. https://doi.org/10.1007/978-3-540-30233-9_12
Mendeley helps you to discover research relevant for your work.