Comparative branching-time semantics for Markov chains

Baier, Christel and Katoen, Joost-Pieter and Hermanns, Holger and Wolf, Verena (2005) Comparative branching-time semantics for Markov chains. Information and Computation, 200 (2). pp. 149-214. ISSN 0890-5401

PDF
Restricted to UT campus only: Request a copy
1462Kb

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.
Item Type:	Article
Copyright:	© 2005 Elsevier
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/55483
Official URL:	http://dx.doi.org/10.1016/j.ic.2005.03.001
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page