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.
Backward Stochastic Bisimulation in CSL Model Checking
SPROSTON, Jeremy James;DONATELLI, Susanna
2004-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.