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>本附属数据集包含SMART模型检验器（model checker）的可执行文件、基准测试集，以及发表于TACAS 2018会议论文《面向存在计算树逻辑的最小类树见证生成（Generation of Minimum Tree-like Witnesses for Existential CTL）》中的原始数据。本研究对比了所提出的最小见证生成方法与传统广度优先方法的性能，实验结果可复现。 本附属数据集为单一ZIP压缩包，内含不同子目录下的脚本文件、实验数据与基准测试用例。 请参阅HOW-TO文件，获取针对以下两类实验运行SMART的详细指导： 1. 基于边值多路决策图（edge-valued multiway decision diagram, EV+MDD）的最小类树见证生成方法（下称**MinWit**）； 2. 基于传统多路决策图（multiway decision diagram, MDD）的广度优先搜索（BFS）方法，用于生成（未必最小的）类树见证（下称**Wit**）。 本次基准测试集包含9个取自2017年模型检验竞赛（https://mcc.lip6.fr/2017/）的Petri网（Petri net）模型。扩展名为.sm的文件为从源PNML（Petri网标记语言）文件自动转换得到的SMART格式文件。所有模型均带有一个或多个缩放参数，可影响状态数量、状态间转移数量，进而影响模型规模与复杂度。请访问/data子目录查看论文中用到的实验数据集（具体公式详见所附TACAS论文的表1）。 **背景** 模型检验（model checking）的优势之一在于其可生成见证或反例。现有方法可针对简单无嵌套公式生成小型或最小化见证，但尚无方法可保证通用嵌套公式的见证最小性。本数据集附带的相关论文给出了见证规模的定义，采用边值决策图递归计算每个子公式的最小见证规模，并提出了面向存在计算树逻辑（CTL）的通用最小类树见证构建方法。