Benchmark for Decomposition

This benchmark provides a set of 2800 random formulas over 14 models extracted from the BEEM benchmark (available at http://anna.fi.muni.cz/models/) which classifies all models into five categories (see Web Portal for Benchmarking Explicit Model Checker):

• Mutual exclusion
• Communication protocol
• Leader election algorithm
• Controller
• Puzzle, planning, scheduling

As we focus on the strength of SCCs the last category is not considered into this benchmark. The most representative category is Controller which provides complex SCCs structures. Nonetheless other categories are represented in this benchmark.

For all above models there are 100 verifed formulas and 100 violated ones. We use SPOT to generate formulas with the two following restrictions: the automaton of the formulas must have at least two distinct strength of SCC and the product must be greater than 2000 (in term of states).

Note that other LTL translator may produce different results (in term of SCC repartition for the properties automaton…

Here we propose to sum up chraracteristic of all SCCs of formulas model by model:

• # U.scc : the number of Non accepting SCCs
• # T.scc : the number of Terminal SCCs
• # W.scc : the number of Weak SCCs
• # S.scc : the number of Strong SCCs

The following table sump up these informations for all approaches in the paper:

Sec.3 of the paper presents results on a benchmark of 10 000 random formulas that can be found here.

The benchmark was realised in Explicit and Symbolic model checking using a patched version of Spot-9.2 and Ltl-Its.

A detailled csv about this experiment can be found here.