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
- 51.7678,14.3253,ff0000
- BTU Cottbus
- 39.56449890136719,-75.59700012207031,6383cf
- (6) Wilmington; United States
- 41.900001525878906,12.48330020904541,6383cf
- (2) Rome; Italy
- -23.183300018310547,-45.88330078125,6383cf
- (2) São José Dos Campos; Brazil
- 49.75,6.633299827575684,6383cf
- (2) Trier; Germany
- 42.273399353027344,-83.71330261230469,6383cf
- (2) Ann Arbor; United States
- 33.80039978027344,-84.3864974975586,6383cf
- (2) Atlanta; United States
- 49.28329849243164,21.283300399780273,6383cf
- (2) Bardejov; Slovakia
- 48.11800003051758,11.661199569702148,6383cf
- (2) Munich; Germany
- 46.91669845581055,7.466700077056885,6383cf
- (2) Berne; Switzerland
- 40.39289855957031,-74.54119873046875,6383cf
- (2) Monmouth Junction; United States
- 51.516700744628906,-0.11670000106096268,6383cf
- (2) Bloomsbury; United Kingdom
- 37.789798736572266,-122.39420318603516,6383cf
- (2) San Francisco; United States
- 24.986900329589844,121.30560302734375,6383cf
- (2) Taoyüan; Taiwan
- 45.79999923706055,16,6383cf
- (1) Zagreb; Croatia
- 48.08330154418945,11.683300018310547,6383cf
- (1) Neubiberg; Germany
- 16.850000381469727,-99.91670227050781,6383cf
- (1) Acapulco; Mexico
- 49.48830032348633,8.464699745178223,6383cf
- (1) Mannheim; Germany
- 55.752201080322266,37.6156005859375,6383cf
- (1) Moscow; Russian Federation
- 52.08330154418945,5.133299827575684,6383cf
- (1) Utrecht; Netherlands
- 49.447200775146484,8.177200317382812,6383cf
- (1) Wachenheim; Germany
- 37.56639862060547,126.99970245361328,6383cf
- (1) Seoul; Korea, Republic of
- 40.084800720214844,-82.8125991821289,6383cf
- (1) New Albany; United States
- 50.86669921875,8.033300399780273,6383cf
- (1) Siegen; Germany
- 40.20000076293945,-8.41670036315918,6383cf
- (1) Coimbra; Portugal
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
Bug Reports
Submit your bug reports and any comments about MC2 to david [period] gilbert [snail] brunel [period] ac [period] uk