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 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||