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

Martinez, José M and Haverkort, Boudewijn R. (2006) MathMC: A mathematica-based tool for CSL model checking of deterministic and stochastic Petri nets. In: Third International Conference on the Quantitative Evaluation of Systems, 11-14 September 2006, Riverside, CA, USA.

Preview

PDF
95Kb

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.
Item Type:	Conference or Workshop Item
Copyright:	© 2006 IEEE
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Design and Analysis of Communication Systems (DACS)
Link to this item:	http://purl.utwente.nl/publications/66850
Official URL:	http://dx.doi.org/10.1109/QEST.2006.29
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 237892