Generation of Minimum Tree-like Witnesses for Existential CTL

This artifact consists of the executable of the model checker <b>SMART</b>, the benchmark suite, and the original data presented in the TACAS 2018 conference paper, <i>Generation of Minimum Tree-like Witnesses for Existential CTL</i>. We compared the performance of our minimum witness generation approach and the traditional breadth-first approach. The results are reproducible.<br><br>The artifact is a single .zip archive holding script files, data and benchmarks in different subdirectories.<br><br>See the file HOW-TO for detailed guidance on running SMART for experiments of: <br> 1. EV+MDD (edge-valued multiway decision diagram)-based approach to generate minimum tree-like witnesses (<b>MinWit</b>), and<br> 2. traditional MDD (multiway decision diagram)-based BFS approach to generate (not necessarily minimum) tree-like witnesses (<b>Wit</b>).<br><br>The benchmarking suite consists of nine Petri net models from the 2017 Model Checking Contest (https://mcc.lip6.fr/2017/). <b>.sm</b> 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).<br><br><b>Background</b><br><br>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.<br>