TY - GEN
T1 - CSL model checking for generalized stochastic Petri nets
AU - Cerotti, Davide
AU - Donatelli, Susanna
AU - Horváth, András
AU - Sproston, Jeremy
PY - 2006
Y1 - 2006
N2 - This paper presents a Continuous Stochastic Logic (CSL) model-checking algorithm for Generalized Stochastic Petri Nets (GSPNs). CSL is a temporal logic defined over Continuous Time Markov Chains (CTMCs). GSPNs are a class of Stochastic Petri Nets in which sojourn times in states are either exponentially distributed (tangible states) or deterministically zero (vanishing states). Although vanishing states have zero probabilities, they can be relevant for the definition of system properties expressed as CSL formulae: the semantics of CSL is therefore modified accordingly. The paper then shows how the set of GSPN states which satisfy a CSL formula can be computed through the solution of CTMCs produced from a series of embedded Discrete Time Markov Chains modified according to the formula being checked.
AB - This paper presents a Continuous Stochastic Logic (CSL) model-checking algorithm for Generalized Stochastic Petri Nets (GSPNs). CSL is a temporal logic defined over Continuous Time Markov Chains (CTMCs). GSPNs are a class of Stochastic Petri Nets in which sojourn times in states are either exponentially distributed (tangible states) or deterministically zero (vanishing states). Although vanishing states have zero probabilities, they can be relevant for the definition of system properties expressed as CSL formulae: the semantics of CSL is therefore modified accordingly. The paper then shows how the set of GSPN states which satisfy a CSL formula can be computed through the solution of CTMCs produced from a series of embedded Discrete Time Markov Chains modified according to the formula being checked.
UR - http://www.scopus.com/inward/record.url?scp=41149180231&partnerID=8YFLogxK
U2 - 10.1109/QEST.2006.13
DO - 10.1109/QEST.2006.13
M3 - Conference contribution
AN - SCOPUS:41149180231
SN - 0769526659
SN - 9780769526652
T3 - Third International Conference on the Quantitative Evaluation of Systems, QEST 2006
SP - 199
EP - 208
BT - Third International Conference on the Quantitative Evaluation of Systems, QEST 2006
T2 - 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006
Y2 - 11 September 2006 through 14 September 2006
ER -