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.

翻译：在人工智能、业务流程管理和数据库理论中，对基于关系状态表示进行操作的动态系统进行建模与验证日益成为研究热点。为了使这些系统适用于验证，需要对每个关系状态中存储的信息量进行限制，或对动作的前提条件和效果施加约束。我们提出了关系动作基（RAB）的通用框架，该框架通过同时解除这两类限制来泛化现有模型：允许通过动作演化无界关系状态，这些动作既可以对数据进行存在性量化也可以进行全称量化，并且可以利用带算术谓词的数值数据类型。随后，我们通过基于SMT（可满足性模理论）的（近似）反向搜索研究RAB的参数化安全性，提炼出该过程的关键元性质，并展示如何通过现成的组合方式，利用业界领先的MCMT模型检查器中已有的验证模块来实现该过程。我们在一组数据感知业务流程基准上证明了该方法的有效性。最后，我们展示了如何利用普适不变性使该过程达到完全正确。