|
Published Articles >> Table of Contents >> Abstract
The Quantitative Evaluation of Systems, First International Conference on (QEST'04)
pp. 220-229
Backward Stochastic Bisimulation in CSL Model Checking
Jeremy Sproston, Università di Torino, Italy
Susanna Donatelli, Università di Torino, Italy
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2004.10033
Send link to a friend
| 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.
|
 Additional Information
|
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
|
|
