data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

M A R C I E

latest update: November 19, 2019, at 01:01 PM

---

Please use the following reference to give credits to Marcie:
M Heiner, C Rohr and M Schwarick:
MARCIE - Model checking And Reachability analysis done effiCIEntly;
In Proc. PETRI NETS 2013, Milano, Springer, LNCS, volume 7927, pp. 389–399, June 2013 (e-link).

---

• News
• General Description
• User Manual
• Downloads
• Related Papers
• Related Tools
• Case Studies
• Bug Reports
• FAQ

News

• 2017-07-27
  • The report for the Model Checking Contest @ Petri Nets 2017 is online;
    10 tools participated in five categories.
  • 

Marcie reached a reliability of 100% based on 27,041 examinations,
and scored bronze in the category upper bounds, in the official point ranking.

• Marcie & MCC'2017, some comments
• For comparison, here some results of the unofficial correct value ranking

category CTL Formulas	correct values	points
1. MARCIE	9115	20 851
2. LoLA	8598	56 429
3. ITS-Tools	7603	21 436
4. Tapaal	7462	42 429
5. LTSMin	7055	16 792
6. GreatSPN	6864	20 091

category Upper Bounds	correct values	points
1. MARCIE	5726	14 200
2. GreatSPN	5709	19 834
3. ITS-Tools	5645	17 933
4. LoLA	4014	13 894
5. LTSMin	3958	9 496
6. Tapaal	3088	8 286

category State Space	correct values	points
1. TINA.tedd	1641	17 988
2. GreatSPN	1611	20 302
3. MARCIE	1499	13 462
4. ITS-Tools	1143	15 880
5. smart	862	10 688
6. LTSMin	792	8 400
7. TINA.stif	724	6 402
8. Tapaal	477	5 040

• 2017-06-19
  • windows version available
  • some bug fixes
• 2017-04-18
  • completely static build on linux
  • some bug fixes
• 2017-04-18
  • added BDD engine for symbolic state space analysis of 1-bounded Petri nets
  • to use it call "WITH_BDD=1 marcie ..."
• 2016-12-27
  • new algorithm to detect leak transitions in DNA walker circuits
  • new tool andl_converter
• 2016-12-08
  • updated user manual released
• 2016-07-01
  • The report for the Model Checking Contest @ Petri Nets 2016 is online, see http://mcc.lip6.fr,
    10 tools participated in five categories; Marcie got three medals.
    
    
    1. Marcie scored GOLD in the category Upper Bounds
    2. Marcie scored SILVER in the category State Space Examination
    3. Marcie scored BRONZE in the category CTL Model Checking

• 2016-06-19
  • new approximate stochastic simulation method: delta-leaping
• 2016-04-14
  • bug fix release, because of a bug in the ctl parser
• 2016-03-07
  • bug fix release, because of a bug in the pnml parser
• 2016-02-10
  • bug fix release, because of a bug related to CTL model checking of formulas with AU and AX
• 2015-09-01
  • The report for the Model Checking Contest @ Petri Nets 2015 is online, see http://mcc.lip6.fr,
    10 tools participated in four categories; Marcie got three medals; no other tool got more than one medal.
    
    
    1. Marcie scored GOLD in the category State Space Examination
    2. Marcie scored GOLD in the category CTL Model Checking
    3. Marcie scored BRONZE in the category Reachability

• 2014-09-02
  • The report for the Model Checking Contest @ Petri Nets 2014 is online, see http://mcc.lip6.fr
    Marcie scored GOLD in the category state space examination:
    
    
    1. Marcie with 3845 points (it also has 90 honor points),
    2. pnmc with 3557 points (it also has 360 honor points),
    3. Tapaal with 1555 points (it also has 0 honor points).

• 2014-06-24
  • Model Checking Contest @ Petri Nets 2014,
    We submitted six models, which served as surprise models in this year's round.
    Marcie participated in the category "state space construction"; results are announced to be published soon here.
• 2013-06-25
  • Model Checking Contest @ Petri Nets 2013,
    Marcie won the following trophies:

	known models	surprise models	all models
state space generation (1 examination)	1 bronze medal	1 silver medal	1 silver medal
reachability properties (6 examinations)	2 bronze medal	4 gold medal 1 silver medal	2 bronze medal
CTL properties (5 examinations)	1 bronze medal	4 gold medal 1 silver medal	1 bronze medal

