Safety Verification and Universal Invariants for Relational Action Bases

1 Introduction

Reasoning about actions and processes has witnessed an important shift in the representation of states and the way actions query and progress them. Relational representations and query/update languages are often used in these systems as a convenient syntactic sugar to compactly represent and evolve propositional states - see, e.g., STRIPS planning. More recently, instead, several works have put emphasis on states captured by full-fledged relational structures, equipping dynamic systems with actions that can create and destroy objects and relations. This data-awareness is essential to capture relevant systems in AI [Baral and De Giacomo, 2015] and business process management [Vianu, 2009; Calvanese et al., 2013]. Notable examples are: (i) Situation Calculus [De Giacomo et al., 2016] and knowledge-based [Bagheri Hariri et al., 2013b] action theories, (ii) relational MDPs [Yang et al., 2022], (iii) data-/artifact-centric business processes [Bagheri Hariri et al., 2013a; Deutsch et al., 2016; Calvanese et al., 2019], and (iv) Petri nets with identifiers [Polyvyanyy et al., 2019; Ghilardi et al., 2022a] or with advanced interaction mechanisms [Fahland, 2019]. The subtle interplay between, data and processes calls for dedicated techniques for verifying at design-time whether such relational dynamic systems behave as expected [Baral and De Giacomo, 2015; Calvanese et al., 2013]. However, verification is extremely difficult, as relational dynamic systems induce infinite state-spaces. This poses two challenges: foundationally, the identification of interesting classes of systems for which suitable verification procedures enjoy key (meta-)properties like correctness and termination; practically, the development of corresponding efficient verification tools. Typically, this leads to data-aware dynamic systems severely controlling the expressiveness of the data component and/or of the way actions operate over data, resulting in decidable/tractable fragments that are however too restrictive in capturing real-life processes.

In this work, we follow a different route. Modeling-wise, we start from one of the most expressive data-aware process modeling frameworks existing in the literature [Calvanese et al., 2020], and we further enrich it with two essential features toward practical applicability. Such feature have never been combined in a unique formalism so far, and are arithmetics, to express conditions over and manipulate the content of numerical data values, and universally-quantified guards, to capture advanced forms of synchronization in concurrent and multi-agent systems and rich conditional updates in complex relational dynamic systems (see Section 2 for more details). While decidability does not hold in general for the resulting framework, we provide an algorithmic approach for verification that enjoys interesting meta-properties such (partial) soundness and completeness, and also demonstrate the benefit of injecting universal safety invariants to avoid spurious results. Computation-wise, we show that practical verification can be conducted through a careful combination of existing verification modules implemented in the MCTM model checker [Ghilardi and Ranise, 2010b]. We then demonstrate feasibility through an extensive experimental evaluation conducted on a suitably extended version of the only existing formal modeling and verification benchmark for data-aware processes [Gianola, 2022]. This extended version is of independent interest, as the research community lacks a comprehensive, shared collection of realistic data-aware process models. Notably, all examples in the benchmark specify the controlflow component of the process through the BPMN language, which is the de-facto standard for the representation of business processes.

Technical contributions. To attack the verification of relational dynamic systems, we start from RASs [Calvanese et al., 2020], one of the most expressive models in the literature. A RAS comes with (i) a read-only database with primary and foreign keys, (ii) a working memory consisting of read-write unbounded relations, and (iii) actions for constrained updates, whose preconditions query the working and read-only memory with existential queries, and whose effects consist in update formulae that can express addition, deletion, or bulk update of tuples in the read-write relations.

Our first contribution is to further push the boundaries of expressiveness of RASs, extending them with two genuinely novel essential features: universal guards and arithmetics. In the resulting framework of relational action bases (RABs), unbounded relational states are evolved through actions that quantify existentially and universally over the data, and that use numerical datatypes with arithmetic predicates (including linear arithmetics for integers and reals). As surveyed later, these features match needs in different application domains.

On top of this framework, we provide a threefold technical contribution. The first concerns algorithmic techniques for verification of RABs. Specifically, we build on the last version of the MCMT model checker [Ghilardi and Ranise, 2010b], a natural choice for two reasons. On the one hand, MCMT comes with an effective backward reachability procedure that handles the automated verification of safety properties over RASs, ascertained parametrically to the content of the read-only database [Calvanese et al., 2020; Calvanese et al., 2021]. On the other hand, MCMT includes two separate modules to respectively handle universal quantifiers via dynamic forms of instantiation [Alberti et al., 2012; Feldman et al., 2019], and deal with the elimination of data variables via cover computation [Calvanese et al., 2021], combined with quantifier elimination for arithmetics [Calvanese et al., 2022a]. While such modules were so far employed in isolation, we here show for the first time that they can be gracefully combined, both theoretically and practically, inside the backward search of MCMT, enabling verification of (parameterized) safety in the novel setting of RABs. This is surprising since these two techniques may appear to interfere with each other, while we show that they interact harmlessly. The integration of these two techniques results in two (over-)approximation steps in the symbolic computation of unsafe states, which could cause the resulting procedure to detect unsafety spuriously. We thus investigate meta-properties of the procedure; decidable cases for which termination is guaranteed are inherited from the RAS fragments from [Calvanese et al., 2020]. This shows that MCMT can handle RABs off-the-shelf, without destroying the metaproperties of the combined procedure.

