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 | English |
---|---|
Title of host publication | CONCUR 2007 – Concurrency Theory |
Subtitle of host publication | 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007. Proceedings |
Place of Publication | London |
Publisher | Springer |
Pages | 412-427 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-540-74407-8 |
ISBN (Print) | 978-3-540-74406-1 |
DOIs | |
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 |
Volume | 4703 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
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
- Continuous-time Markov decision process (CTMDP)