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 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Barbot, Beno^ıt; Kwiatkowska, Marta: On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets (2015)
- Dannenberg, Frits; Hahn, Ernst Moritz; Kwiatkowska, Marta: Computing cumulative rewards using fast adaptive uniformization (2015)
- Amparore, Elvio Gilberto; Beccuti, Marco; Donatelli, Susanna: (Stochastic) model checking in greatspn (2014)
- Blätke, Mary Ann; Rohr, Christian; Heiner, Monika; Marwan, Wolfgang: A Petri-net-based framework for biomodel engineering (2014)
- Brim, Luboš; Češka, Milan; Šafránek, David: Model checking of biological systems (2013)
- 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) ioport