1. Introduction

This page summarizes the results for the 2016 edition of the Model Checking Contest (MCC’2016). This page is divided in three sections:

• First, we list the qualified tools for the MCC'2016,
• Then, we provide some informations about the experimental conditions of the MCC'2016,
• Then, we present an access to details about results,
• Then, we provide the list of winners of the MCC'2016,
• Finally, we provide an attempt to evaluate tool reliability based on the comparison of the results provided in the contest.

IMPORTANT:all these documents can be reused in scientific material and papers but must respect the Creative Common licence CC-BY-NC-SA.

2. List of Qualified Tools in 2016

Ten tools where submitted this year. They all successfully went through a qualification process requiring a total number of more than 25000 runs (each tool had to answer each examination for the first instance of each «known» model).

Data about these tools are summarized in the table below. For any tool, you can download the disk image that was provided with all its data. You may use these to reproduce measures locally and perform comparison with your own tool on the same benchmark.

Summary of the Participating Tools (alphabetical order)
Tool name	Representative Author	Origin	Type of execution	Link to the submitted disk image	Reported Techniques (all examinations)
ITS-Tools	Y. Thierry-Mieg	Univ. P. & M. Curie (France)	Parallel (collateral processing)		DECISION_DIAGRAMS SAT_SMT INITIAL_STATE TOPOLOGICAL USE_NUPN
LoLA	K. Wolf	Univ. Rostock (Germany)	Sequential		EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL
LTSMin	J. Meijer and J. van de Pol	Univ. Twente (Netherlands)	Parallel (parallel processing)		DECISION_DIAGRAMS EXPLICIT STATIC_VARIABLE_REORDERING USE_NUPN
Marcie	C. Rohr and M. Heiner	Univ. Cottbus (Germany)	Sequential		DECISION_DIAGRAMS UNFOLDING_TO_PT
PeCan	G. Trịnh	Ho Chi Minh Univ. of technology (Vietnâm)	Sequential		EXPLICIT
pnmc	A. Hamez	Steery.io (France)	Sequential		DECISION_DIAGRAMS USE_NUPN
PNXDD	E. Paviot-Adet	Univ. P. & M. Curie (France)	Sequential		DECISION_DIAGRAMS TOPOLOGICAL
smart	G. Ciardo and A. Miner	Iowa State University (USA)	Sequential		DECISION_DIAGRAMS
TAPAAL	J. Srba	Univ. Aalborg (Denmark)	3 variants (2 sequential, 1 with parallel processing)	or	COMPRESSION EXPLICIT STATE_COMPRESSION STATE_EQUATIONS STRUCTURAL_REDUCTION (all versions)
ydd-pt	D. Racordon	Univ. Geneva (Switzerland)	Sequential		DECISION_DIAGRAMS

The table below lists the techniques reported per examination (and for all the tool variants when applicable).

Techniques Reported by the Participating Tools (per examination)
Tool name	StateSpace	UpperBounds	Reachability	CTL	LTL
ITS-Tools	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS TOPOLOGICAL	COLLATERAL_PROCESSING DECISION_DIAGRAMS INITIAL_STATE TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN
LoLA	-	EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL	EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL	EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL	EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL
LTSMin	DECISION_DIAGRAMS USE_NUPN STATIC_VARIABLE_REORDERING	-	DECISION_DIAGRAMS USE_NUPN STATIC_VARIABLE_REORDERING	DECISION_DIAGRAMS USE_NUPN STATIC_VARIABLE_REORDERING	EXPLICIT USE_NUPN STATIC_VARIABLE_REORDERING
Marcie	DECISION_DIAGRAMS UNFOLDING_TO_PT	DECISION_DIAGRAMS UNFOLDING_TO_PT	DECISION_DIAGRAMS UNFOLDING_TO_PT	DECISION_DIAGRAMS UNFOLDING_TO_PT	-
PeCan			EXPLICIT		EXPLICIT
pnmc	DECISION_DIAGRAMS USE_NUPN	-	-	-	-
PNXDD	DECISION_DIAGRAMS TOPOLOGICAL	-	-	-	-
smart	DECISION_DIAGRAMS	-	-	-	-
TAPAAL (exp)	EXPLICIT STRUCTURAL_REDUCTION STATE_COMPRESSION	EXPLICIT STRUCTURAL_REDUCTION STATE_COMPRESSION	EXPLICIT STRUCTURAL_REDUCTION STATE_COMPRESSION	-	-
TAPAAL (par)	EXPLICIT	EXPLICIT STRUCTURAL_REDUCTION	EXPLICIT STRUCTURAL_REDUCTION	EXPLICIT COMPRESSION	-
TAPAAL (seq)	EXPLICIT	EXPLICIT STRUCTURAL_REDUCTION	EXPLICIT STRUCTURAL_REDUCTION	EXPLICIT	-
ydd-pt	DECISION_DIAGRAMS	-	-	-	-

3. Experimental Conditions of the MCC'2016

Each tool was submitted to 10701 executions in various conditions (1189 model/instances and 9 examinations per model/instance) for which it could report: DNC (do not compete), CC (cannot compute) or the result of the query. These executions were handled by BenchKit, that was developed in the context of the MCC for massive testing of software. Then, from the raw data provided by BenchKit, some post-analysis scripts consolidated these and computed a ranking.

16 GB of memory were allocated to each virtual machine (both parallel and sequential tools) and a confinement of one hour was considered (execution aborted after one hour). So, a total of 128 682 runs (execution of one examination by the virtual machine) generated 24 Gbyte of raw data (essentially log files and CSV of sampled data)

The table below shows some data about the involved machines and their contribution to the computation of these results.

We are please to thanks those who helped in the execution of tools:

• Bluewhale03 was made available by colleagues at Université de Genève,
• Ebro was made available by colleagues at Rostock University,
• Quadhexa-2 was made available by colleagues at Université Paris Ouest Nanterre La Défense,
• Small is one of the two clusters at LI6 (we got 11 nodes our of 23 there) Université Pierre & Marie Curie.

4. The Results of the MCC’2016

This First table below presents detailed results about the MCC'2016.

This Second table below presents some performance analysis related to tools during the MCC'2016.

You can download the full archive (3.6 GB compressed and 32 GB uncompressed) of the 128 682 runs processed to compute the results of the MCC'2016. This archive contains execution traces, execution logs and sampling, as well as a large CSV files that summarizes all the executions and gnuplot scripts and data to generate the charts produced in the web site. Yo may get separately the two mostly interesting CSV files:

• GlobalSummary.csv that summarizes all results from all runs in the contest (20 MB when expanded),
• raw-result-analysis.csv that contains the same data as the previous one but enriched with scoring information and the expected results (computed as a majority of tools pondered by their confidence rate, 27 MB when expanded).

Note that from the two CSV file, you can identify the unique run identifier that allors you to find the traces and any information in the archive (theyr are also available on the web site when the too did participated).

5. The Winners for the MCC'2016

This section presents the results for the main examinations that are:

• State Space generation,
• UpperBounds computation,
• Reachability Formulas (ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability),
• CTL Formulas (CTLCardinality, CTLFireability),
• LTL Formulas (LTLCardinality, LTLFireability),

Each examination for a given model brought 16 points (see the details in the slides). A multiplier was applied depending to the model category:

• ×1 for «Known» models,
• ×3 for «Stripped» models,
• ×5 for «Surprise» models.

We manually detected a few values (3 or 4) for which apparently the majority of tools where wrong. However, this has only a minor impact on the scoring and could not change the order of tools for any category. A way to deal with such (rare) situations will be considered for the next edition.

Presented scores are dispatched over the three categories of models (yellow for «Known» models, blue for «Stripped» models and red for «Surprise» models). The maximum number of points that a tool could get for a given examination was:

• 8 400 for «Known» models (+ a maximum of 4 200 bonus points),
• 25 200 for «Stripped» models (+ a maximum of 12 600 bonus points),
• 11 120 for «Surprise» models (+ a maximum of 5 560 bonus points).

Note that bonuses are not always collected.

5.1. Winners in the StateSpace Category

This examination had the highest participation rate (10 tools out of 12). Results based on the scoring shown below is:

• ITS-Tools was ranked first,
• Marciewas ranked second,
• pnmcwas ranked third.

Note that all the variants of TAPAAL were considered as one tool with regards to the scoring (see rule E-4.5.).

5.2. Winners in the UpperBounds Category

6 (+1, see below) tools out of 12 participated in this examination. Results based on the scoring shown below is:

• Marcie was ranked first,
• LoLAwas ranked second,
• ITS-Toolswas ranked third.

Note that all the variants of TAPAAL were considered as one tool with regards to the scoring (see rule E-4.5.) . Ydd-pt seems to participate and get no score but these are two accidently "Cannot Compute" answers instead of "Do not compete" that fooled analysis scripts to state that Ydd-pt was participating

5.3. Winners in the Reachability Formulas Category

8 tools out of 12 participated in these examinations (ReachabilityDeadlock, ReachabilityCardinality and ReachabilityFireability). Results based on the scoring shown below is:

• LoLA was ranked first,
• TAPAALwas ranked second (the classic sequential version),
• ITS-Toolswas ranked third.

Note that all the variants of TAPAAL were considered as one tool with regards to the scoring (see rule E-4.5.). We also noted an interaction problem with PeCan. After discussing with the tool developers, it seems that the tool may answers some values in cases it should answer "Cannot compute", thus leading to this bad situation for which the internal engine seems innocent.

5.4. Winners in the CTL Formulas Category

5 tools out of 12 participated in these examinations (CTLCardinality and CTLFireability). Results based on the scoring shown below is:

• LoLA was ranked first,
• Tapaalwas ranked second (the sequential version),
• Marciewas ranked third.

We discovered that the parallel implementation of Tapaal used a compiler option that caused the tool to crash when run on machines different from the one used in the qualification round. This was mainly an issue for the CTL examinations and for Tapaal(PAR) that was withdrawn from the CTL examination competition.

5.5. Winners in the LTL Formulas Category

4 tools out of 12 participated in these examinations (LTLCardinality and LTLFireability). Results based on the scoring shown below is:

• LTSMin was ranked first,
• LoLAwas ranked second (the classic sequential version),
• ITS-Toolswas ranked third.

6. Estimation of Tool Confidence

As for last year, we tried to introduce some confidence analysis to enforce the computation of «right results» based on the answers of participating tools. To do so, we considered each value provided in the contest (a value is a partial result such as the result of a formula or a number provided for state space, bound computation, etc.). To do so, we processed as follows:

1. For each «line» (all tools for a given examination for a given instance), we selected all «significant values» where at least 3 tools do agree.
2. Based on this subset of values, we computed the ratio between the selected values for the tool and the number of good answers. This ratio gave us a tool confidence rate (called reliability rate last year) that is provided in the table below.
3. This tool confidence rate rate was then applied to compute the scores presented in the dedicated section.

The table below provides, in first column, the computed confidence rates (that are naturally lower for tools where a bug was detected). Then, the table provides the number of correct results (column 2) out of the number of «significant values» selected for the tool (column 3). The last column shows the number of examination (and their type) the tool was involved in.

Estimated Tool Confidence rate (based on the «significant values» computed by tools)
Tool name	Reliability	Correct Values	«significant values»	Involved Examinations
ITS-Tools	98,38 %	33 634	34 189	9 (StateSpace, UpperBounds, Reachability, CTL, LTL)
LoLA	99,22 %	41 011	41 335	8 (UpperBounds, Reachability, CTL, LTL)
LTSMin	99,98 %	34 902	34 910	8 (StateSpace, Reachability, CTL, LTL)
Marcie	99,99 %	27 361	27 364	7 (StateSpace, UpperBounds, Reachability, CTL)
PeCan	37,54 %	3 967	10 568	5 (Reachability, LTL)
pnmc	99,84 %	1 219	1 221	1 (StateSpace)
PNXDD	99,11 %	222	224	1 (StateSpace)
Smart	98,72 %	926	938	1 (StateSpace)
TAPAAL (EXP)	99,95 %	22 421	22 434	5 (StateSpace, UpperBounds, Reachability)
TAPAAL (PAR)	99,98 %	19 555	19 558	7 (StateSpace, UpperBounds, Reachability, CTL)
TAPAAL (SEQ)	99,97 %	30 130	30 140	7 (StateSpace, UpperBounds, Reachability, CTL)
ydd-pt	97,70 %	85	87	2 (StateSpace, UpperBounds)

This table raises some comments about PeCan for which the confidence rate is very low. After discussing with the tool developers, it seems that the tool may answers some values in cases it should answer "Cannot compute", thus leading to this bad situation for which the internal engine seems innocent.