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 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.