CSL model checking for generalized stochastic Petri nets

Davide Cerotti, Susanna Donatelli, András Horváth, Jeremy Sproston

Risultato della ricerca: Capitolo in libro/report/atti di convegnoContributo a conferenzapeer review

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.

Lingua originaleInglese
Titolo della pubblicazione ospiteThird International Conference on the Quantitative Evaluation of Systems, QEST 2006
Pagine199-208
Numero di pagine10
DOI
Stato di pubblicazionePubblicato - 2006
Pubblicato esternamente
Evento3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006 - Riverside, CA, United States
Durata: 11 set 200614 set 2006

Serie di pubblicazioni

NomeThird International Conference on the Quantitative Evaluation of Systems, QEST 2006

???event.eventtypes.event.conference???

???event.eventtypes.event.conference???3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006
Paese/TerritorioUnited States
CittàRiverside, CA
Periodo11/09/0614/09/06

Fingerprint

Entra nei temi di ricerca di 'CSL model checking for generalized stochastic Petri nets'. Insieme formano una fingerprint unica.

Cita questo