loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Jeremy Sproston, Universit? di Torino, Italy
Susanna Donatelli, Universit? di Torino, Italy
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.