CSL model checking of deterministic and stochastic Petri nets

J.M. Martinez Verdugo, Boudewijn R.H.M. Haverkort, R. German, A. Heindl (Editor)

Research output: Other contributionOther research output

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 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.
Original languageEnglish
PublisherVDE Verlag GMBH
Number of pages18
Place of PublicationBerlin
ISBN (Print)978-3-8007-2945-6
Publication statusPublished - 2006
Externally publishedYes

Fingerprint

Model checking
Random processes
Petri nets
Discrete event simulation
Numerical models
Semantics

Keywords

  • EWI-8992
  • METIS-237894
  • IR-66852

Cite this

Martinez Verdugo, J. M., Haverkort, B. R. H. M., German, R., & Heindl, A. (Ed.) (2006). CSL model checking of deterministic and stochastic Petri nets. Berlin: VDE Verlag GMBH.
Martinez Verdugo, J.M. ; Haverkort, Boudewijn R.H.M. ; German, R. ; Heindl, A. (Editor). / CSL model checking of deterministic and stochastic Petri nets. 2006. Berlin : VDE Verlag GMBH. 18 p.
@misc{9919b27dba154b20878464fc8ef24b58,
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 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.",
keywords = "EWI-8992, METIS-237894, IR-66852",
author = "{Martinez Verdugo}, J.M. and Haverkort, {Boudewijn R.H.M.} and R. German and A. Heindl",
year = "2006",
language = "English",
isbn = "978-3-8007-2945-6",
publisher = "VDE Verlag GMBH",
type = "Other",

}

Martinez Verdugo, JM, Haverkort, BRHM, German, R & Heindl, A (ed.) 2006, CSL model checking of deterministic and stochastic Petri nets. VDE Verlag GMBH, Berlin.

CSL model checking of deterministic and stochastic Petri nets. / Martinez Verdugo, J.M.; Haverkort, Boudewijn R.H.M.; German, R.; Heindl, A. (Editor).

18 p. Berlin : VDE Verlag GMBH. 2006, .

Research output: Other contributionOther research output

TY - GEN

T1 - CSL model checking of deterministic and stochastic Petri nets

AU - Martinez Verdugo, J.M.

AU - Haverkort, Boudewijn R.H.M.

AU - German, R.

A2 - Heindl, A.

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - EWI-8992

KW - METIS-237894

KW - IR-66852

M3 - Other contribution

SN - 978-3-8007-2945-6

PB - VDE Verlag GMBH

CY - Berlin

ER -

Martinez Verdugo JM, Haverkort BRHM, German R, Heindl A, (ed.). CSL model checking of deterministic and stochastic Petri nets. 2006. 18 p.