data structures and software dependability

computer science department

brandenburg university of technology cottbus - senftenberg

MC2 - Monte Carlo Model Checker

author: Robin Donaldson

latest update: November 03, 2020, at 12:56 PM

BTU Cottbus
(2) Munich; Germany
(2) Monmouth Junction; United States
(2) São José Dos Campos; Brazil
(1) Coimbra; Portugal
(1) Utrecht; Netherlands


  • 2020-10-30 MC2 is happy to join the PetriNuts platform


General Description

  • off-line Monte Carlo Model Checker for LTLc and PLTLc;
  • operates on stochastic, deterministic, and hybrid simulation traces or even wetlab data, given as CSV files;
  • in terms of Petri nets, these traces can represent place markings or transition rates, both uncoloured or coloured ones;


  • No installation required; runs on any machine where Java is installed

Related Papers

Introduction of PLTLc:

  • Donaldson, R. & Gilbert, D.:
    A model checking approach to the parameter estimation of biochemical pathways.
    in Proc. Computational Methods in Systems Biology (CMSB), Vol. LNCS/LNBI 5307, Springer 2008, pp. 269-287.

MC2 has been used in many case studies, including:

  • [GHGC19]
    D Gilbert, M Heiner, L Ghanbar and J Chodak:
    Spatial quorum sensing modelling using coloured hybrid Petri nets and simulative model checking;
    BMC Bioinformatics, 20(supplement 4), 2019 (accepted: July, 26 2018; published: April 2019). [ doi ] [ BibTeX ]
  • [GHJR17]
    D Gilbert, M Heiner, Y Jayaweera and C Rohr:
    Towards dynamic genome scale models;
    Briefings in Bioinformatics, 2017 (online: October 13, 2017). [ doi ] [ BibTeX ]
  • [LHY14]
    F Liu, M Heiner and M Yang:
    Modeling and analyzing biological systems using colored hierarchical Petri nets, illustrated by C. elegans vulval development;
    WSPC Journal of Biological Systems, 22(3):463–493, online May 2014. [ doi ] [ BibTeX ]
  • [HDG10]
    M Heiner, R Donaldson and D Gilbert:
    Petri Nets for Systems Biology;
    In Symbolic Systems Biology: Theory and Methods, (MS Iyengar, Ed.), Jones & Bartlett Learning, LCC, pages 61–97, 2010. [ url ] [ pdf ] [ BibTeX ]
  • [HLGM09]
    M Heiner, S Lehrack, D Gilbert and W Marwan:
    Extended Stochastic Petri Nets for Model-based Design of Wetlab Experiments;
    Transactions on Computational Systems Biology XI, 5750:138–163, 2009. [ url ] [ pdf ] [ doi ] [ BibTeX ]
  • [HGD08]
    M Heiner, D Gilbert and R Donaldson:
    Petri Nets for Systems and Synthetic Biology;
    In SFM 2008, (M Bernardo, P Degano and G Zavattaro, Eds.), Springer, pages 215–264, 2008. [ pdf ] [ doi ] [ BibTeX ]

Related Tools

  • MC2 expects simulation traces, which can, e.g., be created with

Bug Reports

Submit your bug reports and any comments about MC2 to david [period] gilbert [snail] brunel [period] ac [period] uk

… the end …

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