论文标题
关系行动基础：形式化，有效的安全验证和不变（扩展版）
Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)
论文作者
论文摘要
在AI，业务流程管理和数据库理论中，越来越多地研究了在国家关系代表方面运行的动态系统的建模和验证。为了使这些系统适合验证，需要对每个关系状态中存储的信息量进行界限，否则对动作的前提和影响施加了限制。我们介绍了关系行动基库（RABS）的一般框架，该框架通过抬高这两个限制来概括了现有模型：可以通过可以通过数据对数据量化和普遍普遍量化数据的行动来发展无限的关系状态，并且可以用Arithmetic Predicaties利用数值数据。然后，我们通过（近似）基于SMT的向后搜索来研究RABS的参数化安全性，挑选出所得过程的必需元概述，并展示如何通过最先进的ART MCMT模型检查器现有验证模块的现成验证模块的现成组合来实现它。我们证明了这种方法在数据感知业务流程的基准上的有效性。最后，我们展示了如何利用通用不变性以使此过程完全正确。
Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management, and Database Theory. To make these systems amenable to verification, the amount of information stored in each relational state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We introduce the general framework of relational action bases (RABs), which generalizes existing models by lifting both these restrictions: unbounded relational states can be evolved through actions that can quantify both existentially and universally over the data, and that can exploit numerical datatypes with arithmetic predicates. We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an off-the-shelf combination of existing verification modules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.