As a second technical contribution, we put MCMT at work: we show that it terminates producing a correct answer with very good performance, on a set of 34 RABs that we derive from a benchmark of data-aware processes [Li et al., 2017].

Last, we study the injection on invariants in the safety analysis of RABs. We obtain the key result that under the existence of universal invariants, spurious results for unsafety are never produced. This requires to prove, using model theory, that the two approximation techniques do not interfere with each other, but again combine well. Notably, our invariance result is analogous, in spirit, to that in [Karbyshev et al., 2017], but substantially differs from the technical point of view: it holds for a different verification procedure and covers the whole expressiveness of RABs, out of reach so far.

The paper is organized as follows. In Section 2, we discuss the related work and the motivations for the need of new features of RABs. After the preliminaries, in Section 4 we introduce the general model of RABs and we describe an informative RAB example inspired by a process for evaluating visa applications, where we concretely present the novel modeling features. In Section 5, we introduce the SMT-based verification procedure for checking safety of RABs and we show its meta-properties. In Section 6, we prove how universal invariants can be exploited to avoid spurious unsafety outcomes, and in Section 7 we experimentally test our approach against the only existing verification benchmark for data-aware processes. We conclude in Section 8. Full proofs and details are provided in the online extended version [Ghilardi et al., 2022b].

2 Motivation and RelatedWork

We discuss related work with two goals: (i) motivate the need of arithmetics and universal quantification when modeling relational dynamic systems in different application domains; (ii) discuss how RABs relate to the state-of-the-art. As the importance of arithmetics is well-known (see, e.g., [Gerevini et al., 2008; Belardinelli, 2014; Deutsch et al., 2016; Felli et al., 2022]), we concentrate on universal quantification, discussing that it is essential to model the injection of fresh objects, capture conditional updates, deal with constraint checking, and capture synchronization in concurrent systems.

Injection of fresh objects. Relational dynamic systems need to create new, fresh objects during the execution. Classical examples are the creation of a new primary key within a database [Bagheri Hariri et al., 2013a; Belardinelli et al., 2014], or of a new identifier in a (high-level) Petri net [Polyvyanyy et al., 2019; Ghilardi et al., 2022a]. Without universal quantification, freshness cannot be guaranteed: it is possible to nondeterministically pick an object, but not to enforce that it is not contained in the working memory.

Conditional updates and constraint checking. Universal quantification is need to express rich conditional updates operating at once over the entire extension of a relation [Bagheri Hariri et al., 2013a; Belardinelli et al., 2014]. Conditional updates can also be used to enforce constraints on the working memory of the system, using the following modelling pattern. Considering the forms of actions supported by RABs, the constraint of interest can be formulated as a universally quantified sentence. The system alternates an action mode and a check mode. In the check mode, the system verifies whether the constraint holds. If so, the system goes back to the action mode. If not (i.e., the negation of the constraint holds), the system enters into an error state. Universally quantified sentences can express, key and disjointness constraints.

Universal synchronization. Dynamic systems with multiple concurrent entities call for synchronization mechanisms. Two key scenarios are (parameterized) multiagent systems, where all agents synchronously perform a joint action [Kouvaros and Lomuscio, 2016; Felli et al., 2020], and equality synchronization in proclets [Fahland, 2019], where a transition can be performed by a parent entity only if all its children are in a certain state (e.g., all same-order items have been validated). With universally quantified variables, RABs support such mechanisms, allowing for verification of proclets that has been out of reach [Fahland, 2019; Ghilardi et al., 2022a].

Related work. Verification of relational dynamic systems has been addressed along two main lines. In the first, a bound is imposed on the number of objects that can be stored in a single state. This makes verification for first-order µcalculus [Bagheri Hariri et al., 2014; Calvanese et al., 2018] and a fragment of first-order LTL [Calvanese et al., 2022b] reducible to finite-state model checking, for systems with a fixed initial state and objects only equipped with equality comparison. This carries over relational multiagent systems verified against epistemic first-order CTL [Belardinelli et al., 2014]. These techniques do not correspond to concrete verification tools, and only preliminary results exist on implementations [Yang et al., 2022].

The second line of research studies relational dynamic systems operating over a working memory that can contain unboundedly many objects per state, and accessing read-only data. Verification is studied parametrically to the read-only storage, ensuring that desired properties hold irrespectively of its content. This setting, surveyed in [Vianu, 2009], is more delicate than the one of state-bounded systems: the identification of verifiable fragments calls for a very careful analysis of modelling features supported in action specifications. At the same time, perhaps surprisingly, there are practical verifiers working with unbounded data, based on explicit-state model checking and vector addition systems [Li et al., 2017], or on symbolic model checking via SMT [Calvanese et al., 2019] implemented in a dedicated module of the MCMT model checker [Ghilardi and Ranise, 2010b]. Other SMTbased approaches dealing with universal quantification and parameterized verification, such as [Gurfinkel et al., 2016; Cimatti et al., 2021], cannot instead be readily applied, as they do not natively handle relational dynamic systems.

