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.

Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools

D'APRILE, DAVIDE;DONATELLI, Susanna;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 6th International Conference on Application of Concurrency to System Design (ACSD'06)
IEEE Computer Society Press
143
152
0769525563
D. CEROTTI; D. D'APRILE; S. DONATELLI; 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/124930
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact