fond
Model Checking Contest 2023
13th edition, Paris, France, April 26, 2023 (at TOOLympics II)
Complete Results for the 2023 Edition of the Model Checking Contest
Last Updated
May 14, 2023

1. Introduction

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

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

2. List of Qualified Tools in 2023

15 tools where submitted this year. They all successfully went through a qualification process requiring about 1625 runs (each tool had to answer each examination for the first instance of each «known» model).

We introduce two classes of tools :

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. Please note that one tool (with two variants) was out of competition this year: this was agreed between the tool developer and the organizers and is part of an experiment with precomputed deep-learning.

IMPORTANT: all tool developers agreed to provide the original image disk embedding the tool they submitted his year (see links in the table below). You may operate these tools on your own. To do so, you need the second disk image (mounted by the other one) that contains all models for 2023 together with the produced formulas. This image is mounted with the default configuration, as well as in he default disk image provided in the tool submission kit (see here).

IMPORTANT: You also have access to the archive containing all models and the corresponding formulas for 2023 here.

IMPORTANT: Note that Gold2022 is an hybrid artificial tool made with the tools that won categories in 2022. It correspond usually to several virtual machines, so the corresponding archive is a bit larger. For the MCC'2023, Gold 2022 is composed as follows:

The table below presents all participating tools for 2023.

Summary of the Participating Tools
Tool name Supported
Petri nets
Representative Author Origin Type of execution Link to the submitted disk image
Tools competing in 2023
Gold2022 P/T and colored Fabrice Kordon Aalborg/Paris/Toulouse Collateral Processing
GreatSPN-meddly P/T and colored Elvio Amparore Univ. Torino (Italy) Collateral Processing
LTSMin+red P/T and colored Yann Thierry-Mieg Univ. Twente (the Netherlands) & Sorbonne Université (France) (driver) Collateral Processing
LoLA+red P/T and colored Yann Thierry-Mieg Univ. Rostock (Germany) & Sorbonne Université (France) (driver) Collateral Processing
Marcie+red P/T and colored Yann Thierry-Mieg Univ. Cottbus (Germany) & Sorbonne Université (France) (driver) Collateral Processing
Smart+red P/T and colored Yann Thierry-Mieg Iowa State University (USA) & Sorbonne Université (France) (driver) Collateral Processing
TINA.tedd P/T and colored Bernard Berthomieu LAAS-CNRS (France) Collateral Processing
itstools P/T and colored Yann Thierry-Mieg Sorbonne Université (France) Collateral Processing
smpt P/T and colored Nicolas Amat LAAS-CNRS (France) Collateral Processing
tapaal P/T and colored Jiri Srba Aalborg University Collateral Processing
Reference Tools
LTSMin P/T and colored (unfolding by ITS) Jeroen Meijer and Tom van Dijk (2019) edited by Yann Thierry-Mieg Univ. Twente (the Netherlands) & Sorbonne Université (France) Collateral Processing
LoLA P/T and colored (unfolding by ITS on LTL/CTL) Karsten Wolf (2021) edited by Yann Thierry-Mieg Univ. Rostock (Germany) Collateral Processing
Marcie P/T and colored Christian Rohr (2017) edited by Yann Thierry-Mieg Univ. Cottbus (Germany) Sequential Processing
Smart P/T and colored (unfolding by ITS) Junaid Babar and Andrew Miner (2020) edited by Yann Thierry-Mieg Iowa state University (USA) Sequential Processing
pnmc P/T and colored Alexandre Hamez (2016) edited by Yann Thierry-Mieg Unaffiliated (France) Sequential Processing

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 GlobalProperties UpperBounds Reachability CTL LTL All together
Tools competing in 2023
Gold2022 COLLATERAL_PROCESSING DECISION_DIAGRAMS EXPLICIT IMPLICIT LATTICE_POINTS_COUNTING LINEAR_EQUATIONS STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE INVARIANTS LTSMIN MARKED_SUFFIX_TEST PARIKH_WALK PARTIAL_ORDER PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT TOPOLOGICAL USE_NUPN COLLATERAL_PROCESSING CPN_APPROX EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT COLLATERAL_PROCESSING CPN_APPROX CTL_CZERO EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT AUTOMATON_HEUR AUT_STUB COLLATERAL_PROCESSING DIST_HEUR EXPLICIT HEURISTIC LOGFIRECOUNT_HEUR(5000) LP_APPROX NDFS QUERY_REDUCTION RANDOM_HEUR SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN STUBBORN_SETS TARJAN UNFOLDING_TO_PT WEAK_SKIP AUTOMATON_HEUR AUT_STUB BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX CTL_CZERO DEADLOCK_TEST DECISION_DIAGRAMS DIST_HEUR EXHAUSTIVE_WALK EXPLICIT HEURISTIC IMPLICIT INITIAL_STATE INVARIANTS LATTICE_POINTS_COUNTING LINEAR_EQUATIONS LOGFIRECOUNT_HEUR(5000) LP_APPROX LTSMIN MARKED_SUFFIX_TEST NDFS OPTIM-1 PARIKH_WALK PARTIAL_ORDER PROBABILISTIC_WALK QUASILIVENESS_TEST QUERY_REDUCTION RANDOM_HEUR RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STATE_COMPRESSION STRUCTURAL STRUCTURAL_REDUCTION STUBBORN STUBBORN_SETS TARJAN TOPOLOGICAL TRACE_ABSTRACTION_REFINEMENT TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT USE_NUPN WEAK_SKIP
GreatSPN-meddly DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS PARALLEL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
LTSMin+red DECISION_DIAGRAMS PARALLEL_PROCESSING USE_NUPN BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARALLEL_PROCESSING PARIKH_WALK RANDOM_WALK SAT_SMT TOPOLOGICAL USE_NUPN BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE OVER_APPROXIMATION PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN BESTFIRST_WALK DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN INITIAL_STATE KNOWLEDGE LENGTHENING_INSENSITIVE REACHABILITY_KNOWLEDGE SHORTENING_INSENSITIVE STACK_TEST STUTTER_TEST TOPOLOGICAL BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SHORTENING_INSENSITIVE SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN
LoLA+red BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STATE_COMPRESSION STRUCTURAL STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK CPN_APPROX EXPLICIT INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN COLLATERAL_PROCESSING EXPLICIT INITIAL_STATE KNOWLEDGE LENGTHENING_INSENSITIVE REACHABILITY_KNOWLEDGE SHORTENING_INSENSITIVE STACK_TEST STATE_COMPRESSION STUBBORN_SETS STUTTER_TEST TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SHORTENING_INSENSITIVE SIPHON_TEST SKELETON_TEST STACK_TEST STATE_COMPRESSION STRUCTURAL STRUCTURAL_REDUCTION STUBBORN_SETS STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT USE_NUPN
Marcie+red DECISION_DIAGRAMS SEQUENTIAL_PROCESSING UNFOLDING_TO_PT BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT BESTFIRST_WALK DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT
Smart+red DECISION_DIAGRAMS IMPLICIT RELATIONS SEQUENTIAL_PROCESSING BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK IMPLICIT_RELATION INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SATURATION SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING TOPOLOGICAL BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STRUCTURAL_REDUCTION TOPOLOGICAL BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK IMPLICIT IMPLICIT_RELATION INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE RELATIONS SATURATION SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST
TINA.tedd COLLATERAL_PROCESSING DECISION_DIAGRAMS EXPLICIT LATTICE_POINTS_COUNTING LINEAR_EQUATIONS STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN COLLATERAL_PROCESSING DECISION_DIAGRAMS EXPLICIT LATTICE_POINTS_COUNTING LINEAR_EQUATIONS STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
itstools DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE INVARIANTS LTSMIN MARKED_SUFFIX_TEST PARIKH_WALK PARTIAL_ORDER PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT TOPOLOGICAL USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE LTSMIN OVER_APPROXIMATION PARIKH_WALK PARTIAL_ORDER PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS EXPLICIT HOA INITIAL_STATE KNOWLEDGE LENGTHENING_INSENSITIVE LTSMIN PARTIAL_ORDER REACHABILITY_KNOWLEDGE SAT_SMT SHORTENING_INSENSITIVE STACK_TEST STUTTER_TEST TOPOLOGICAL USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK EXPLICIT HOA INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE LTSMIN MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PARTIAL_ORDER PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SHORTENING_INSENSITIVE SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN
smpt BMC BULK COLLATERAL_PROCESSING COLORED_WALK COMPOUND DUPLICATE IMPLICIT INITIAL_MARKING K-INDUCTION NET_UNFOLDING PARIKH PDR_REACH_SATURATED PROJECTION SAT_SMT SKELETON SLICING STATE_EQUATION STRUCTURAL-REDUCTION STRUCTURAL_REDUCTION TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN WALK BMC BULK COLLATERAL_PROCESSING COLORED_WALK COMPOUND DUPLICATE IMPLICIT INITIAL_MARKING K-INDUCTION NET_UNFOLDING PARIKH PDR_REACH_SATURATED PROJECTION SAT_SMT SKELETON SLICING STATE_EQUATION STRUCTURAL-REDUCTION STRUCTURAL_REDUCTION TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN WALK
tapaal COLLATERAL_PROCESSING CPN_APPROX CTL_CZERO EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT SIPHON_TRAP STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT COLLATERAL_PROCESSING CPN_APPROX EXPLICIT QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TRACE_ABSTRACTION_REFINEMENT COLLATERAL_PROCESSING CPN_APPROX EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT COLLATERAL_PROCESSING CPN_APPROX CTL_CZERO EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT AUTOMATON_HEUR AUT_STUB COLLATERAL_PROCESSING DIST_HEUR EXPLICIT HEURISTIC LOGFIRECOUNT_HEUR(5000) LP_APPROX NDFS QUERY_REDUCTION RANDOM_HEUR SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN STUBBORN_SETS TARJAN UNFOLDING_TO_PT WEAK_SKIP AUTOMATON_HEUR AUT_STUB COLLATERAL_PROCESSING CPN_APPROX CTL_CZERO DIST_HEUR EXPLICIT HEURISTIC LOGFIRECOUNT_HEUR(5000) LP_APPROX NDFS OPTIM-1 QUERY_REDUCTION RANDOM_HEUR SAT_SMT SIPHON_TRAP STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN STUBBORN_SETS TARJAN TOPOLOGICAL TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT WEAK_SKIP
Reference Tools
LTSMin DECISION_DIAGRAMS PARALLEL_PROCESSING USE_NUPN Participates in ReachabilityDeadlock only so not listed in the category : BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARALLEL_PROCESSING PARIKH_WALK RANDOM_WALK SAT_SMT TOPOLOGICAL USE_NUPN BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE OVER_APPROXIMATION PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN BESTFIRST_WALK DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN INITIAL_STATE KNOWLEDGE LENGTHENING_INSENSITIVE REACHABILITY_KNOWLEDGE SHORTENING_INSENSITIVE STACK_TEST STUTTER_TEST TOPOLOGICAL BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARALLEL_PROCESSING PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SHORTENING_INSENSITIVE SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST USE_NUPN
LoLA BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STATE_COMPRESSION STRUCTURAL STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK CPN_APPROX EXPLICIT INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN COLLATERAL_PROCESSING EXPLICIT INITIAL_STATE KNOWLEDGE LENGTHENING_INSENSITIVE REACHABILITY_KNOWLEDGE SHORTENING_INSENSITIVE STACK_TEST STATE_COMPRESSION STUBBORN_SETS STUTTER_TEST TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BESTFIRST_WALK COLLATERAL_PROCESSING CPN_APPROX DEADLOCK_TEST EXHAUSTIVE_WALK EXPLICIT INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SHORTENING_INSENSITIVE SIPHON_TEST SKELETON_TEST STACK_TEST STATE_COMPRESSION STRUCTURAL STRUCTURAL_REDUCTION STUBBORN_SETS STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT USE_NUPN
Marcie DECISION_DIAGRAMS SEQUENTIAL_PROCESSING UNFOLDING_TO_PT Participates in ReachabilityDeadlock only so not listed in the category : BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT
BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING TOPOLOGICAL UNFOLDING_TO_PT BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT BESTFIRST_WALK DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST UNFOLDING_TO_PT
Smart DECISION_DIAGRAMS IMPLICIT RELATIONS SEQUENTIAL_PROCESSING BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK IMPLICIT_RELATION INITIAL_STATE INVARIANTS MARKED_SUFFIX_TEST PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK SATURATION SAT_SMT SCC_TEST SIPHON_TEST SKELETON_TEST STRUCTURAL STRUCTURAL_REDUCTION TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS INITIAL_STATE PARIKH_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING TOPOLOGICAL BESTFIRST_WALK CPN_APPROX DECISION_DIAGRAMS EXHAUSTIVE_WALK INITIAL_STATE OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK RANDOM_WALK SAT_SMT SEQUENTIAL_PROCESSING STRUCTURAL_REDUCTION TOPOLOGICAL BESTFIRST_WALK CPN_APPROX DEADLOCK_TEST DECISION_DIAGRAMS EXHAUSTIVE_WALK IMPLICIT IMPLICIT_RELATION INITIAL_STATE INVARIANTS KNOWLEDGE LENGTHENING_INSENSITIVE MARKED_SUFFIX_TEST OVER_APPROXIMATION PARIKH_WALK PROBABILISTIC_WALK QUASILIVENESS_TEST RANDOM_WALK REACHABILITY_KNOWLEDGE RELATIONS SATURATION SAT_SMT SCC_TEST SEQUENTIAL_PROCESSING SIPHON_TEST SKELETON_TEST STACK_TEST STRUCTURAL STRUCTURAL_REDUCTION STUTTER_TEST TOPOLOGICAL TRIVIAL_UNMARKED_SCC_TEST
pnmc DECISION_DIAGRAMS SEQUENTIAL_PROCESSING USE_NUPN DECISION_DIAGRAMS SEQUENTIAL_PROCESSING USE_NUPN

3. Experimental Conditions of the MCC'2023

Each tool was submitted to 21 814 executions in various conditions (1 678 model/instances and 13 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 168 168 runs (execution of one examination by the virtual machine) generated 29 GB 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. This year, we affected only physical cores to the virtual machines (discarding logical cores obtained from hyper-threading) so the balance between the various machine we used is quite different from he one of past years.

Involved Machines and Execution of the Benchmarks
  tall Small Octoginta-2 Tajo Total
Physical Cores 13×32 @ 2.1GHz 23×12 @ 2.4GHz 80 @ 2.4GHz 96 @ 2.40GHz
Memory (GB) 12×384 9×64 1536 2048
Used Cores (sequential tools) 12×31,
12×31 VM in //
9×3,
9×3 VM in //
79,
79 VM in //
95,
95 VM in //
Used Cores (parallel tools) 11×28 (4 per VM),
11×7 VM in //
9×8 (4 per VM),
9×2 VM in //
76 (4 per VM),
19 VM in //
92 (4 per VM),
23 VM in //
Number of runs 162 435 95 550 37 050 32 175 327 210
Total CPU consumed 2 875d, 1h, 0m, 54s 1 455d, 4h, 11m, 35s 645d, 21h, 51m, 2s 660d, 1h, 37m, 10s 5 635d, 4h, 40m, 41s
Total CPU about 15 years, 5 months and 9 days
Time spent to complete benchmarks about 25 days
Estimated boot time of VMs +
management (overhead)
about 17d (Included in total CPU) so ≅ 3.0 ‰ overhead

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

4. The Results of the MCC’2023

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

Details about the Examinations in the MCC (part I):
Details about Results and Scoring + Model Performance Charts
   Details about Results 
and Scoring
 Model Performance 
Charts
 Tool Resource 
consumption
StateSpace
ReachabilityDeadlock (GlobalProperties)
QuasiLiveness (GlobalProperties)
StableMarking (GlobalProperties)
Liveness (GlobalProperties)
OneSafe (GlobalProperties)
UpperBounds
ReachabilityCardinality
ReachabilityFireability
CTLCardinality
CTLFireability
LTLCardinality
LTLFireability

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

Details about the examinations in the MCC’2023 (part II)
Tool Performance Charts
  All
 models 
«Surprise»
 models only 
«Known»
 models only 
Original Tools (or combinations)
2022-Gold
GreatSPN
ITS-Tools
LTSMin+red
LoLA+red
Marcie+red
Smart+red
Tapaal
smpt
tedd-c
Reference Tools
LTSMin
LoLA
Marcie
Smart
pnmc

You can download the full archive (7.9 GB compressed and 121 GB uncompressed) of the 327 210 runs processed to compute the results of the MCC'2023. 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 (please have a look on the READ_ME.txt file). You may get separately the two mostly interesting CSV files:

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

5. The Winners for the MCC'2023

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

To avoid a too large disparity between models with numerous instances and those with only one, a normalization was applied so that the score, for an examination and a model, varies between 102 and 221 points. Therefore, providing a correct value may brings a different number of points according to the considered model. A multiplier was applied depending to the model category:

Let us introduce two «special» tools:

5.1. Winners in the StateSpace Category

4 tools out of 6 participated in this examination (plus 4 reference). Results based on the scoring shown below is:

Then, tools rank in the following order: Marcie+Red (11 825 pts), Smart+red (10 853 pts), LTSMin+red (8 806 pts). The the Gold-medal of 2022 collected 16 632 pts. BVT-2023 (Best Virtual Tool) collected 17 354 pts and computed 61.77% of the total number of values in this category.





GreatSPN (fastest 340 times)


GreatSPN (less memory 375 times)


TINA.tedd (61.28% values computed)

Estimated Tool Confidence rate for StateSpace (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
Tools competing in 2023
GreatSPN 99.847% 3912 3918
ITS-Tools 99.930% 2870 2872
tedd-c 100.000% 4113 4113
LTSMin+red 100.000% 2048 2048
Marcie+red 100.000% 2841 2841
Smart+red 99.726% 2544 2551
2022-gold and BVT-2023
2022-gold 100.000% 4089 4089
BVT-2023 100.000% 4146 4146
Reference tools
LTSMin 100.000% 2189 2189
Marcie 100.000% 2700 2700
pnmc 100.000% 1908 1908
Smart 99.239% 2477 2496

Remarks about the StateSpace examination

Some detailed results state that marking ins infinite (use of the value «+Inf********»). There are some infinite models in our benchmark but our analysis tools have a constrains in the representation of very large state spaces which is the one of the Long_Long_Float Ada type (maximum value of 1.0E+4932). When watching the execution report of some tools, you can check weather «+Inf********» really means infinite or not.

5.2. Winners in the GlobalProperties Category

3 tools out of 7 participated in these examinations (ReachabilityDeadlock , QuasiLiveness, StableMarking, Liveness, OneSafe). Results based on the scoring shown below is:

Other tools (in the same family than ITS-Tools) rank in the following order: LoLA+red (107 384 pts), Marcie+red (105 084 pts), Smart+red (102 776 pts). The the Gold-medal of 2022 collected 93 632 pts. BVT-2023 (Best Virtual Tool) collected 111 287 pts and computed 94.42% of the total number of values in this category. Please note that both LTSMin and Marcie information are not provided because they only compute ReachabilityDeadlock (20% of the total examinations in this family) ; howewer, results for ReachabilityDeadlock for these tools can be viewed here.





Tapaal (fastest 739 times)


Tapaal (less memory 4 493 times)


ITS-Tools (93.86% values computed)

Estimated Tool Confidence rate for GlobalPropertiesScores (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
Tools competing in 2023
GreatSPN 100.000% 4339 4339
ITS-Tools 100.000% 7875 7875
Tapaal 99.727% 6930 6949
LoLa+red 99.987% 7866 7867
LTSMin+red 100.000% 7725 7725
Marcie+red 100.000% 7729 7729
Smart+red 99.282% 7742 7798
2022-gold and BVT-2023
2022-gold 99.949% 7807 7811
BVT-2023 100.000% 7922 7922
Reference tools
LoLa 99.680% 7154 7177
Smart 97.514% 2079 2132

5.3. Winners in the UpperBounds Category

3 tools out of 7 participated in this examination. Results based on the scoring shown below is:

Other tools (in the same family than ITS-Tools) rank in the following order: Marcie+red (21 782 pts), Smart+red (21 270 pts), LTSMin+red (20 974 pts) and Lola+red (20 746). Then, the Gold-medal of 2022 collected 19 535 pts. BVT (Best Virtual Tool) collected 22 263 points and computed 93.32% of the total number of values in this category.





Tapaal (fastest 91 times)


Tapaal (less memory 338 times)


ITS-Tools (93.16% values computed)

Estimated Tool Confidence rate for UpperBound (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
Tools competing in 2023
GreatSPN 100.000% 14955 14955
Tapaal 100.000% 23163 23163
ITS-Tools 99.992% 25011 25013
LoLa+red 100.000% 24806 24806
LTSMin+red 100.000% 24830 24830
Marcie+red 100.000% 24955 24955
Smart+red 100.000% 24892 24892
2022-gold and BVT-2023
2022-gold 99.988% 24750 24753
BVT-2023 100.000% 25054 25054
Reference tools
LoLa 100.000% 22542 22542
LTSMin 100.000% 11888 11888
Marcie 100.000% 10900 10900
Smart 99.493% 9803 9853

5.4. Winners in the Reachability Formulas Category

4 tools out of 7 participated in these examinations (ReachabilityCardinality and ReachabilityFireability). Results based on the scoring shown below is:

Other tools (in the same family than Lola+red) rank in the following order: ITS-Tools (44 340 pts), Marcie+red (44 115 pts), LTSMin+red (43 753 pts) and Smart+red (43 134). GreatSPN got 31 116 pts. Then, the Gold-medal of 2022 collected 44 009 pts. BVT (Best Virtual Tool) collected 45 965 points and computed 96.21% of the total number of values in this category.





Tapaal (fastest 491 times)


Tapaal (less memory 1 257 times)


Lola+red (95.12% values computed)

Estimated Tool Confidence rate for Reachability (based on the «significant values» computed by tools)
see section 6. for details
Tools competing in 2023
GreatSPN 100.000% 22934 22934
ITS-Tools 99.996% 50573 50575
smpt 99.998% 49838 49839
Tapaal 100.000% 50184 50184
LoLa+red 100.000% 51078 51078
LTSMin+red 100.000% 50046 50046
Marcie+red 100.000% 50152 50152
Smart+red 99.944% 49764 49792
2022-gold and BVT-2023
2022-gold 100.000% 50002 50002
BVT-2023 100.000% 51659 51659
Reference tools
LoLa 99.977% 43920 43930
LTSMin 100.000% 24853 24853
Marcie 100.000% 18494 18494
Smart 99.822% 17969 18001

5.5. Winners in the CTL Formulas Category

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

Other tools (in the same family than LoLA+red) rank in the following order: ITS-Tools (26 417 pts), Marcie+red (25 647 pts), LTSMin+red (20 925 pts). Then, the Gold-medal of 2022 collected 34 428 pts. BVT (Best Virtual Tool) collected 40 899 points and computed 68.67% of the total number of values in this category.





GreatSPN (fastest 392 times)


GreatSPN (less memory 412 times)


Tapaal (64.72% values computed)

Estimated Tool Confidence rate for CTL (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
Tools competing in 2023
GreatSPN 100.000% 20690 20690
ITS-Tools 99.996% 28307 28308
Tapaal 99.963% 34751 34764
LoLa+red 99.985% 32914 32919
LTSMin+red 99.996% 22955 22956
Marcie+red 99.969% 25756 25764
2022-gold and BVT-2023
2022-gold 99.962% 34451 34464
BVT-2023 100.000% 36873 36873
Reference tools
LoLa 99.952% 29140 29154
LTSMin 99.918% 13444 13455
Marcie 99.981% 16071 16074

5.6. Winners in the LTL Formulas Category

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

Other tools (in the same family than ITS-Tools) rank in the following order: Lola+red (44 139 pts), LTSMin+red (42 121 pts). Then, the Gold-medal of 2022 collected 44 227 pts. BVT (Best Virtual Tool) collected 45 663 points and computed 91.56% of the total number of values in this category.





Tapaal (fastest 537 times)


Tapaal (less memory 603 times)


Tapaal (91.13% values computed)

Estimated Tool Confidence rate for LTL (based on the «significant values» computed by tools)
see section 6. for details
Tools competing in 2023
GreatSPN 98.145% 22068 22485
ITS-Tools 99.994% 48856 48859
Tapaal 100.000% 48932 48932
LoLa+red 100.000% 48549 48549
LTSMin+red 100.000% 46347 46347
Marcie+red 100.000% 18780 18780
Smart+red 100.000% 18903 18903
2022-gold and BVT-2023
2022-gold 100.000% 49028 49028
BVT-2023 100.000% 49162 49162
Reference tools
LoLa 99.961% 41216 41232

6. Estimation of the Global Tool Confidence

A confidence analysis enforces 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 hey provide for such values. This ratio gave us a tool confidence rate 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 examinations (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
Tools competing in 2023
GreatSPN 99.526% 88898 89321 13 StateSpace, UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
ITS-Tools 99.994% 163492 163502 13 StateSpace, UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
smpt 99.998% 49838 49839 2 LTLCardinality, LTLFireability
Tapaal 99.980% 163960 163992 12 UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
tedd-c 100.000% 4113 4113 1StateSpace
LoLa+red 99.996% 165213 165219 12 UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
LTSMin+red 99.999% 153951 153952 13 StateSpace, UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
Marcie+red 99.994% 130213 130221 13 StateSpace, UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
Smart+red 99.912% 103845 103936 11 StateSpace, UpperBounds, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
2022-gold and BVT-2023
2022-gold 99.988% 170127 170147 13 StateSpace, UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
BVT-2023 100.000% 174816 174816 13 StateSpace, UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
Reference tools
LoLa 99.956% 143972 144035 12 UpperBounds, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe
LTSMin 99.977% 53102 53114 7 StateSpace, UpperBounds, CTLCardinality, CTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock
Marcie 99.994% 48788 48791 7 StateSpace, UpperBounds, CTLCardinality, CTLFireability, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock
pnmc 100.000% 1908 1908 1 StateSpace
Smart 99.526% 32328 32482 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityFireability, ReachabilityDeadlock, QuasiLiveness, StableMarking, Liveness, OneSafe