3 Preliminaries

We adopt the usual first-order syntactic notions of signature, term, formula, and the like. Signatures are multi-sorted. Every sort comes with equality. For simplicity, most definitions are given for single-sorted languages - the adaptation to multisorted is straightforward. Notation t(x) (resp., φ(x)) means that term t (resp., formula φ) has free variables included in x, where x represents a tuple 〈x1, . . . , xn〉 of variables. We assume that terms and formulae are well-typed. A formula is universal (resp., existential) if it has the form∀x(φ(x)) (resp.,

∃x(φ(x))), where φ is a quantifier-free formula. A sentence is a formula without free variables.

For semantics, we use the standard notions of Σ-structure M and of truth of a formula in a Σ-structure under a free variables assignment. A Σ-theory T is a set of Σ-sentences; a model of T is a Σ-structure M where all sentences in T are true. T |= φ expresses that φ is true in all models of T for every assignment to the variables occurring free in φ. φ is T-satisfiable iff there exists a model M of T and an assignment to the free variables of φ that makes φ true in M: if φ is quantifier-free, the problem of establishing for φ the existence of such a model and an assignment is called SMT problem for T . Examples of theories from the SMT literature are EUF, the theory of equality with uninterpreted symbols, and LIA/LRA, the theory of linear integer/real arithmetics. A T-cover of a formula ∃xφ(x, y) is a formula ψ(y) that is implied by ∃xφ(x, y) and implies all the other implied formulae φ′ (z, y) modulo T. A theory T has covers iff all formulae ∃xφ(x, y) have a T -cover, and an effective procedure for computing them is available. Computing T-covers is strictly related to the problem of eliminating quantifiers in suitable theory extensions of T [Calvanese et al., 2021].

We introduce case-defined functions. Fix a Σ-theory T; a T-partition is a finite set κ1(x), . . . , κn(x) of quantifierfree formulae s. t. T |= ∀x ∨ni=1 κi(x) and T |= ∧i̸=j ∀x¬(κi(x) ∧ κj(x)). Given such a T-partition together with Σ-terms t1(x), . . . , tn(x) (all of the same target sort), a case-definable extension is the Σ′ -theory T ′ where Σ′ = Σ ∪ {F}, with F ̸∈ Σ, and T ′ = T ∪ ⋃ni=1 {∀x (κi(x) → F(x) = ti(x))}. Intuitively, F represents a case-defined function using nested if-then-else expressions as: F(x) := case of {κ1(x) : t1; · · · ; κn(x) : tn}. We identify T with any of its case-definable extensions T ′ . In fact, given a Σ′ -formula φ′ , one can easily find a Σ-formula φ that is equivalent to φ′ in all models of T ′ . We also use specific λ-abstractions and abbreviate FO formulae of the form ∀y. b(y) = F(y, z) (where, typically, F is a symbol introduced in a case-defined extension) into b = λy.F(y, z).

4 Relational Action Bases

Now we introduce the formalism of relational action bases (RABs), following the widely adopted framework of artifact systems [Hull, 2008], in their most general form structured in three components [Deutsch et al., 2016]: (i) a read-only relational database (DB) with primary and foreign keys, to store background, static information; (ii) a mutable working memory consisting of a set of evolving relations; (iii) a set of guarded transitions that inspects the DB and the working memory, and updates the latter. RABs actually take the RAS model of [Calvanese et al., 2020] (which supports the most expressive forms of guarded transitions), with two essential extensions: full-fledged arithmetic theories, and universal quantification in the guards and effects of transitions.

4.1 Static DB Schemas

Static DB schemas define read-only relations with primary and foreign key constraints, which host pure identifiers subject to EUF, or integer/real data attributes subject to arithmetic constraints expressed in LIA/LRA.

Definition 1. A static DB schema (SDB schema for short) is a pair DB := 〈ΣDB ∪ Σar , T DB ∪ T ar 〉, where:

• ΣDB , called SDB signature, is a finite multi-sorted signature (where sorts are partitioned into id and value sorts ΣDB srt = ΣDB ids ⊎ΣDB val ), whose symbols are equality, unary functions, n-ary relations and constants;
• T DB , called SDB theory, is EUF(ΣDB ) ∪ {∀x (x = undef ↔ f(x) = undef)}, for every function f in ΣDB ;
• Σar , called arithmetic signature, is the signature of LRA or of LIA, and its sorts are Σar srt ;
• T ar , called arithmetic theory, is LRA or LIA.
• ΣDB val ∪Σar srt can only be the codomain sort of a symbol from ΣDB other than an equality predicate;

We respectively call Σ := ΣDB ∪ Σar and T := T DB ∪ T ar the full signature and the full theory of DB.

The definition employs an unusual functional approach for modeling DB schemas (needed for the technical machinery of safety checking procedures), and captures the most sophisticated read-only DB schemas considered in the literature [Deutsch et al., 2019; Calvanese et al., 2019]. Unary functions capture relations with primary and foreign keys. Specifically, the domain of a unary function is an id sort, representing object identifiers for that sort. Functions sharing the same id sort as domain model the attributes of such objects, which either point to other id sorts (implicitly representing foreign keys), or to so-called value sorts that denote primitive datatypes. While in previous works only uninterpreted value sorts could be employed, here we also support real/integer datatypes, subject to arithmetic theories that considerably increases the modeling power of the language.

