Trace Relations and Logical Preservation for Continuous-Time Markov Decision Processes

摘要

Equivalence relations are widely used for comparing the behavior of stochastic systems. This paper introduces several variants of trace equivalence for continuous-time Markov decision processes (CTMDPs). These trace equivalences are obtained as a result of button pushing experiments with a black box model of CTMDP. For every class of CTMDP scheduler, a corresponding variant of trace equivalence has been introduced. We investigate the relationship among these trace equivalences and also compare them with bisimulation for CTMDPs. Finally, we prove that the properties specified using deterministic timed automaton (DTA) specifications and metric temporal logic (MTL) formulas are preserved under some of these trace equivalences.