CSL Model Checking for Generalized Stochastic Petri Nets
D. Cerotti, S. Donatelli, A. Horváth, J. Sproston
Abstract:
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.
PDF
András Horváth, 2008-06-25