We use a special undef constant to model NULL-like objects/values in the working memory, and an axiom ∀x (x = undef ↔ f(x) = undef) to indicate that application of a function to undef returns an undefined value/object and that this is the only case for which the function is undefined.

Definition 2. An SDB instance of DB := (Σ, T) with Σ := ΣDB ∪ Σar is a Σ-structure M that is a model of T and s.t. every id sort of ΣDB is interpreted inMon a finite set.

There is a key difference between SDB instances and arbitrary models of T DB ∪ T ar : finiteness of id sorts and of the non-id values that can be pointed from id sorts using functions. This is customary for DBs [Abiteboul et al., 1995]. Notice, T DB has the finite model property for constraint satisfiability, so the SMT problem can be equivalently reframed by asking for the existence of an SDB instance instead of a generic T DB model [Calvanese et al., 2020].

Example 1. Consider a visa application center, with a readonly DB storing information critical to the application process. We formalize this in a DB signature Σv with: (i) one id sort to identify citizens; (ii) two value sorts INT and STRING, used for evaluating applications (e.g., by giving scores).

4.2 RAB Transitions

The working memory of a RAB consists of individual and function variables. Function variables model evolving relations, in the style of [Li et al., 2017], while individual variables are used both to store global information about the control state of the process, and to load and manipulate (components of) tuples from the static relations.

Given an SDB schema 〈Σ, T〉, a (working) memory extension of Σ is a signature Σext obtained by adding to Σ extra sort symbols E, E1, E2 . . . , called memory sorts, together with corresponding equality predicates. Now, the "old" sorts from Σ are called basic (variables of basic sorts we call 'basic sort' variables). This is done to model the mutable working memory similarly to the static DB: implicit identifiers of working memory tuples form working memory relations, whereas data values of such tuples have basic sorts.

A memory schema is a pair (x, a) of individual and unary function variables. Variables in x are called memory variables, and the ones in a - memory components. The latter are required to have a memory sort as source sort and a basic sort as target sort. Given an SDB instance M of Σext , an assignment to a memory schema (x, a) over Σext is a map α assigning to every xi ∈ x of sort Si an element xα ∈ SM i and to every aj : Ej -→ Uj (with aj ∈ a) a function aαj : EM j -→ U M j . The notion of assignment formally captures the current configuration of the working memory. An assignment to (x, a) can be seen as an SDB instance extending the SDB instance M. Assuming that a contains ai1 : E -→ S1, · · · , ain : E -→ Sn, the memory relation E in the assignment (M, α) is the set {〈e, aαi1 (e), . . . , aαin (e)〉 | e ∈ EM}. Thus each tuple of E is formed by an implicit unique "identifier" e ∈ EM (called index) and by "data" aαi (e) taken from the static DBM. When the system evolves, EM remains fixed, while aαi (e) may get repeatedly updated. "Removing" a tuple from E results in e being reset to undef. This clarifies the relational nature of the working memory.

Given a memory schema (x, a) over Σext with x = x1, . . . , xn and a = a1, . . . , am, we list the kind of formulae that can be used in RABs: (1) an initial formula ι(x, a) := (∧ni=1 xi = ci) ∧ (∧mj=1 aj = λy.dj), where ci, dj are constants from Σ (typically, ci and dj are initially set to undef); (2) a state formula ∃eφ(e, x, a), where φ is quantifier-free and e are individual variables of artifact sorts (called 'index' variables); (3) a transition formula (t-formula)

where the e and d are 'index' and 'basic sort' individual variables resp., k is an individual variable of artifact sort, γ (the "(plain) guard") and γu (the "universal guard") are quantifierfree, x′ and a′ are renamed copies of x and a, and Fi, Gj (the "updates") are case-defined functions. The existentially quantified "data" variables d (of basic sort) are essential: they support existential queries over the SDB schema for retrieving data elements or arithmetical values (integers or reals), and (non-deterministic) external inputs. There are two key technical differences with the RAS model [Calvanese et al., 2020]: universally quantified guards γu, and the usage of arithmetical constraints and operations in guards and updates.

Such transition formulae can model operations over tuples like (i) insertion (with/without duplicates) in a memory relation, (ii) removal from a memory relation, (iii) transfer from a memory relation to memory variables (and vice-versa), and (iv) bulk removal/update in a memory relation, based on a condition expressed on such relation. These operations can be formalized as RAB transitions: modeling patterns using this approach have been shown in [Calvanese et al., 2019].

Definition 3. A relational action base (RAB) is a tuple S = 〈〈Σ, T〉,Σext , x, a, ι(x, a), τ(x, a, x′ , a′ )〉, where: (i) 〈Σ, T〉 is an SDB schema, (ii) Σext is a memory extension of Σ, (iii) (x, a) is a memory schema over Σext , (iv) ι is an initial formula, and (v) τ is a disjunction of t-formulae tr.

Notice that τ symbolically represents the union of all system transitions. Such transitions are used to establish interaction between the static DB (with SDB schema DB) and the working memory (with memory schema (x, a)).

