关系动作基：形式化、有效安全性验证与不变量（扩展版）

在人工智能、业务流程管理与数据库理论中，对基于状态关系表示运行的动态系统进行建模与验证是日益受到关注的问题。为使这些系统可被验证，需限制每个关系状态所存储的信息量，或对动作的先决条件与效果施加约束。我们引入了关系动作基（RABs）这一通用框架，通过解除上述两类限制对现有模型进行了推广：无界关系状态可通过能对数据施加存在性与全称量化、并利用带算术谓词的数值数据类型的动作进行演化。随后，我们通过（近似的）基于 SMT 的反向搜索研究 RABs 的参数化安全性，提炼出该过程的基本元属性，并展示如何借助前沿 MCMT 模型检测器中现有验证模块的现成组合来实现它。我们在一组具有数据感知能力的业务流程基准上证明了该方法的有效性。最后，我们展示了如何利用全称不变量使该过程完全正确。