MARCIE -- model checking and reachability analysis done efficiently. MARCIE is a tool for the analysis of generalized stochastic Petri nets which can be augmented by rewards. The supported analysis methods range from qualitative and quantitative standard properties to model checking of established temporal logics. MARCIE’s analysis engines for bounded Petri net models are based on Interval Decision Diagrams. They are complemented by simulative and approximative engines to allow for quantitative reasoning on unbounded models. Most of the quantitative analyses benefit from a multi-threaded implementation. This paper gives an overview on MARCIE’s functionality and architecture and reports on the recently added feature of CSRL and PLTLc model checking.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Barbot, Beno^ıt; Kwiatkowska, Marta: On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets (2015)
- Blätke, Mary Ann; Rohr, Christian; Heiner, Monika; Marwan, Wolfgang: A Petri-net-based framework for biomodel engineering (2014)
- Heiner, Monika; Rohr, Christian; Schwarick, Martin: MARCIE -- model checking and reachability analysis done efficiently (2013)
- Heiner, Monika; Herajy, Mostafa; Liu, Fei; Rohr, Christian; Schwarick, Martin: Snoopy -- a unifying Petri net tool (2012)