Example 2. Consider a RAB Sva capturing a process for evaluating visa applications and informing the applicants about the visa decisions. Sva works over the SDB schema from Example 1. The working memory of Sva consists of variables capturing the main process phases (pState), the citizen's visa status (visaStat) and ID used to notify about the application result (toNotify), and a multi-instance artifact for managing visa applications. The latter is formalized by adding to DB signature Σv a memory sort appIndex (to "internally" identify the applications), and by adding a memory schema with the applicant's ID applicant : appIndex -→ Int, evaluation score appScore : appIndex -→ Int, and application results appResult : appIndex -→ String.

We now showcase a few t-formulae for managing visa applications. We assume that if a memory variable/component is not mentioned in a t-formula, then its values remain unchanged. To insert an application into the system, the process has to be enabled. The corresponding update simultaneously (i) selects the applicant's ID and inserts it into the memory component applicant , (ii) evaluates the visa application and inserts a non-negative score into the memory component appScore. Since memory tuples must have implicit identifiers, the above insertion requires a"free" index (i.e., an index pointing to an undefined applicant) to be selected:

Applications can be nondeterministically evaluated (by assigning evaluation to pState), resulting in highly evaluated ones being approved and others rejected:

If there is at least one approved application, a nondeterministically selected applicant is getting notified:

∃i:appIndex

⎛⎝pState = evaluated ∧ pState ′ = notified ∧ applicant [i] ̸= undef ∧ appResult [i] = approved ∧ toNotify ′ = applicant [i] ∧ visaStat ′ = appResult [i] ⎞⎠

Algorithm 1: BReachRAB

input: RAB 〈〈Σ, T 〉, Σext , x, a, ι(x, a), τ (x, a, x′ , a′ )〉 input: (Unsafe) state formula υ(x, a) 1 P ←- υ; ˜B ←- ⊥; 2 while P ∧ ¬ ˜B is T -satisfiable do 3 if ι ∧ P is T -satisfiable then return (UNSAFE, unsafe trace witness) 4 ˜B ←- P ∨ ˜B; 5 P ←- InstPre(τ, P); 6 P ←- Covers(T, P); return (SAFE, ˜B);

Finally, we demonstrate a transition with a universal guard checking whether no application has been approved and, if so, changes the process state to no-visa: pState = evaluated ∧ ∀k (appResult [k] ̸= approved) ∧ pState ′ = no-visa

5 Parameterized Safety Verification

We turn to safety verification of a RAB S, formalizing it by analogy with RASs [Calvanese et al., 2020], in tradition of artifact systems [Deutsch et al., 2018]. As we will see, inspite of similar formulation, the corresponding algorithmic techniques for RABs are different, and so is proving their (meta-) properties. The main idea is to analyse whether S is safe (i.e., S never reaches an undesired state satisfying unsafe formula υ(x, a)) independently from the specific configuration of read-only data, i.e., for every instance of the SDB schema of S. Technically, S is safe w.r.t. υ if there is no SDB instance M of 〈Σext , T〉, no k ≥ 0, and no assignment in M to the variables x0 , a0 . . . , xk , ak s.t. formula

is true in M (xi , ai are renamed copies of x, a). Formula can be seen as a symbolic unsafe trace. The safety problem (S, υ) consists of establishing whether S is safe w.r.t υ.

Example 3. The following formula describes an unsafety property for the RAB from Example 2, checking whether the evaluation notification goes to an applicant who was rejected: ∃i:appIndex(applicant[i] ̸= undef ∧ toNotify = applicant [i] ∧ visaStat = rejected ∧ pState = notified).

Safety verification procedure. Algorithm 1 introduces the BReachRAB procedure for safety verification. It shows how the backward reachability procedure for SMT-based safety verification, first studied in [Ghilardi and Ranise, 2010a] for array-based systems and refined in [Calvanese et al., 2020] to deal with RASs, is extended to handle the advanced features of RABs. BReachRAB takes as input a RAB S and an unsafe formula υ. The main loop starts from the undesired states of the system (represented by υ), and explores backwards the state space by iteratively computing, symbolically, the set of states that can reach the undesired ones. Every iteration regresses the current undesired states by considering the transitions τ of S in a reversed fashion. As we describe next, due to the presence of universal guards, τ can be reversed only in an approximated way. The computation of symbolic, approximated preimages is handled in Lines 5 and 6.

Let ψ(x, a) be a state formula describing the state of variables x, a. The exact preimage of the set of states captured by ψ(x, a) is the set of states captured by Pre(τ, ψ) (note that, when τ = ∨i tri, then Pre(τ, ψ) = ∨i Pre(tri, ψ)). This is the exact set of states that, by executing τ once, reaches the set of states described by ψ. The main issue we get in doing so is that a state formula is an existentially quantified Σ-formula over indexes only. While ψ is a state formula, Pre is not, making it impossible to reiterate the preimage computation. This is due to universally quantified 'index' variable k and existentially quantified 'data' variables d in τ. To attack this problem, we introduce in Lines 5 and 6 of BReachRAB two over-approximations, guaranteeing that the preimage is a proper state formula and that we use preimage computation to regress undesired states arbitrarily many times.

