The full archives with formulas can be found there.
Results for the MCC@Petri Net 2013
- The HTML report,
- The PDF report: it contains a main report (422 pages) and its associated annex 1 (1378 pages) and annex 2 (1732 pages), available at CoRR,
- The slides presented at Milano.
Objectives
When modeling a system with formal methods, such as Petri Nets, one may have several questions such as: "To verify highly concurrent systems, should we use a symmetry-based or a partial order-based model checker?" or "For models with large variable domains, should we use decision diagram-based, or a symmetry-based model checker?"
Results that help to answer these questions are spread among numerous papers in numerous conferences. Moreover, as benchmarks are executed over several platforms and composed of different models, conclusions are not easy.
The objective of the Model Checking Contest is to compare the efficiency of techniques according to characteristics of models. To do so, the Model Checking Contest compares tools on several classes of models with scaling capabilities (e.g. values that set up the "size" of its associated state space). Through the feedback on tools efficiency according to the selected benchmarks, we aim at identifying the techniques that can tackle a given type of problem identified in a "typical mode", for a given class of problem (e.g. state space generation, deadlock detection, reachability analysis, causal analysis).
After two editions in 2011 and 2012, this is the third one that will take place at PETRI NET 2013 in Milano.
Results from previous editions
- MCC'2011 @ Newcastle: slides - report (ToPnoC link)
- MCC'2012 @ Hamburg: slides - report (CoRR)
Types of Models
Several classes of models will be provided:
- Academic models: P/T Nets (1-bounded, k-bounded), and colored Nets (1 and k-bounded per color, with and without non-equal guards on transitions, with and without cartesian product on colors, with and without successor/predecessor functions) - for Colored nets, P/T equivalent nets will be provided,
- "Case studies" P/T Nets.
All models will be provided as PNML files. The two types of models will be provided with a detailed set of characteristics that tools can exploit when possible. For colored Nets, a P/T unfolded equivalent P/T net will be provided in most cases.
IMPORTANT: you may submit a tool that is not working on Petri nets provided the models in your formalism are Kripke equivalent to those of the Model Checking Contest.
Case studies are proposed to evaluate the possibilities of a tool in a "push-button" mode. Thus, they will not be known before submission time and, to participate, tools will have to parse the PNML format (for P/T nets only), PNML for colored nets will also be provided but this is not mandatory for tools to support it.
Examinations for Model Checkers
Several examinations are proposed:
- State Space Generation: tools will have to generate the state space and provide data on its size,
- Deadlock detection: tools will have to check if there is at least one deadlock in the system,
- Evaluation of reachability properties: tools will have to process verified and unverified reachability properties, stating for each one if it is verified or not,
- Evaluation of temporal logic properties: tools will have to process verified and unverified causal properties, stating for each one if it is verified or not.
Each examination will be processed for all the scaling values of benchmark models. CPU and memory consumption will be measured and reported. Formulae will be provided in a dedicated language for which a BNF in ANTLR format will be provided.
Tools will have to provide results as well as an identification of the techniques activated during their execution.
Steps of the Model Checking Contest
The Model Checking Contest will have several steps:
- Model submission: November 15, 2012
- Detailed Procedure and publication of models: mid March, 2013
- Call for Tool Submission:
May 1st, 2013May 6th, 2013 - Announcement of results: June 25, 2013