Comparative Branching-Time Semantics

Christel BaierChristel Baier, Holger HermannsHolger Hermanns, Joost-Pieter KatoenJoost-Pieter Katoen, Verena WolfVerena Wolf

DOI Link

Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Verena Wolf
Comparative Branching-Time Semantics
In Roberto M. Amadio and Denis Lugiez, eds., 14th International Conference on Concurrency Theory (CONCUR), volume 2761 of Lecture Notes in Computer Science, 482--497, 2003. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-45187-7_32.

@inproceedings{BHKW2003,
  author    = {Christel Baier and Holger Hermanns and Joost-Pieter Katoen and
               Verena Wolf},
  title     = {Comparative Branching-Time Semantics},
  editor    = {Roberto M. Amadio and Denis Lugiez},
  booktitle = {14th International Conference on Concurrency Theory (CONCUR)},
  series    = {Lecture Notes in Computer Science},
  volume    = {2761},
  publisher = {Springer},
  year      = {2003},
  pages     = {482--497},
  doi       = {10.1007/978-3-540-45187-7_32}
}