The first approximation (Line 5) compiles away the universal quantifier ranging over the index k through instantiation, by invoking InstPre(τ, ψ). Given τ := ∨pr=1 trr, let ∀k γ ru (k, e, d, x, a) be the universal guard of trr for all r = 1, . . . , p. InstPre(τ, ψ) approximates Pre by instantiating the universally quantified 'index' variable k with the existential 'index' variables appearing in Pre(trr, ψ), for all r = 1, . . . , p. Formally, given ψ := ∃e1ϕ1(e1 , x, a), InstPre(trr, ψ) is the formula obtained from

by making the appropriate substitutions (followed by betareduction) in order to eliminate the existentially quantified variables x′ and a′ (see, e.g., [Calvanese et al., 2020] for details). The second approximation (Line 6) takes the socomputed result InstPre(τ, ψ) ≡ ∃e2 , dϕ2, and compiles away the existentially quantified data variables d. This is done by invoking Covers(T, ∃e2 , dϕ2): it 'eliminates' the d variables via the cover computation algorithm for the theory combination T DB ∪ T ar , which admits covers [Calvanese et al., 2022a]. Both approximation operators are T-implied by the exact preimage operator.

Together, Lines 5 and 6 produce proper state formula ψ′ that can be fed into another approximate preimage computation step. In fact, BReachRAB iteratively computes such preimages starting from the unsafe formula υ, until one of two possible termination conditions holds: these conditions are tested by SMT-solvers. The first condition occurs when the non-inclusion test in Line 2 fails, detecting a fixpoint: the set of current unsafe states is included in the set of states reached so far by the search. In this case, BReachRAB stops returning that S is safe w.r.t. υ. The second termination condition, occurring when the non-disjointness test in Line 3 succeeds, detects that set of current unsafe states intersects the initial states (i.e., satisfies ι). In this case, BReachRAB stops returning that S is unsafe w.r.t. υ, together with a symbolic unsafe trace of the form (1). Such a trace provides a sequence of transitions tri that, starting from the initial configurations, witness how S can evolve from an initial state in ι, under some instance of its SDB, to a state satisfying υ.

Being preimages computed in an over-approximated way, unsafety may be spuriously returned, together with an unsafe spurious trace that cannot be produced by a given RAB. We next study this and other meta-properties of BReachRAB.

Meta-properties. Consider a procedure for verifying safety of RABs. Given a RAB S and an unsafe formula υ, a SAFE (resp. UNSAFE) output is correct iff S is safe (resp. unsafe) w.r.t. υ. We use this to define some key meta-properties.

Definition 4. Given a RAB S and an unsafe formula υ, a procedure for verifying unsafety of S w.r.t. υ is: (i) sound if, when terminating, it returns a correct result; (ii) partially sound if a SAFE result is always correct; (iii) complete if, whenever UNSAFE is the correct result, then it returns so.

By using that reachable states via approximated preimages include those obtained via exact preimages, we get:

Proposition 1. If BReachRAB returns SAFE when applied to the safety problem (S, υ), then S is safe w.r.t. υ.

It can be also proved (see the extended version [Ghilardi et al., 2022b]) that if S is unsafe w.r.t. υ, the procedure terminates with UNSAFE. We show that BReachRAB can only be used partially to verify unsafety of RABs. Next, effectiveness means that all subprocedures in BReachRAB can be effectively computed (from [Calvanese et al., 2020], the occurring T -satisfiability tests are decidable).

Theorem 1. BReachRAB is effective, partially sound and complete when verifying unsafety of RABs.

RABs that do not employ universal guards collapse to RASs equipped with numerical values and arithmetics. By carefully combining results on soundness and completeness of backward reachability of RASs [Calvanese et al., 2020], and on the existence of combined covers for EUF and LIA/LRA [Calvanese et al., 2022a], we obtain for these RABs that no spurious results are produced:

Theorem 2. BReachRAB is effective, sound and complete (and hence a semi-decision procedure) when verifying safety of RABs without universal guards.

Proof. FromTheorem 1, the only thing that remains to prove is that Algorithm 1 is fully sound if the RAB does not contain universal guards. In this case, InstPre ≡ Pre, hence Algorithm 1 coincides with the SMT-based backward reachability procedure for RASs introduced in [Calvanese et al., 2020]. Notice, however, that RABs without universal guards still strictly extend plain RASs from [Calvanese et al., 2020], since SDB are strictly more expressive than DB schemas of RASs: SDB schema contain arithmetic operations and are constrained by theory combinations where one component is an arithmetical theory. Nevertheless, using the results and the procedures presented in [Calvanese et al., 2021; Calvanese et al., 2022a] for computing covers, and given the equivalence between computing covers and eliminating quantifiers in model completions from [Calvanese et al., 2020], in order to conclude one can use the analogous arguments based on model completions as the ones used in [Calvanese et al., 2020] for proving full soundness of RASs.

6 Safety Universal Invariants

