Comparative branching-time semantics for Markov chains

Abstract

This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship.

@article{baierComparativeBranchingTimeSemanticsFor2005,
 author = {Christel Baier and Joost-Pieter Katoen and Holger Hermanns and Verena Wolf},
 doi = {10.1016/j.ic.2005.03.001},
 journal = {Information and Computation (Inform. Comput.)},
 month = {8},
 number = {2},
 pages = {149-214},
 publisher = {Elsevier, Amsterdam},
 title = {Comparative branching-time semantics for Markov chains},
 volume = {200},
 year = {2005}
}