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 dened 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 verification 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.
|Title of host publication||Proceedings 13th GI/ITG conference on measuring, Modelling and Evaluation of Computer and Communication Systems|
|Editors||R. German, A. Heindl|
|Place of Publication||Berlin|
|Number of pages||18|
|Publication status||Published - 2006|
Martinez Verdugo, J. M., & Haverkort, B. R. H. M. (2006). CSL model checking of deterministic and stochastic Petri nets. In R. German, & A. Heindl (Eds.), Proceedings 13th GI/ITG conference on measuring, Modelling and Evaluation of Computer and Communication Systems (pp. 265-282). Berlin: VDE Verlag.