Injecting and exploiting invariants in the verification of dynamic systems is a well-known approach. Also, instantiation is a widely studied in invariant checking [Feldman et al., 2019]. In our setting, invariants can dramatically prune the search space of backward reachability procedures, in general also increasing the chances that the procedure terminates [Ghilardi and Ranise, 2010a]. We contribute to this line by introducing a suitable notion of (universal) invariant for RABs, and by studying its impact to safety verification.

Definition 5. φ(x, a) := ∀iψ(i, x, a) (with i variables of artifact sort) is an (inductive) universal invariant for a RAB S iff (a) T |= ι(x, a) ⇒ φ(x, a), and (b) T |= φ(x, a) ∧ τ(x, a, x′ , a′ ) ⇒ φ(x′ , a′ ). If, in addition to (a) and (b), we also have (c) φ(x, a)∧υ(x, a) is T -unsatisfiable, then φ(x, a) is a safety universal invariant for the safety problem (S, υ).

Following the arguments from [Calvanese et al., 2020], the T-satisfiability tests required in (a), (b), and (c) are decidable. Using invariants for safety verification is, to some extent, "more general" than using (variants of) backward reachability. Unfortunately, the so-called invariant method is more challenging because finding safety invariants cannot be mechanized (see, e.g., [Ghilardi and Ranise, 2010a]). Yet, if a universal invariant has been found in some way (e.g., with heuristics) or supplied by a trusted knowledge source, then it can be effectively employed in the fixpoint test of backward reachability, e.g., by replacing Line 2 of Algorithm 1 with:

where Inv is a conjunction of universal invariants. This further constrains the formula P ∧ ¬ ˜B with Inv, possibly increasing the chances to detect unsatisfiability.

The following result is useful: it shows that Algorithm 1 can be used to find safety universal invariants.

Proposition 2. If Algorithm 1 returns (SAFE, ˜B), then ¬ ˜B is a safety universal invariant.

Sketch. By construction, ˜B is an existential formula over artifact sorts only, hence ¬ ˜B is universal. We show in the extended version [Ghilardi et al., 2022b] that conditions (a),(b),(c) from Definition 5 hold.

Let Pn the value of the variable P at the n-th iteration of the main loop BReachRAB. We prove the following key, nontrivial result on how safety universal invariants relate to the (approximated) preimages computed by BReachRAB.

Theorem 3. If a safety universal invariant φ exists for a RAB S w.r.t. υ, then for every n ∈ N, we have Pn → ¬φ.

Sketch. The argument is quite delicate: it is always possible to extend a structure w.r.t. its Σ-reduct and at the same time to restrict the given structure w.r.t. its Σext \Σ-reduct, and these 'opposite' constructions does not interfere with each other. We prove the statement by induction on the number n of iterations of the main loop of BReachRAB.

Base case. In case n = 0, the statement follows from P0 ≡ υ and condition (b) of Definition 5.

Inductive case. By inductive hypothesis, we have that T |= Pn → ¬φ. We show that T |= Pn+1 → ¬φ holds as well. First, we notice that, by condition (c) of Definition 5, T |= τ (x, a, x′ , a′ ) ∧ ¬φ(x′ , a′ ) → ¬φ(x, a) holds. The previous implication can be rewritten as

since, by definition of preimage, we have T |= ∃x′∃a′ (τ (x, a, x′ , a′ ) ∧ ¬φ(x′ , a′ )) ≡ Pre(τ, ¬φ).

Preimage is monotonic, i.e., given two formulae α and β, α → β implies Pre(τ, α) → Pre(τ, β). Hence, from the inductive hypothesis T |= Pn → ¬φ, we get

From Formulae (3) and (2) it follows that

By construction and induction, InstPre(τ, Pn) is an existential formula over artifact and basic sorts. By applying Covers, we eliminate the existentially quantified variables over basic sorts, and get an existential formula over artifact sorts only. Hence, since Pn+1 ≡ Covers(T, InstPre(τ, Pn)), we can assume that Pn+1 has the form ∃ˆeψ(ˆe), where ψ is quantifier-free. Thus, we need to prove that:

By reduction to absurdum, suppose that there is a SDB instance A s.t. A ̸|= ∃ˆe ψ(ˆe) → ¬φ. By model-theoretic properties of covers, from A it is possible to build a SDB instance B1 s.t. B1 |= InstPre(τ, Pn) ∧φ. Moreover, from B1 we can find a SDB instance B2 where the instantiations of the universal quantifiers cover all the elements of its domain: hence, B2 |= Pre(τ, Pn) ∧ φ, which contradicts entailment (4), as wanted. All the details are in [Ghilardi et al., 2022b].

By combining Definition 5 and Theorem 3 we get:

Corollary 1. If there exists a safety universal invariant φ a RAB S, then BReachRAB cannot return UNSAFE.

Corollary 1 implies that if there is a safety universal invariant for S, then Algorithm 1 cannot find any spurious unsafe traces. We know from Proposition 1 that in case Algorithm 1 returns (SAFE, ˜B), then the system is safe: notice also that in this case, ¬ ˜B is a safety universal invariant (see [Ghilardi et al., 2022b] for details). However, if it returns an unsafe outcome, the answer could be wrong due to the presence of spurious unsafe traces.

