MathMC: A mathematica-based tool for CSL model checking of deterministic and stochastic Petri nets

J.M. Martinez Verdugo, Boudewijn R.H.M. Haverkort

Research output: Other contribution

1 Citation (Scopus)

Abstract

Deterministic and Stochastic Petri Nets (DSPNs) are a widely used high-level formalism for modeling discreteevent systems where events may occur either without consuming time, after a deterministic time, or after an exponentially distributed time. CSL (Continuous Stochastic Logic) is a (branching) temporal logic developed to express probabilistic properties in continuous time Markov chains (CTMCs). In this paper we present a Mathematica-based tool that implements recent developments for model checking CSL style properties on DSPNs. Furthermore, as a consequence of the type of process underlying DSPNs (a superset of Markovian processes), we are also able to check CSL properties of Generalized Stochastic Petri Nets (GSPNs) and labeled CTMCs.
Original languageEnglish
PublisherIEEE Computer Society
Number of pages2
Place of PublicationLos Alamitos
ISBN (Print)978-0-7695-2665-2
DOIs
Publication statusPublished - 2006
Externally publishedYes

Keywords

  • EWI-8990
  • IR-66850
  • METIS-237892

Fingerprint Dive into the research topics of 'MathMC: A mathematica-based tool for CSL model checking of deterministic and stochastic Petri nets'. Together they form a unique fingerprint.

  • Cite this