Comparative branching-time semantics for Markov chains

Christel Baier, H. Hermanns, Joost P. Katoen, Verena Wolf

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)
52 Downloads (Pure)

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 languageUndefined
Title of host publicationConcurrency Theory (CONCUR)
EditorsRoberto Amadio, Denis Lugiez
Place of PublicationBerlin
PublisherSpringer
Pages492-507
Number of pages16
ISBN (Print)978-3-540-40753-9
DOIs
Publication statusPublished - 2003
Event14th International Conference on Concurrency Theory, CONCUR 2003 - Marseille, France
Duration: 3 Sep 20035 Sep 2003
Conference number: 14

Publication series

NameLecture Notes in Computer Science
PublisherSpringer-Verlag
NumberXI
Volume2761
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Conference on Concurrency Theory, CONCUR 2003
Abbreviated titleCONCUR
CountryFrance
CityMarseille
Period3/09/035/09/03

Keywords

  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • FMT-MC: MODEL CHECKING
  • FMT-PM: PROBABILISTIC METHODS
  • METIS-217628
  • IR-47300
  • EWI-6537

Cite this

Baier, C., Hermanns, H., Katoen, J. P., & Wolf, V. (2003). Comparative branching-time semantics for Markov chains. In R. Amadio, & D. Lugiez (Eds.), Concurrency Theory (CONCUR) (pp. 492-507). (Lecture Notes in Computer Science; Vol. 2761, No. XI). Berlin: Springer. https://doi.org/10.1007/978-3-540-45187-7_32
Baier, Christel ; Hermanns, H. ; Katoen, Joost P. ; Wolf, Verena. / Comparative branching-time semantics for Markov chains. Concurrency Theory (CONCUR). editor / Roberto Amadio ; Denis Lugiez. Berlin : Springer, 2003. pp. 492-507 (Lecture Notes in Computer Science; XI).
@inproceedings{dfe5db8d36234ceda5bf1d03ebe9f657,
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 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.",
keywords = "FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-MC: MODEL CHECKING, FMT-PM: PROBABILISTIC METHODS, METIS-217628, IR-47300, EWI-6537",
author = "Christel Baier and H. Hermanns and Katoen, {Joost P.} and Verena Wolf",
year = "2003",
doi = "10.1007/978-3-540-45187-7_32",
language = "Undefined",
isbn = "978-3-540-40753-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "XI",
pages = "492--507",
editor = "Roberto Amadio and Denis Lugiez",
booktitle = "Concurrency Theory (CONCUR)",

}

Baier, C, Hermanns, H, Katoen, JP & Wolf, V 2003, Comparative branching-time semantics for Markov chains. in R Amadio & D Lugiez (eds), Concurrency Theory (CONCUR). Lecture Notes in Computer Science, no. XI, vol. 2761, Springer, Berlin, pp. 492-507, 14th International Conference on Concurrency Theory, CONCUR 2003, Marseille, France, 3/09/03. https://doi.org/10.1007/978-3-540-45187-7_32

Comparative branching-time semantics for Markov chains. / Baier, Christel; Hermanns, H.; Katoen, Joost P.; Wolf, Verena.

Concurrency Theory (CONCUR). ed. / Roberto Amadio; Denis Lugiez. Berlin : Springer, 2003. p. 492-507 (Lecture Notes in Computer Science; Vol. 2761, No. XI).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Comparative branching-time semantics for Markov chains

AU - Baier, Christel

AU - Hermanns, H.

AU - Katoen, Joost P.

AU - Wolf, Verena

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-MC: MODEL CHECKING

KW - FMT-PM: PROBABILISTIC METHODS

KW - METIS-217628

KW - IR-47300

KW - EWI-6537

U2 - 10.1007/978-3-540-45187-7_32

DO - 10.1007/978-3-540-45187-7_32

M3 - Conference contribution

SN - 978-3-540-40753-9

T3 - Lecture Notes in Computer Science

SP - 492

EP - 507

BT - Concurrency Theory (CONCUR)

A2 - Amadio, Roberto

A2 - Lugiez, Denis

PB - Springer

CY - Berlin

ER -

Baier C, Hermanns H, Katoen JP, Wolf V. Comparative branching-time semantics for Markov chains. In Amadio R, Lugiez D, editors, Concurrency Theory (CONCUR). Berlin: Springer. 2003. p. 492-507. (Lecture Notes in Computer Science; XI). https://doi.org/10.1007/978-3-540-45187-7_32