Generation of Minimum Tree-like Witnesses for Existential CTL

This artifact consists of the executable of the model checker SMART, the benchmark suite, and the original data presented in the TACAS 2018 conference paper, Generation of Minimum Tree-like Witnesses for
Existential CTL. We compared the performance of our minimum witness generation approach and the traditional breadth-first approach. The results are reproducible.

The artifact is a single .zip archive holding script files, data and benchmarks in different subdirectories.

See the file HOW-TO for detailed guidance on
running SMART for experiments of:

1. EV+MDD (edge-valued multiway decision diagram)-based approach to generate
minimum tree-like witnesses (MinWit), and

2. traditional MDD (multiway decision diagram)-based BFS approach to generate
(not necessarily minimum) tree-like witnesses (Wit).

The benchmarking suite consists of nine Petri
net models from the 2017 Model Checking Contest (https://mcc.lip6.fr/2017/).
.sm files are SMART files automatically converted from source PNML
files. All models have one or more scaling parameters affecting the number of
states and state-to-state transitions, thus the model size and complexity. See
the subdirectory /data for datasets presented in the paper (the specific
formulas are listed in Table 1 of the linked TACAS paper).

Background

An advantage of model checking is its ability to generate witnesses or counterexamples. Approaches exist to generate small or minimum witnesses for simple unnested formulas, but no existing method guarantees minimality for general nested ones. The related paper linked from this data record provides a definition of witness size, uses edge-valued decision diagrams to recursively compute the minimum witness size for each subformula, and describes a general approach to build minimum tree-like witnesses for existential CTL.