loading...
CSL Model Checking for Generalized Stochastic Petri Nets
Riverside, California September 11-September 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2006.13Third International Conference on the ...
 This Article 
 
PDF
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Davide Cerotti, Universita di Torino, 10149 Torino, Italy
Susanna Donatelli, Universita di Torino, 10149 Torino, Italy
Andras Horvath, Universita di Torino, 10149 Torino, Italy
Jeremy Sproston, Universita di Torino, 10149 Torino, Italy
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.
Citation:
Davide Cerotti, Susanna Donatelli, Andras Horvath, Jeremy Sproston, "CSL Model Checking for Generalized Stochastic Petri Nets," qest, pp.199-210, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.