Logo

software

data structures and software dependability

computer science department

brandenburg university of technology cottbus - senftenberg

M A R C I E

latest update: June 19, 2016, at 08:49 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

  • 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 modelssurprise modelsall models
state space
generation
(1 examination)
1 bronze medal1 silver medal1 silver medal
reachability
properties
(6 examinations)
2 bronze medal4 gold medal
1 silver medal
2 bronze medal
CTL
properties
(5 examinations)
1 bronze medal4 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

Download the manual (17.10.2013) as PDF.
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/os and linux (windows will follow) in the hope to be useful and with expectations of feedback.

Mac OSX 10.9+ (64bit)

Linux (64bit)

manual

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

Related Papers

  • [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 ] [ 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 ] [ 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 ]
  • [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

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 ] [ BibTeX ]

Bug Reports

Submit your bug reports and comments about Marcie here or contact marcie(at)informatik(dot)tu-cottbus(dot)de.

  • 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

… the end …

Any comments or questions are welcome. Please direct them to monika [period] heiner [snail] b-tu [period] de