data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

MC2 - Monte Carlo Model Checker

author: Robin Donaldson

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

• News
• Downloads
• General Description
• Installation
• Related Papers
• Related Tools
• Bug Reports

News

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

Downloads

• MC2.jar - all platforms
• MC2-Manual.pdf

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;

Installation

• 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
  • Snoopy
  • Spike

Bug Reports

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