Title :
MARCIE - Model Checking and Reachability Analysis Done EffiCIEntly
Author :
Schwarick, Martin ; Heiner, Monika ; Rohr, Christian
Author_Institution :
Comput. Sci. Dept., BTU Cottbus, Cottbus, Germany
Abstract :
MARCIE is a multi-threaded tool for the analysis of Generalized Stochastic Petri Nets. Its capabilities range from standard properties of qualitative Petri nets to CTL and CSL model checking, recently extended by rewards. The core of MARCIE builds upon Interval Decision Diagrams for the symbolic representation of marking sets of bounded Petri nets (finite state space) and on-the-fly matrix computation for numerical analysis. Approximative engines supporting fast adaptive uniformization and Gillespie simulation open the door to quantitative reasoning on unbounded Petri nets (infinite state space). This paper presents MARCIE´s architecture and its most important distinguishing features. Extensive computational experiments demonstrate MARCIE´´s strength in comparison with related tools.
Keywords :
Petri nets; decision diagrams; formal verification; matrix algebra; reachability analysis; CSL model checking; CTL model checking; Gillespie simulation; MARCIE; Petri net marking set symbolic representation; adaptive uniformization; approximative engines; generalized stochastic Petri nets; interval decision diagrams; multithreaded tool; on-the-fly matrix computation; reachability analysis; Analytical models; Biological system modeling; Computational modeling; Engines; Numerical models; Petri nets; Stochastic processes; Computation Tree Logic; Continuous Stochastic Logic; Continuous Time Markov Chain; Fast Adaptive Uniformization; Generalized Stochastic Petri Net; Interval Decision Diagram; Model Checking; Rewards; Stochastic Simulation;
Conference_Titel :
Quantitative Evaluation of Systems (QEST), 2011 Eighth International Conference on
Conference_Location :
Aachen
Print_ISBN :
978-1-4577-0973-9
DOI :
10.1109/QEST.2011.19
