Abstract
This paper introduces strong bisimulation for continuoustime 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 measuretheoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Neuhäußer, M. R., & Katoen, J. P. (2007). Bisimulation and logical preservation for continuous-time Markov decision processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4703 LNCS, pp. 412–427). Springer Verlag. https://doi.org/10.1007/978-3-540-74407-8_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
