The Quantitative Evaluation of Systems, First International Conference on (QEST'04)
Backward Stochastic Bisimulation in CSL Model Checking
Enschede, the Netherlands
September 27-September 30
ISBN: 0-7695-2185-1
Equivalence relations can be used to reduce the state space of a system model, thereby permitting more efficient analysis. We study backward stochastic bisimulation in the context of model checking continuous-time Markov chains against Continuous Stochastic Logic (CSL) properties. While there are simple CSL properties that are not preserved when reducing the state space of a continuous-time Markov chain using backward stochastic bisimulation, we show that the equivalence can nevertheless be used in the verification of a practically significant class of CSL properties. Furthermore, we identify the logical properties for which the requirement on the equality of state-labelling sets (normally imposed on state equivalences in a model-checking context) can be omitted from the definition of the equivalence, resulting in a better state-space reduction.
Citation:
Jeremy Sproston, Susanna Donatelli, "Backward Stochastic Bisimulation in CSL Model Checking," qest, pp.220-229, The Quantitative Evaluation of Systems, First International Conference on (QEST'04), 2004