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>本研究工件包含模型检查器（model checker）<b>SMART</b>的可执行文件、基准测试集，以及发表于TACAS 2018年会论文《面向存在性计算树逻辑的最小类树见证生成》<i>（Generation of Minimum Tree-like Witnesses for Existential CTL）</i>中的原始实验数据。本研究对比了我们的最小见证生成方法与传统广度优先方法的性能，且实验结果可复现。 本研究工件为单个.zip压缩包，内含不同子目录下的脚本文件、实验数据与基准测试集。 请参阅HOW-TO文件，获取针对以下两类实验运行<b>SMART</b>的详细操作指南：1. 基于边值多路决策图（edge-valued multiway decision diagram, EV+MDD）的最小类树见证生成方法（<b>MinWit</b>）；2. 基于多路决策图（multiway decision diagram, MDD）的传统广度优先搜索（breadth-first search, BFS）方法，用于生成（未必满足最小性要求的）类树见证（<b>Wit</b>）。 本基准测试集包含来自2017年模型检查竞赛（Model Checking Contest, MCC）的9个Petri网（Petri net）模型，竞赛官网链接为https://mcc.lip6.fr/2017/。<b>.sm</b>格式文件为从源PNML（Petri网标记语言，Petri Net Markup Language）文件自动转换得到的<b>SMART</b>格式文件。所有模型均配备一个或多个缩放参数，这些参数会影响状态数量、状态间转移的规模，进而决定模型的整体尺寸与复杂度。请参阅/data子目录，获取论文中呈现的实验数据集（具体公式详见所关联的TACAS论文的表1）。 <b>背景说明</b> 模型检查的核心优势之一在于其能够生成见证或反例。目前已有针对简单非嵌套逻辑公式生成小型或最小见证的方法，但尚无现有技术可保证通用嵌套逻辑公式对应的见证满足最小性要求。本数据记录所关联的相关论文首次给出了见证规模的明确定义，采用边值决策图递归计算每个子公式的最小见证规模，并提出了一种面向存在性计算树逻辑（Computation Tree Logic, CTL）构建最小类树见证的通用方法。