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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    101 Downloads (Pure)

    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 languageUndefined
    Title of host publicationProceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems
    Place of PublicationLos Alamitos
    PublisherIEEE Computer Society Press
    Pages133-134
    Number of pages2
    ISBN (Print)978-0-7695-2665-2
    DOIs
    Publication statusPublished - 2006
    Event3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States
    Duration: 11 Sep 200614 Sep 2006
    Conference number: 3
    http://www.qest.org/qest2006/

    Publication series

    Name
    PublisherIEEE Computer Society Press
    NumberPaper PMD-

    Conference

    Conference3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
    Abbreviated titleQEST
    CountryUnited States
    CityRiverside
    Period11/09/0614/09/06
    Internet address

    Keywords

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

    Cite this

    Martinez Verdugo, J. M., & Haverkort, B. R. H. M. (2006). MathMC: A mathematica-based tool for CSL model checking of deterministic and stochastic Petri nets. In Proceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems (pp. 133-134). [10.1109/QEST.2006.29] Los Alamitos: IEEE Computer Society Press. https://doi.org/10.1109/QEST.2006.29