Comparative branching-time semantics for Markov chains
Baier, C. and Katoen, J.P. and Hermanns, H. and Wolf, V. (2004) Comparative branching-time semantics for Markov chains. [Report]
| PDF 567Kb |
| 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 characterised in terms of the temporal logics PCTL (Probabilistic Computation Tree Logic) and CSL (Continuous Stochastic Logic). 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: | Report |
| Copyright: | ©2004 CTIT |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/49190 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Repository Staff Only: item control page
Metis ID: 221297

Show download statistics for this publication
Show download statistics for this publication