MathMC: A Mathematica-Based Tool for CSL Model Checking of Deterministic and Stochastic Petri Nets

Author

Martinez, J.M. ; Haverkort, B.J.

Author_Institution

Fac. of Electr. Eng., Math. & Comput. Sci., Twente Univ., Enschede

fYear

2006

fDate

11-14 Sept. 2006

Firstpage

133

Lastpage

134

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

Keywords

Markov processes; Petri nets; continuous time systems; discrete event systems; mathematics computing; probabilistic logic; program verification; temporal logic; CSL model checking; MathMC; Mathematica-based tool; branching temporal logic; continuous stochastic logic; continuous time Markov chains; deterministic Petri nets; discrete-event systems; exponentially distributed time; high-level formalism; stochastic Petri nets; CSL; DSPNs; Markov process; Markov regenerative process.; model checking;

fLanguage

English

Publisher

ieee

Conference_Titel

Quantitative Evaluation of Systems, 2006. QEST 2006. Third International Conference on

Conference_Location

Riverside, CA

Print_ISBN

0-7695-2665-9

Type

conf

DOI

10.1109/QEST.2006.29

Filename

1704004