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.

CSL Model Checking for Generalized Stochastic Petri Nets

CEROTTI, DAVIDE;DONATELLI, Susanna;HORVATH, Andras;SPROSTON, Jeremy James
2006-01-01

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.
2006
Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QEST'06)
IEEE Computer Society Press
199
210
0769526659
D. CEROTTI; S. DONATELLI; A. HORVATH; J. SPROSTON
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/125301
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact