Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Rules of the Model Checking Contest
Last Updated
Apr. 26, 2013

Rules for Publication and Participation

R01: Only the developers of a tool (or a tool extension) can participate with their own work.

R02: Computation must be effectively performed, precomputed results cannot be accepted unless for parts specified in the examination.

R03: Life cycle of the virtual machine is limited to an instance of a particular model.

R04: Each examination must be computed independently, i.e. without using previous results of an earlier computation. When a file contains several formulas, then computation for the evaluation of a formula can be reused for another one.

Rules for Formalisms and Models

R05: The contest is primarily dedicated to petri nets but not closed to other notations for concurrency. However, since the input format provided concerns Petri nets only, it is required that the correspondence in the other formalisms are Kripke equivalent. This can be checked since we provide a dummy tool that shows the number of states for the first scaling value of most models.

R06: PNML is the input format for Petri nets but you may enrich the disk image with a representation more suitable for your tool.

R07: To participate to "surprise models", tools must read the PNML format that will be provided in input.

Rules for Computing Results

R08: Tools must be freely available for the PC members of the contest (at least as an academic license).

R09: Participants authorize result publication, on the web site and on the resulting publication. Additional comments from the authors on the results are encouraged and expected.

R10: Participation can be done only on a part of the tests (state space generation, some types of formulas) or only on a part of the models. Then, the tool must provide an explicit answer (see the Submission Manual).

R11: For colored models, tools may either choose the colored version or the equivalent P/T version. This choice must be the same for all the instances of a given model.

R12: Participants are providing sources or binaries for the benchmark in a disk-image to be used in a Virtual Machine. Benchmark characteristics and instructions are communicated by the organizers as precisely as possible (see the Submission Manual).

R13: Result obtained by the benchmark computers are communicated as early as possible for detection and correction of possible problems.

R14: Tool can exploit structural properties of a model only when they are provided. Otherwise, you cannot consider them as being precomputed and must compute them online to integrate this computation in the process of model checking.

R15: Organizers make all their possible to select the "push-button model" to evaluate the push-button mode at the very last minute, when all tool are already submitted. This, in order to be sure that no participant might be advantaged.

Rules for Litigious Situations

R16: Only basic explanations of the used techniques are expected, for more detail use bibliographical references.

R17: In case of technical problems, participants and organizers communicate to solve the problems.

R18: Litigious situation are transmitted to the organizer who tries to solve the problems, no other entities can solve the complaints.

R19: Withdrawal of a participant by the organizers at any moment is possible in case of not respecting the present rules.

R20: A participant can resign at any moment, it will be completely removed from the record of the contest.