@book{f12bec19317a4850800e8402ca99c1c9,
title = "CSL Model Checking of Deterministic and Stochastic Petri Nets",
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 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 verication 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.",
keywords = "EWI-5716, METIS-248094, IR-57050",
author = "{Martinez Verdugo}, J.M. and Haverkort, {Boudewijn R.H.M.}",
note = "Imported from CTIT",
year = "2005",
month = dec,
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-05-63",
address = "Netherlands",
}