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

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

doi:10.1109/QEST.2006.29

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 proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

261 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 language	Undefined
Title of host publication	Proceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems
Place of Publication	Los Alamitos
Publisher	IEEE
Pages	133-134
Number of pages	2
ISBN (Print)	978-0-7695-2665-2
DOIs	https://doi.org/10.1109/QEST.2006.29
Publication status	Published - 2006
Event	3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States Duration: 11 Sept 2006 → 14 Sept 2006 Conference number: 3 http://www.qest.org/qest2006/

Publication series

Name
Publisher	IEEE Computer Society Press
Number	Paper PMD-

Conference

Conference	3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
Abbreviated title	QEST
Country/Territory	United States
City	Riverside
Period	11/09/06 → 14/09/06
Internet address	http://www.qest.org/qest2006/

Keywords

EWI-8990
IR-66850
METIS-237892

Access to Document

10.1109/QEST.2006.29

Martinez06mathmc

Cite this

@inproceedings{528eb18509194adf9984f42e1f13661e,

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

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

keywords = "EWI-8990, IR-66850, METIS-237892",

author = "{Martinez Verdugo}, J.M. and Haverkort, {Boudewijn R.H.M.}",

note = "10.1109/QEST.2006.29 ; 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 ; Conference date: 11-09-2006 Through 14-09-2006",

year = "2006",

doi = "10.1109/QEST.2006.29",

language = "Undefined",

isbn = "978-0-7695-2665-2",

publisher = "IEEE",

number = "Paper PMD-",

pages = "133--134",

booktitle = "Proceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems",

address = "United States",

url = "http://www.qest.org/qest2006/",

}

Martinez Verdugo, JM & Haverkort, BRHM 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., 10.1109/QEST.2006.29, IEEE, Los Alamitos, pp. 133-134, 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006, Riverside, California, United States, 11/09/06. https://doi.org/10.1109/QEST.2006.29

MathMC: A mathematica-based tool for CSL model checking of deterministic and stochastic Petri nets. / Martinez Verdugo, J.M.; Haverkort, Boudewijn R.H.M.
Proceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems. Los Alamitos: IEEE, 2006. p. 133-134 10.1109/QEST.2006.29.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Martinez Verdugo, J.M.

AU - Haverkort, Boudewijn R.H.M.

N1 - Conference code: 3

PY - 2006

Y1 - 2006

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

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

KW - EWI-8990

KW - IR-66850

KW - METIS-237892

U2 - 10.1109/QEST.2006.29

DO - 10.1109/QEST.2006.29

M3 - Conference contribution

SN - 978-0-7695-2665-2

SP - 133

EP - 134

BT - Proceedings of the Third Int'l. Conference on the Quantitative Evaluation of Systems

PB - IEEE

CY - Los Alamitos

T2 - 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006

Y2 - 11 September 2006 through 14 September 2006

ER -