@article{8d4ddeccc26e43f9b2a1c8a880613ba2,
title = "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 branchingtime 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.",
keywords = "2024 OA procedure",
author = "Christel Baier and Joost-Pieter Katoen and Holger Hermanns and Verena Wolf",
year = "2005",
doi = "10.1016/j.ic.2005.03.001",
language = "English",
volume = "200",
pages = "149--214",
journal = "Information and computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "2",
}