MARCIE - Model Checking and Reachability Analysis Done EffiCIEntly
Martin Schwarick, Monika Heiner, Christian Röhr · 2011
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.