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

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 CSL 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. [ABSTRACT FROM AUTHOR]