Simulation for continuous-time Markov chains

Christel Baier; Joost P. Katoen; Holger Hermanns; Boudewijn Haverkort

doi:10.1007/3-540-45694-5_23

Simulation for continuous-time Markov chains

Christel Baier, Joost P. Katoen, Holger Hermanns, Boudewijn Haverkort

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

19 Citations (Scopus)

27 Downloads (Pure)

Abstract

This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

Original language	English
Title of host publication	CONCUR 2002 — Concurrency Theory
Subtitle of host publication	13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings
Editors	Luboš Brim, Mojmír Křetínský, Antonín Kučera, Petr Jančar
Place of Publication	978-3-540-45694-0
Publisher	Springer
Pages	338-354
ISBN (Electronic)	978-3-540-45694-0
ISBN (Print)	978-3-540-44043-7
DOIs	https://doi.org/10.1007/3-540-45694-5_23
Publication status	Published - 2002
Event	13th International Conference on Concurrency Theory, CONCUR 2002 - Brno, Czech Republic Duration: 20 Aug 2002 → 23 Aug 2002 Conference number: 13

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2421
ISSN (Print)	0302-9743

Conference

Conference	13th International Conference on Concurrency Theory, CONCUR 2002
Abbreviated title	CONCUR
Country/Territory	Czech Republic
City	Brno
Period	20/08/02 → 23/08/02

Keywords

FMT-MC: MODEL CHECKING
FMT-PM: PROBABILISTIC METHODS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

Access to Document

10.1007/3-540-45694-5_23

Cite this

Baier, C., Katoen, J. P., Hermanns, H., & Haverkort, B. (2002). Simulation for continuous-time Markov chains. In L. Brim, M. Křetínský, A. Kučera, & P. Jančar (Eds.), CONCUR 2002 — Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings (pp. 338-354). (Lecture Notes in Computer Science; Vol. 2421). Springer. https://doi.org/10.1007/3-540-45694-5_23

Baier, Christel ; Katoen, Joost P. ; Hermanns, Holger et al. / Simulation for continuous-time Markov chains. CONCUR 2002 — Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings. editor / Luboš Brim ; Mojmír Křetínský ; Antonín Kučera ; Petr Jančar. 978-3-540-45694-0 : Springer, 2002. pp. 338-354 (Lecture Notes in Computer Science).

@inproceedings{b29d0b55e3d9499592a269241d02a85e,

title = "Simulation for continuous-time Markov chains",

abstract = "This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.",

keywords = "FMT-MC: MODEL CHECKING, FMT-PM: PROBABILISTIC METHODS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS",

author = "Christel Baier and Katoen, {Joost P.} and Holger Hermanns and Boudewijn Haverkort",

year = "2002",

doi = "10.1007/3-540-45694-5_23",

language = "English",

isbn = "978-3-540-44043-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "338--354",

editor = "Lubo{\v s} Brim and Mojm{\'i}r K{\v r}et{\'i}nsk{\'y} and Anton{\'i}n Ku{\v c}era and Petr Jan{\v c}ar",

booktitle = "CONCUR 2002 — Concurrency Theory",

address = "Germany",

note = "13th International Conference on Concurrency Theory, CONCUR 2002, CONCUR ; Conference date: 20-08-2002 Through 23-08-2002",

}

Baier, C, Katoen, JP, Hermanns, H & Haverkort, B 2002, Simulation for continuous-time Markov chains. in L Brim, M Křetínský, A Kučera & P Jančar (eds), CONCUR 2002 — Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings. Lecture Notes in Computer Science, vol. 2421, Springer, 978-3-540-45694-0, pp. 338-354, 13th International Conference on Concurrency Theory, CONCUR 2002, Brno, Czech Republic, 20/08/02. https://doi.org/10.1007/3-540-45694-5_23

Simulation for continuous-time Markov chains. / Baier, Christel; Katoen, Joost P.; Hermanns, Holger et al.
CONCUR 2002 — Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings. ed. / Luboš Brim; Mojmír Křetínský; Antonín Kučera; Petr Jančar. 978-3-540-45694-0: Springer, 2002. p. 338-354 (Lecture Notes in Computer Science; Vol. 2421).

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

TY - GEN

T1 - Simulation for continuous-time Markov chains

AU - Baier, Christel

AU - Katoen, Joost P.

AU - Hermanns, Holger

AU - Haverkort, Boudewijn

N1 - Conference code: 13

PY - 2002

Y1 - 2002

N2 - This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

AB - This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

KW - FMT-MC: MODEL CHECKING

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

U2 - 10.1007/3-540-45694-5_23

DO - 10.1007/3-540-45694-5_23

M3 - Conference contribution

SN - 978-3-540-44043-7

T3 - Lecture Notes in Computer Science

SP - 338

EP - 354

BT - CONCUR 2002 — Concurrency Theory

A2 - Brim, Luboš

A2 - Křetínský, Mojmír

A2 - Kučera, Antonín

A2 - Jančar, Petr

PB - Springer

CY - 978-3-540-45694-0

T2 - 13th International Conference on Concurrency Theory, CONCUR 2002

Y2 - 20 August 2002 through 23 August 2002

ER -

Baier C, Katoen JP, Hermanns H, Haverkort B. Simulation for continuous-time Markov chains. In Brim L, Křetínský M, Kučera A, Jančar P, editors, CONCUR 2002 — Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings. 978-3-540-45694-0: Springer. 2002. p. 338-354. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45694-5_23

Simulation for continuous-time Markov chains

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this