The importance of Corollary 1 lies in the fact that, even if we do not know any safety universal invariant, we are assured that in case one exists, the procedure behaves well/properly/in a fair way, as no unsafe outcome can be returned and therefore no spurious trace can be detected. Corollary 1 is conceptually analogous to the invariant result in [Karbyshev et al., 2017], with two subtantial technical differences: (i) they deal with formulae that fall into the decidable Barneys-Sch¨onfinkel FO fragment (the '∃∗∀∗ ' fragment) with only relational symbols, which does not capture functional key dependencies nor standard arithmetical operations over real/integers as we do here; (ii) the two results hold for different verification procedures: ours for backward reachability, theirs for IC3.

Example 4. The following is a safety universal invariant for (Sva , υ): (visaStat = rejected → toNotify = undef).

7 Practical Verification of RABs

We now put our verification machinery in practice, exploiting that, as shown in our technical development, we can employ the different modules of MCMT to handle parameterized safety checking of RABs. We test the novel features of RABs, namely universal quantification and arithmetics on relational dynamic systems, for which no other existing tool can be employed. Specifically, we conduct an extensive experimental evaluation on RABs representing 33 (32 plus one variant) concrete data-aware processes derived from the existing benchmark in [Li et al., 2017]. We encode all these 33 models into RABs, using the concrete syntax of the database-driven mode of MCMT (available since Version 2.8). We set up our benchmark by taking 26 out of the 33 process models in [Li et al., 2017], naturally extending them with arithmetic and/or universal guards (features not supported by VERIFAS [Li et al., 2017]). The remaining 7 examples do not lend themselves to such an extension, and are kept unaltered. We nevertheless include them for completeness. We also add an extra example E+ that incorporates all modeling features of RABs (e.g., bulk updates that go beyond the capabilities of VERIFAS [Li et al., 2017]), with the intention of stress-testing MCMT. Each example is checked against 12 conditions, with at least one safe and one unsafe; E+ is checked against 33 conditions. Overall, we ran MCMT over 429 specification files. The benchmark is on https://github.com/AlessandroGianola/RAB-verification.

Experiments were performed on a 2.3 GHz Intel Core i5 machine with macOS High Sierra and 8 GB RAM. Results are shown in Table 1 (more detailed information is in [Ghilardi et al., 2022b]), which reports, for each example: (i) if it contains arithmetics (Ar) and universal guards (UG); (ii) the number of transitions (#T), also counting those that contain quantified data variables (#Q). The table also includes several measures: (i) number of UNSAFE (#U) and SAFE (#S) outcomes; (ii) seconds for the average (µT) and maximum (MaxT) MCMT execution time; (iii) indications of number of calls to the external SMT solver (#(calls)).

The means of execution times are relatively small. For the 26 plus 1 models supporting the specific features of RABs, MCMT terminates in less than one second for 85.2% of the tested files, and in less than one minute for 343 out of 345. The two files over one minute take 90.36 and 98.27 seconds. For all 34 models, MCMT terminates in less than one second for 366 out of 429, the highest timing being 171.63 seconds. Our preliminary experiments indicate that universal guards and arithmetic constraints do not sensibly impact the timing.

If the outcome is unsafe, MCMT returns a witness that reconstructs the unsafe trace as a formula. With this formula one can test whether the trace is spurious or not. This feature is currently not directly supported by MCMT, but can be tested via SMT solvers off-the-shelf. In particular, trace formulae belong to the ∃∗∀∗ (EPR) fragment of FOL, for which the Z3 solver [de Moura and Bjørner, 2008] has a dedicated decision procedure. The complexity is the one of satisfiability checking in the EPR fragment, which is NEXPTIME-complete.

As far as we know, no other tool or benchmark exists for further experimental evaluation. The existing model checkers (also infinite-state ones) rarely can handle specifications expressed with quantifiers: however, as also argued in [Calvanese et al., 2020], quantifiers are needed when dealing with relational database-driven verification. For handling them, we need non-trivial approximation modules, such as instantiation for universal variables and covers computation for data variables. MCMT is the only model checker specifically oriented to employ these sophisticated techniques.

8 Conclusions

We have presented the RAB framework for modeling rich relational dynamic systems with arithmetics and universal guards, developing techniques for safety verification and invariant-based analysis. Our results do not only have a foundational importance, but also witness that separately implemented verification modules in the MCMT model checker can be indeed gracefully combined to obtain a safety verification procedure for RABs. The experimental evaluation here reported shows that this is an effective, practical approach.

In the paper, we have surveyed concrete scenarios that require the advanced features of RABs, in the context of multiagent systems [Felli et al., 2021] and extensions of Petri nets [Fahland, 2019; Polyvyanyy et al., 2019; Ghilardi et al., 2020]. The next step is to encode them into RABs. Considering that encoding concrete models typically produce update formulae with a specific shape, we then want to extract relevant universal invariants as a by-product of the encoding. Another interesting direction is to verify properties that go beyond safety. This is an open research problem for SMT-based verification in general, as symbolic reachability techniques like those used in this paper are tailored to safety.

Acknowledgments

This research has been partially supported by the Italian Ministry of University and Research (MUR) under PRIN project PINPOINT Prot. 2020FNEB27, and by the Free University of Bozen-Bolzano with the ADAPTERS project.