ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources

This report presents the results from the 2022 friendly competition in the ARCH workshop for the falsification of temporal logic specifications over Cyber-Physical Systems. We briefly describe the competition settings, which have been inherited and adapted from the previous years, give background on the participating teams and tools, and discuss the selected benchmarks. In this year’s competition, in addition to the result validation introduced in the previous year, we change the experimental settings for a better account of the difficulty of benchmarks and for a better comparability between the tools.

There are three files. The data submitted by the participants is stored in the results archive. The validator infrastructure is stored in validation and the produced validation report is stored in report.

To re-run the validation on Linux with a somewhat recent MATLAB installation, unpack the first two archives in the same directory. Make sure that the models folder from https://gitlab.com/goranf/ARCH-COMP is available at relative path ../../models/ which you can check by:

ls ../../models
ls validation/falstar.sh

To run validation, proceed as follows

cd validation
./falstar-config.sh # once
./falstar.sh validate-$TOOL.cfg

where $TOOL is the name of one of the tools such that the corresponding configuration file exists.

If there are open issues, please contact Gidon Ernst

本报告呈现了2022年ARCH研讨会（ARCH workshop）中，针对信息物理系统（Cyber-Physical Systems）时序逻辑规范证伪的友好竞赛成果。本文简要介绍了延续并优化自往届的竞赛规则设置，阐述参赛团队与参赛工具的背景信息，并讨论本次竞赛选定的基准测试集。在本届竞赛中，除保留往届引入的结果验证环节外，我们对实验设置作出调整，以更合理地体现基准测试的难度，并提升不同工具间的可比较性。

本次竞赛数据集包含三类文件：参赛者提交的参赛数据存储于results归档包中，验证器基础设施存放于validation文件夹，生成的验证报告则存储于report文件夹。

若需在搭载版本较新的MATLAB的Linux系统中重新运行验证流程，请将前两个归档包解压至同一目录下。请确保从https://gitlab.com/goranf/ARCH-COMP 获取的models文件夹可通过相对路径../../models/访问，可通过以下命令进行验证：
ls ../../models
ls validation/falstar.sh

执行验证的流程如下：
cd validation
./falstar-config.sh # 仅需执行一次
./falstar.sh validate-$TOOL.cfg
其中$TOOL为参赛工具的名称，且需存在对应配置文件。

若存在未解决的问题，请联系吉登·恩斯特（Gidon Ernst）