• Please note: in the surprise models category (unknown models), Marcie scored gold or silver in 11 out of 12 examinations.
• The detailed results are shown here.
• The pdf version of the report is available in the Cornell Research Repository (see http://arxiv.org/abs/1309.2485v1).

• 2012-07-19
  • some bug fixes
  • multi-threaded, symbolic CSRL model checking based on Markovian approximation
  • new input formats
    • Abstract Net Description Language (ANDL)
    • PNML for qualitative Petri nets
  • advanced simulation capabilities
    • steadystate detection
    • time unbounded temporal operators
• 2011-09-06
  • some bug fixes
  • PLTLc model checking
  • reward support for the simulative engine
  • experimental CSRL model checking (not documented)
• 2011-04-11
  • some minor changes and bug fixes
• 2011-02-17
  • bug fix concerning massaction kinetics
  • improved Gauss-Seidel solver
  • improved heuristics for generating variable orders
• 2010-12-23
  • first release of Marcie

General Description

Marcie - (M)odel checking (A)nd (R)eachability analysis done effi(CIE)ntly

Marcie is a tool for qualitative and quantitative analysis of Generalized Stochastic Petri nets with extended arcs. It comprises four engines.

(1) Qualitative analysis based on Interval Decision Diagrams (IDD)

• no previous knowledge of the boundedness degree required;
• efficient saturation-based reachability analysis;
• pre-computation of suitable static variable orders ;
• dead state analysis with trace generation;
• analysis of strongly connected components (liveness, reversibility);
• efficient CTL model checking;

(2) Quantitative analysis based on symbolic exact numerical analysis

• builds upon the IDD-based qualitative analysis engine;
• efficient on-the-fly analysis of the underlying CTMC (no Kronecker algebra, no Multi-Terminal Decision Diagrams);
• multi-threaded transient analysis (uniformization);
• multi-threaded computation of the joint distribution of time and accumulated reward (Markovian approximation and uniformization);
• steady state analysis using a Jacobi (multi-threaded), a Pseudo-Gauss-Seidel or a Gauss-Seidel solver;
• efficient CSL model checking;
• efficient CSRL model checking;
• low sensitivity to the number of distinct rate values;
• fixed number of IDD variables independent of boundedness degree;
• requires no partitioning of the set of places;

---

These two IDD-based engines outperform related tools for many case studies.

---

(3) Quantitative analysis based on explicit approximative numerical analysis

• efficient Fast Adaptive Uniformization (FAU) to compute an approximative probability distribution;
• model checking of the timed-bounded, unnested subset of CSL

(4) Quantitative analysis based on simulation

• multi-threaded trace generation based on Gillespie's exact stochastic simulation algorithm (SSA);
• simulative model checking of a subset of PLTL;

---

For detailed informations concerning data structures and algorithms see the related papers.

---

User manual

• latest version (31/05/2017): marcie-manual-2017.pdf
• [SRH16]
  M Schwarick, C Rohr and M Heiner:
  MARCIE Manual;
  Technical report 02-16, Brandenburg University of Technology Cottbus, Department of Computer Science, December 2016. [ url ] [ pdf ] [ BibTeX ]
• For a quick overview, take a look on these slides.

Downloads

Marcie is free for non-commercial use only. We provide the binaries for mac osx and linux (windows will follow) in the hope to be useful and with expectations of feedback.

• Windows (64bit)
• Mac OSX 10.11+ (64bit)
• Linux (64bit)

It is possible to use Marcie with a graphical user interface provided by the tool Charlie. The following steps are required:

• install Charlie
• copy plugin-CLT.zip to its plugin-folder
• copy the files options.dtd and marcie_linux/mac.xml into the folder of the marcie binary
• start Charlie and the CLT dialog and load the tool description file(xml)

andl_converter:

• convert andl, candl, pnml
• standalone unfolding using IDDs
• Windows (64bit)
• Mac OSX 10.11+ (64bit)
• Linux (64bit)

Related Papers

• Marcie & MCC'2017, some comments
• [HRST16]
  M Heiner, C Rohr, M Schwarick and A Tovchigrechko:
  MARCIE’s secrets of efficient model checking;
  Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) XI, LNCS 9930, 2016 (accepted: March 11, 2016). [ url ] [ doi ] [ BibTeX ]
• [Rohr16]
  Rohr, C:
  Discrete-Time Leap Method For Stochastic Simulation;
  In Proc. Int. Workshop on Biological Processes & Petri Nets (BioPPN 2016), CEUR-WS.org, CEUR Workshop Proceedings, volume 1591, pages 362–376, June 2016. [ url ] [ pdf ] [ BibTeX ]
• [Schwarick14]
  Martin Schwarick:
  Symbolic on-the-fly analysis of stochastic Petri nets;
  PhD thesis, BTU Cottbus, Dep. of CS, June 2014. [ pdf ] [ BibTeX ]
• [Rohr13]
  C Rohr:
  Simulative Model Checking of Steady-State and Time-Unbounded Temporal Operators;
  ToPNoC VIII, LNCS 8100, 2013. [ doi ] [ BibTeX ]
• [HRS13]
  M Heiner, C Rohr and M Schwarick:
  MARCIE - Model checking And Reachability analysis done effiCIEntly;
  In Proc. PETRI NETS 2013, Milano, Springer, LNCS, volume 7927, pages 389–399, June 2013. [ url ] [ pdf ] [ doi ] [ BibTeX ]
• [HRS13.sld]
  M Heiner, C Rohr and M Schwarick:
  MARCIE - Model checking And Reachability analysis done effiCIEntly;
  Talk, PETRI NETS 2013, Milano, June 2013. [ pdf ] [ BibTeX ]
