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 - Sept 2007 |
| Event | 18th International Conference on Concurrency Theory, CONCUR 2007 - Lisbon, Portugal Duration: 3 Sept 2007 → 8 Sept 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/Territory | Portugal |
| City | Lisbon |
| Period | 3/09/07 → 8/09/07 |
Keywords
- Continuous-time Markov decision process (CTMDP)