- This manual gives an overview on MARCIE – Model Checking And Reachability analysis done effiCIEntly. MARCIE was originally developed as a symbolic model checker for stochastic Petri nets, building on its predecessor – IDDMC – Interval Decision Diagram based Model Checking – which has been previously developed for the qualitative analysis of bounded Place/Transition nets extended by special arcs. Over the last years the tool has been enriched to allow also quantitative analysis of extended stochastic Petri nets. We concentrate here on the user viewpoint. For a detailed introduction to the relevant formalisms, formal definitions and algorithms we refer to related literature.
Keine Lizenz vergeben. Es gilt das deutsche Urheberrecht.