• [Schw12]
  M Schwarick:
  Symbolic model checking of stochastic reward nets;
  In Proc. International Workshop on Concurrency, Specification, and Programming (CSP 2012), CEUR-WS.org, CEUR Workshop Proceedings, volume 928, pages 343–357, September 2012. [ url ] [ pdf ] [ BibTeX ]
• [SRH11]
  M Schwarick , C Rohr and M Heiner:
  MARCIE - Model checking And Reachability analysis done effiCIEntly;
  In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST 2011), Aachen, Germany, IEEE CS Press, pages 91–100, September 2011. [ url ] [ pdf ] [ BibTeX ]
• [Schw10]
  M Schwarick:
  IDD-MC - a model checker for bounded stochastic Petri nets;
  In Proc. 17th German Workshop on Algorithms and Tools for Petri Nets (AWPN 2010), CEUR-WS.org, CEUR Workshop Proceedings, volume 643, pages 80–87, October 2010. [ pdf ] [ BibTeX ]
• [HRSS10]
  M Heiner, C Rohr, M Schwarick and S Streif:
  A Comparative Study of Stochastic Analysis Techniques;
  In Proc. 8th International Conference on Computational Methods in Systems Biology (CMSB 2010), Trento, ACM digital library, pages 96–106, September 2010. [ pdf ] [ doi ] [ BibTeX ]
• [SH09]
  M Schwarick and M Heiner:
  CSL model checking of biochemical networks with Interval Decision Diagrams;
  In Proc. 7th International Conference on Computational Methods in Systems Biology (CMSB 2009), Bologna, Italy, Springer, LNCS/LNBI, volume 5688, pages 296–312, September 2009. [ url ] [ pdf ] [ doi ] [ BibTeX ]
• [HST09]
  M Heiner, M Schwarick and A Tovchigrechko:
  DSSZ-MC – A Tool for Symbolic Analysis of Extended Petri Nets;
  In Proc. PETRI NETS 2009, Paris, Springer, LNCS, volume 5606, pages 323–332, June 2009. [ url ] [ pdf ] [ doi ] [ BibTeX ]
• [Schw08]
  M Schwarick:
  Transient Analysis of Stochastic Petri Nets With Interval Decision Diagrams;
  In Proc. 15th German Workshop on Algorithms and Tools for Petri Nets (AWPN 2008), CEUR-WS.org, CEUR Workshop Proceedings, volume 380, pages 43–48, September 2008. [ pdf ] [ BibTeX ]
• [Tovchig08]
  Alexey Tovchigrechko:
  Efficient symbolic analysis of bounded Petri nets using Interval Decision Diagrams;
  PhD thesis, BTU Cottbus, Dep. of CS, October 2008. [ pdf ] [ BibTeX ]
• [Lehr07]
  Sebastian Lehrack:
  A Modelling and Simulation Tool for Stochastic Petri Nets Models of Biochemical Networks (in German);
  Diploma thesis, BTU Cottbus, Dep. of CS, November 2007. [ pdf ] [ BibTeX ]
• [Tovc04]
  A Tovchigrechko:
  Model Checking of Bounded Petri Nets Using Interval Diagrams;
  Technical report I-05/2004, Brandenburg University of Technology Cottbus, Department of Computer Science, November 2004. [ pdf ] [ BibTeX ]
• [Spranger01]
  Jochen Spranger:
  Symbolic LTL verification of Petri nets;
  PhD thesis, BTU Cottbus, Dep. of CS, December 2001. [ pdf ] [ BibTeX ]
• [Noac99]
  Andreas Noack:
  Ein ZBDD-Paket für effizientes Model Checking von Petrinetzen;
  Study thesis, BTU Cottbus, Dep. of CS, June 1999. [ BibTeX ]

Related Tools

• modelling tools
  • Snoopy
• other CSL model checker
  • PRISM - probabilistic symbolic model checker
  • MRMC - markov reward model checker

Case Studies»

For some benchmark case studies, see also:

• [SRH11]
  M Schwarick , C Rohr and M Heiner:
  MARCIE - Model checking And Reachability analysis done effiCIEntly;
  In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST 2011), Aachen, Germany, IEEE CS Press, pages 91–100, September 2011. [ url ] [ pdf ] [ BibTeX ]
• [HRSS10]
  M Heiner, C Rohr, M Schwarick and S Streif:
  A Comparative Study of Stochastic Analysis Techniques;
  In Proc. 8th International Conference on Computational Methods in Systems Biology (CMSB 2010), Trento, ACM digital library, pages 96–106, September 2010. [ pdf ] [ doi ] [ BibTeX ]
• [SH09]
  M Schwarick and M Heiner:
  CSL model checking of biochemical networks with Interval Decision Diagrams;
  In Proc. 7th International Conference on Computational Methods in Systems Biology (CMSB 2009), Bologna, Italy, Springer, LNCS/LNBI, volume 5688, pages 296–312, September 2009. [ url ] [ pdf ] [ doi ] [ BibTeX ]

Bug Reports

Submit your bug reports and comments about Marcie here.

• Please check, if your problem still exists in the latest available version of Marcie
• Please include the information about your platform (Mac OS X, Linux) and Marcie build details