Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

M. Neuhausser; Joost P. Katoen

doi:10.1007/978-3-540-74407-8_28

Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

M. Neuhausser, Joost P. Katoen

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

20 Citations (Scopus)

Abstract

This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL - a stochastic variant of CTL for continuous-time Markov chains - on CTMDPs and show its measure theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.

Original language	Undefined
Title of host publication	18th International Conference on Concurrency Theory (CONCUR)
Place of Publication	London
Publisher	Springer
Pages	412-427
Number of pages	16
ISBN (Print)	978-3-540-74406-1
DOIs	https://doi.org/10.1007/978-3-540-74407-8_28
Publication status	Published - Sep 2007
Event	18th International Conference on Concurrency Theory, CONCUR 2007 - Lisbon, Portugal Duration: 3 Sep 2007 → 8 Sep 2007 Conference number: 18

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Number	Supplement
Volume	4703

Conference

Conference	18th International Conference on Concurrency Theory, CONCUR 2007
Abbreviated title	CONCUR
Country	Portugal
City	Lisbon
Period	3/09/07 → 8/09/07

Keywords

IR-64519
METIS-245846
EWI-11539

Cite this

Neuhausser, M., & Katoen, J. P. (2007). Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. In 18th International Conference on Concurrency Theory (CONCUR) (pp. 412-427). [10.1007/978-3-540-74407-8_28] (Lecture Notes in Computer Science; Vol. 4703, No. Supplement). London: Springer. https://doi.org/10.1007/978-3-540-74407-8_28

@inproceedings{960bed9aeab946a99c5a346e9a6b61c7,

title = "Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes",

abstract = "This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL - a stochastic variant of CTL for continuous-time Markov chains - on CTMDPs and show its measure theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.",

keywords = "IR-64519, METIS-245846, EWI-11539",

author = "M. Neuhausser and Katoen, {Joost P.}",

note = "10.1007/978-3-540-74407-8_28",

year = "2007",

month = "9",

doi = "10.1007/978-3-540-74407-8_28",

language = "Undefined",

isbn = "978-3-540-74406-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "Supplement",

pages = "412--427",

booktitle = "18th International Conference on Concurrency Theory (CONCUR)",

}

Neuhausser, M & Katoen, JP 2007, Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. in 18th International Conference on Concurrency Theory (CONCUR)., 10.1007/978-3-540-74407-8_28, Lecture Notes in Computer Science, no. Supplement, vol. 4703, Springer, London, pp. 412-427, 18th International Conference on Concurrency Theory, CONCUR 2007, Lisbon, Portugal, 3/09/07. https://doi.org/10.1007/978-3-540-74407-8_28

Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. / Neuhausser, M.; Katoen, Joost P.

18th International Conference on Concurrency Theory (CONCUR). London : Springer, 2007. p. 412-427 10.1007/978-3-540-74407-8_28 (Lecture Notes in Computer Science; Vol. 4703, No. Supplement).

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

TY - GEN

T1 - Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

AU - Neuhausser, M.

AU - Katoen, Joost P.

N1 - 10.1007/978-3-540-74407-8_28

PY - 2007/9

Y1 - 2007/9

N2 - This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL - a stochastic variant of CTL for continuous-time Markov chains - on CTMDPs and show its measure theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.

AB - This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL - a stochastic variant of CTL for continuous-time Markov chains - on CTMDPs and show its measure theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.

KW - IR-64519

KW - METIS-245846

KW - EWI-11539

U2 - 10.1007/978-3-540-74407-8_28

DO - 10.1007/978-3-540-74407-8_28

M3 - Conference contribution

SN - 978-3-540-74406-1

T3 - Lecture Notes in Computer Science

SP - 412

EP - 427

BT - 18th International Conference on Concurrency Theory (CONCUR)

PB - Springer

CY - London

ER -

Access to Document

10.1007/978-3-540-74407-8_28

http://eprints.eemcs.utwente.nl/secure2/11539/01/ctmdp_logic.pdf