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 and CSL. Apart from presenting various existing branching-time relations in a uniform manner, our contributions are: (i) weak simulation for DTMCs is defined, (ii) weak bisimulation equivalence is shown to coincide with weak simulation equivalence, (iii) logical characterisation of weak (bi)simulations are provided, and (iv) a classification of branching-time relations is presented, elucidating the semantics of DTMCs, CTMCs and their interrelation.
Original language | English |
---|---|
Title of host publication | CONCUR 2003 - Concurrency Theory |
Subtitle of host publication | 14th International Conference, Marseille, France, September 3-5, 2003. Proceedings |
Editors | Roberto Amadio, Denis Lugiez |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 492-507 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-540-45187-7 |
ISBN (Print) | 978-3-540-40753-9 |
DOIs | |
Publication status | Published - 2003 |
Event | 14th International Conference on Concurrency Theory, CONCUR 2003 - Marseille, France Duration: 3 Sep 2003 → 5 Sep 2003 Conference number: 14 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 2761 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 14th International Conference on Concurrency Theory, CONCUR 2003 |
---|---|
Abbreviated title | CONCUR |
Country/Territory | France |
City | Marseille |
Period | 3/09/03 → 5/09/03 |
Keywords
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-MC: MODEL CHECKING
- FMT-PM: PROBABILISTIC METHODS