Simulation for Continuous Time Markov ChainsChristel Baier (Baier@cs.uni-bonn.de) Abstract Simulation and bisimulation relations are widely used to compare the stepwise behaviour of transition systems. The talk presents a notion of a simulation preorder for Continuous Time Markov Chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result is that the simulation preorder preserves quantitative safety properties such as "with high probability the system is safe in the next t time units''. |