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.
|
concur02@fi.muni.cz |