Comparative branching-time semantics for Markov chains

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

doi:10.1007/978-3-540-45187-7_32

Comparative branching-time semantics for Markov chains

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

12 Citations (Scopus)

72 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 language	Undefined
Title of host publication	Concurrency Theory (CONCUR)
Editors	Roberto Amadio, Denis Lugiez
Place of Publication	Berlin
Publisher	Springer
Pages	492-507
Number of pages	16
ISBN (Print)	978-3-540-40753-9
DOIs	https://doi.org/10.1007/978-3-540-45187-7_32
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-Verlag
Number	XI
Volume	2761
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Conference on Concurrency Theory, CONCUR 2003
Abbreviated title	CONCUR
Country	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
METIS-217628
IR-47300
EWI-6537

Access to Document

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

404_BHKW03
open
baier03comparative
open

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

@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 proceeding › Conference contribution › Academic › peer-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 -