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