Comparative branching-time semantics for Markov chains

Christel Baier; Holger Hermanns; Joost-Pieter Katoen; Verena Wolf

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

Comparative branching-time semantics for Markov chains

Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Verena Wolf

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

17 Citations (Scopus)

81 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	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	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
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

Access to Document

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

17 Citations
1 Report

Comparative Branching-Time Semantics for Markov Chains
Baier, C., Katoen, J-P., Hermanns, H. & Wolf, V., Aug 2004, Enschede: Centre for Telematics and Information Technology (CTIT). 64 p. (CTIT technical report series; no. 04-32)
Research output: Book/Report › Report › Professional

Open Access
File

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.), CONCUR 2003 - Concurrency Theory: 14th International Conference, Marseille, France, September 3-5, 2003. Proceedings (pp. 492-507). (Lecture Notes in Computer Science; Vol. 2761). 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",

author = "Christel Baier and Holger Hermanns and Joost-Pieter Katoen and Verena Wolf",

year = "2003",

doi = "10.1007/978-3-540-45187-7_32",

language = "English",

isbn = "978-3-540-40753-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "492--507",

editor = "Roberto Amadio and Denis Lugiez",

booktitle = "CONCUR 2003 - Concurrency Theory",

note = "14th International Conference on Concurrency Theory, CONCUR 2003, CONCUR ; Conference date: 03-09-2003 Through 05-09-2003",

}

Baier, C, Hermanns, H, Katoen, J-P & Wolf, V 2003, Comparative branching-time semantics for Markov chains. in R Amadio & D Lugiez (eds), CONCUR 2003 - Concurrency Theory: 14th International Conference, Marseille, France, September 3-5, 2003. Proceedings. Lecture Notes in Computer Science, 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, Holger; Katoen, Joost-Pieter et al.

CONCUR 2003 - Concurrency Theory: 14th International Conference, Marseille, France, September 3-5, 2003. Proceedings. ed. / Roberto Amadio; Denis Lugiez. Berlin : Springer, 2003. p. 492-507 (Lecture Notes in Computer Science; Vol. 2761).

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, Holger

AU - Katoen, Joost-Pieter

AU - Wolf, Verena

N1 - Conference code: 14

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

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 - CONCUR 2003 - Concurrency Theory

A2 - Amadio, Roberto

A2 - Lugiez, Denis

PB - Springer

CY - Berlin

T2 - 14th International Conference on Concurrency Theory, CONCUR 2003

Y2 - 3 September 2003 through 5 September 2003

ER -

Comparative branching-time semantics for Markov chains

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Research output

Comparative Branching-Time Semantics for Markov Chains

Cite this