关系动作基础：形式化、有效的安全验证和不变量（扩展版）
摘要：对于使用关系表示的动态系统的建模和验证日益成为人工智能、业务流程管理和数据库理论等领域的研究问题。为了使这些系统便于验证，需要限制每个关系状态中存储的信息量，或者对动作的前提条件和效果施加限制。我们引入了关系动作基础（RABs）的通用框架，通过解除这些限制来推广现有的模型：无限制的关系状态可以通过可以对数据进行存在量词和普遍量词量化的动作进行演化，并且可以利用带有算术谓词的数值数据类型。然后，我们通过（近似的）基于SMT的向后搜索研究了RABs的参数化安全性，突出了所得到的过程的基本元属性，并展示了如何通过使用现有验证模块的最新状态MCMT模型检查器的组合来实现这个过程。我们通过对数据感知业务流程的基准测试证明了这种方法的有效性。最后，我们展示了如何利用普遍不变式使该过程完全正确。
作者：Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin
论文ID：2208.06377
分类：Artificial Intelligence
分类简称：cs.AI
提交时间：2023-08-14