# Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)

arXiv: https://arxiv.org/abs/2208.06377 · HTML: https://mlsanity.com/paper/2208.06377/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 44 references that are in the map.
- First posted on arXiv 12 Aug 2022.

## Builds on (most cited first, 10 of 10)

- [Bounded Situation Calculus Action Theories](https://mlsanity.com/paper/1509.02012/) (2015)
- [Description Logic Knowledge and Action Bases](https://mlsanity.com/paper/1402.0569/) (2014)
- [Petri Nets with Parameterised Data: Modelling and Verification (Extended Version)](https://mlsanity.com/paper/2006.06630/) (2020)
- [Verification of Agent-Based Artifact Systems](https://mlsanity.com/paper/1301.2678/) (2013)
- [Verification of Hierarchical Artifact Systems](https://mlsanity.com/paper/1604.00967/) (2016)
- [Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic](https://mlsanity.com/paper/2203.07982/) (2022)
- [VERIFAS: A Practical Verifier for Artifact Systems](https://mlsanity.com/paper/1705.10007/) (2017)
- [Combined Covers and Beth Definability (Extended Version)](https://mlsanity.com/paper/1911.07774/) (2019)
- [Lifted Model Checking for Relational MDPs](https://mlsanity.com/paper/2106.11735/) (2021)
- [Bounded Quantifier Instantiation for Checking Inductive Invariants](https://mlsanity.com/paper/1710.08668/) (2017)

## Abstract (arXiv)

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.