Paper Details

Simulation for Continuous-Time Markov Chains
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn Haverkort

This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is shown to be a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.