CSL model checking of deterministic and stochastic Petri nets


Share/Save/Bookmark

Martinez, José M and Haverkort, Boudewijn R. (2006) CSL model checking of deterministic and stochastic Petri nets. In: 13th GI/ITG Conference on Measuring, Modelling and Evaluation of Computer and Communication Systems, March 27-29, 2006, Nürnberg, Germany (pp. pp. 265-282).

open access
[img]
Preview
PDF
248kB
Abstract:Deterministic and Stochastic Petri Nets (DSPNs) are a widely used high-level formalism for modeling discrete-event systems where events may occur either without consuming time, after a deterministic time, or after an exponentially distributed time. The underlying process defined by DSPNs, under certain restrictions, corresponds to a class of Markov Regenerative Stochastic Processes (MRGP). In this paper, we investigate the use of CSL (Continuous Stochastic Logic) to express probabilistic properties, such a time-bounded until and time-bounded next, at the DSPN level. The veri�cation of such properties requires the solution of the steady-state and transient probabilities of the underlying MRGP. We also address a number of semantic issues regarding the application of CSL on MRGP and provide numerical model checking algorithms for this logic. A prototype model checker, based on SPNica, is also described.
Item Type:Conference or Workshop Item
Copyright:© 2006 VDE
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66852
Publisher URL:http://www.vde-verlag.de/data/buecher.php?action=bookdetail&vertriebsnr=562945
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 237894