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

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