Dynamic Logic for Data-aware Systems: Decidability Results

1 Introduction

In recent years data-aware and data-driven systems acquired pre-eminence as a formal framework to represent and reason about systems in which data play a key role in the system's execution [Bhattacharya et al., 2007; Deutsch et al., 2007; 2009]. Initially, data-aware systems (DaS) appeared as a novel paradigm for the design of business processes in service-oriented computing [Singh and Huhns, 2005]. The originality of this approach consists in "combin[ing] data and processes in a holistic manner as the basic building block[s]" of the system's description [Cohn and Hull, 2009]. Normally a DaS is comprised of a data model accounting for the relational structure of data, as well as the business processes manipulating data. Both the data model and business processes are equally important components of the system specification. Due to that, DaS differ profoundly from most of the tradition on service architectures and composition, in which data are typically abstracted away to reduce the complexity of the system description, thus making the verification task amenable to standard model checking techniques [Singh and Huhns, 2005].

Recently, the data-driven paradigm has found applications beyond service-oriented computing. Notably, a wealth of contributions have put forward data-driven approaches to knowledge representation and reasoning (KR&R) as well as to the modelling of multi-agent system (MAS). More specifically, [Bagheri et al., 2011; 2013] introduced knowledge and action bases (KAB) to describe distributed systems comprising a relational database, over which agent-services oper-

Andreas Herzig

IRIT Toulouse Universit´e de Toulouse CNRS

herzig@irit.fr

ate. KAB were then extended to include a number of different features relevant for modelling MAS, including commitments [Montali et al., 2014], plans [Calvanese et al., 2016b], and norms [Baldoni et al., 2016]. More directly related to the present contribution, [Belardinelli et al., 2012; 2014] tackled the verification problem for artifact-centric multiagent systems-a particular class of data-aware systemsand proved it to be decidable under specific assumptions. Here we extend the state of the art by considering an expressive dynamic modal language. Indeed, in the line including [Deutsch et al., 2009; Bagheri et al., 2011; 2013; Belardinelli et al., 2012; 2014], the specification language for data-aware systems is typically a first-order extension of either branching-time temporal logic CTL or of the µcalculus [Clarke et al., 1999]. In such languages one can express properties holding in some or all executions of the system. However, the structure of such executions is not exhibited transparently in the specification language, and actions do not appear explicitly in the temporal operators of CTL nor in those of the µ-calculus. To overcome these issues, here we consider a dynamic modal language [Pratt, 1976; Harel et al., 2000] in which actions are explicitly named in the modal operators. This syntactic choice allows us to express complex behaviours in a precise and concise way. However, the application of dynamic logic to the specification of dataaware systems calls for novel verification techniques w.r.t. the state of the art.

Contribution. We introduce a novel interpretation of firstorder dynamic logic that suits the formal description of relevant aspects of DaS. The language has assignments v := t and v :=? as atomic actions, which are intuitively interpreted as assigning to variable v the value t, or, respectively, any value. More complex actions are built by using the operators of Propositional Dynamic Logic (PDL). Most importantly, by using finite abstractions we prove that the model checking problem for a significant class of data-aware systems is decidable. We illustrate the importance of the technical result through an application to the verification of English auctions.

Related work. Dynamic logic is one of the success stories of formal methods applied to computer science. However, its first-order extensions are comparatively less studied than its standard propositional version. The language we consider appears in [Harel et al., 2000] with some key differences. First, we do not include function symbols and the only relation symbols are the identity '=' and less or equal than '≤'. More importantly, we interpret this language on structures with a finite active domain. We will show that this key difference, motivated by the literature on databases, allows us to obtain a decidable verification problem.

As regards DaS, besides the contributions discussed above, a further line of research works within the situation calculus [De Giacomo et al., 2012; de Giacomo et al., 2014; De Giacomo et al., 2016]. By assuming that the underlying theories are bounded, the model checking problem is proved decidable. Here we do not need to assume boundedness as a separate hypothesis. More closely related to the present contribution, [Giacomo et al., 2016] shows that GOLOG programs in the situation calculus are naturally bounded, and therefore their verification is decidable [Calvanese et al., 2016a]. Differently from these works (including [Bagheri et al., 2011; 2013; Belardinelli et al., 2012; 2014]) here we consider a rich first-order dynamic modal language where actions are explicit.

2 Data-aware Systems and Dynamic Logic

In this section we introduce formally DaS as well as all notions to be used in the rest of the paper. Hereafter we assume:

1. a finite, non-empty set V of individual variables v1, . . . , vn;
2. a finite, possibly empty set C of individual constants c1, . . . , cm;
3. a possibly infinite set U ⊇ C of individuals u1, u2, . . . for the interpretation of variables, together with a total order ≤ defined on U .

Definition 1 (DaS) A Data-aware System is a tuple M = 〈V, C, U〉, where V , C, and U are defined as above.

Intuitively, given a program written in some programming language (e.g., Fortran, Java, C), a DaS M is the collection of all variables and constants appearing in the program, together with the range of values for the variables. Notice that, while most programming languages are typed, here we consider an untyped formalism. We do so to keep the presentation more easily accessible to the general audience. The present formalism can be extended quite seamlessly to typed languages, even though the exercise is time- and spaceconsuming. Hereafter we distinguish between general dataaware systems and DaS in the technical sense of Def. 1.

Given a DaSM, a state s : V → U is an interpretation of the variables in V . States can be thought of as a representation of the registers of the program associated withMat a given time. Given a state s, its active domain adom(s) = {u ∈ U | u = s(v) for some v ∈ V } ∪ C ⊆ U is the co-domain of s (the set of all values for the variables in V at s), together with constant values. This (standard) notion of active domain is taken from the literature on database systems [Abiteboul et al., 1995]. Observe that adom(s) is finite as V and C are.

Finally, since the domain U of interpretation is possibly infinite, we have an infinite number of states in general, and therefore DaS are infinite-state systems.

Syntax. In order to write formulas that describe the dynamics of DaS, we consider an infinite set P of parameters x1, x2, . . .. Then, a term t ∈ T is any element in V ∪ C ∪ P , that is, t can be either a variable, or a constant, or a parameter. We introduce assignments v := t and v :=? as atomic actions, as well as atomic formulas t = t′ and t ≤ t′ , for v ∈ V and t, t′ ∈ T .

Definition 2 (FO-DL) Formulas φ and actions α in Firstorder Dynamic Logic are defined by mutual recursion as follows:

where v ∈ V is a variable, t ∈ T is a term, and x ∈ P is a parameter.

Definition 2 is inspired by the language for first-order dynamic logic appearing in [Harel et al., 2000]. Atomic actions are assignments v := t, that assign the value of term t to variable v, and "wildcard" assignments v :=?, that assign to v some arbitrary value from domain U. Complex actions are obtained by composition ;, non-deterministic choice ∪, iteration ∗, and test ?.

Differently from [Harel et al., 2000], we here restrict the first-order component: FO-DL contains no function symbol and only two relation symbols, the identity '=' and less or equal than '≤'. Indeed, first-order dynamic logic with two function symbols (and identity) has the same expressive power as elementary arithmetic [Harel et al., 2000, Proposition 12.1], and therefore it is undecidable. Notwithstanding these restrictions, we will see that our FO-DL is expressive enough for many cases of interest; notably, we will see in in Section 2.1 that we can express auctions.

As a note on syntax, observe that parameters x ∈ P are used to write formulas and are infinite in number, while variables v ∈ V are really constituents of the Data-aware System and are finitely many. The two must be kept distinct. Hereafter, propositional connectives are introduced as standard and formula 〈α〉φ is shorthand for [α]φ.

Given a term t ∈ T, we introduce the function P(t) that returns set {t} if t = x ∈ P is a parameter, and the empty set otherwise. Then, given a formula φ and an action α in FODL, we define sets fr(φ) and fr(α) of free parameters, and P(φ) and P(α) of all parameters as follows:

Observe that the definitions of fr and P differ only as to the clause for quantified formulas. Also, wildcard assignments v :=? mention parameters implicitly. This remark motivates the following definition of #P (φ) ∈ N:

Because of the base case #P(v :=?) = 1 we have that |P(φ)| ≤ #P(φ) and |P(α)| ≤ #P(α). In particular, differently from P , #P keeps track of the occurrences of wildcard assignments as well. We use this fact in the construction of finite abstractions in Section 3. Notice that symbol P has been overloaded as it is used to denote functions on terms, formulas, and program expressions.

We now illustrate the expressive power of FO-DL by means of some toy examples.

Example 1 We consider a simple program that takes as input two integers, assign these as values to variables a and b, and then swaps their values by using a temporary variable tmp. Such a program can be specified in pseudo-code as follows:

int a, b; int tmp; tmp := a; a := b; b := tmp;

Even for such a simple program we might want to check that the new values for variables a and b are equal to the old values for b and a respectively, and this is indeed the case for every possible value of a and b. To do so, consider the following formula in FO-DL:

Intuitively, formula (1) corresponds to the specification above. In particular, parameters x and y are used to compare the values of variables a and b before and after the swap, that is, parameters are meant to store the value of variables throughout the computation.

As a further example, we consider an action α in FO-DL whose intended meaning is to compute the maximum among variables in V = {a0, . . . , an}:

α = max := a0; if max < a1 then max := a1; . . . if max < an then max := an;

where < is defined in the standard way (viz. u < u′ iff u ≤ u′ and u ̸= u′ ) and if φ then α is defined as usual in dynamic logic as (φ?; α) ∪ ¬φ?.

Then, we might want to check that action α actually returns the maximum. To this end, consider formula (2) in FO-DL that intuitively specifies that α is correct, as it actually computes the maximum, no matter what values for a0, . . . , an are provided as input:

As a result, FO-DL can be used as a specification language to express correct termination of programs involving variables for individuals, among other properties. ■

Semantics. To assign a meaning to the formulas and actions in FO-DL, we introduce interpretations σ : P → U of parameters into the domain U. In a state s, interpretations can be extended to any term t ∈ T as follows: for t = v ∈ V , (s ◦ σ)(t) = s(v); for t = c ∈ C, (s ◦ σ)(t) = c; while for t = x ∈ P, (s ◦ σ)(t) = σ(x). Hence, variables are interpreted according to s, parameters according to σ, while we adopt a Herbrandian interpretation of constants: they are interpreted as themselves. Given u ∈ U, σx u is the interpretation that assigns u to x ∈ P and coincides with σ on all other parameters.

Given a state s, we define the meaning of formula φ according to interpretation σ.

Definition 3 (Satisfaction) The satisfaction relation |= for DaSM, state s, interpretation σ, and formula φ is given as:

(M, s, σ) |= t = t′ iff (s ◦ σ)(t) = (s ◦ σ)(t′ ) (M, s, σ) |= t ≤ t′ iff (s ◦ σ)(t) ≤ (s ◦ σ)(t′ ) (M, s, σ) |= ¬φ iff (M, s, σ) ̸|= φ (M, s, σ) |= φ → φ′ iff (M, s, σ) ̸|= φ or (M, s, σ) |= φ′ (M, s, σ) |= [α]φ iff for all s′ , Rα(s, s′ ) implies (M, s′ , σ) |= φ (M, s, σ) |= ∀xφ iff for all u ∈ adom(s), (M, s, σx u) |= φ

where the relation Rα is defined by mutual recursion as

Rv:=t(s, s′ ) iff s′ (v) = (s ◦ σ)(t) and for every v′ ̸= v, s′ (v′ ) = s(v′ ) Rv:=?(s, s′ ) iff s′ (v) ∈ U and for every v′ ̸= v, s′ (v′ ) = s(v′ ) Rα;β(s, s′ ) iff for some s′′ , Rα(s, s′′ ) and Rβ(s′′ , s′ ) Rα∪β(s, s′ ) iff either Rα(s, s′ ) or Rβ(s, s′ ) Rα∗ (s, s′ ) iff R∗α(s, s′ ), where R∗α is the reflexive and transitive closure of Rα Rφ?(s, s′ ) iff (M, s, σ) |= φ and s′ = s

We remark that the interpretation of actions is as standard in first-order dynamic logic. In particular, atomic assignments v := t and v :=? update variable v with the value of term t, or, respectively, of any value in U.

As regards formulas, differently from [Harel et al., 2000], quantification is restricted to the active domain adom(s) in a given state s. This is a typical assumption in the theory of databases [Abiteboul et al., 1995], which we will show to be sufficient for our expressivity purposes, as it is the case in formulas (1) and (2).

We say that formula φ is true at state s of DaS M, or (M, s) |= φ, iff for every interpretation σ, (M, s, σ) |= φ; while φ is true in M, or M |= φ, iff for all s ∈ M, (M, s) |= φ. As an example, the formula

is true for every dense linear order <, in particular for the structure 〈Q,≤〉 of the rational numbers seen as a DaSM= 〈{a, b, c}, ∅, Q〉. On the other hand, the formula

is not true in general on dense orders, as parameter x ranges over the finite set adom(s) = {s(a), s(b), s(c)} of active elements. As a consequence, wildcard assignments and firstorder quantification express different notions in our semantics for FO-DL.

To investigate their relationship further, notice that if formula φ does not exhaust the finite set V of variables, then standard universal quantification, ranging on U rather than adom(s), is captured by formula [v :=?]∀x(x = v → φ), with the proviso that variable v does not occur in φ. However, since set V is finite, the translation scheme above is not applicable in general. In particular, first-order quantification is always restricted to the active domain.

In Example 1 we informally discussed the verification of programs against specifications (1) and (2). More precisely, we now state the model checking problem for this setting.

Definition 4 (Model Checking Problem) Given a DaS M and formula φ in FO-DL, determine whether M |= φ.

Since M is an infinite-state system in general, Def. 4 assumes some finitary representation of M, in particular of the interpretation domain U. This can be achieved in standard ways [Bagheri et al., 2013; Belardinelli et al., 2014].

Then, verifying the correctness of the swap and max programs in Example 1 when the variables are assigned real values is tantamount to model checking formulas (1) and (2) on all states interpreting the variables on the reals R. Notice that in this case M has infinitely many states: it is therefore not obvious whether the model checking problem is decidable.

2.1 Example: Auctions

In this section we model a toy example of an English (ascending bid) auction as a DaS. We assume familiarity with English auctions, in which a number of bidders bid for one or more items put on offer by an auctioneer. Bidders are assumed to be rational, in particular they have a true value up to which they are ready to bid. The auctioneer keeps track of the bids and, at the end of the bidding phase, she assigns the item to the bidder with the highest offer. We refer to [Easley and Kleinberg, 2010] for a detailed presentation of English auctions.

To represent the scenario above as a DaS with n bidders, we assume that the set V contains variables bidi and t valuei for every bidder i ≤ n, respectively representing the current bid and the true value of bidder i; moreover, we suppose that V contains a variable high for the highest offer so far. All these variables range over the rationals Q. Also, we consider a variable time out to terminate the bidding phase, taking values 0 and 1. We then model an English auction for n bidders as a DaS M = 〈V, {0, 1}, Q〉.

Then, we can specify the bidding cycle by means of the following action α:

time out := 0; while (time out = 0) do { ⋃i≤n (bidi :=?; if (bidi ≤ t valuei) ∧ (high < bidi) then high := bidi) ∪ time out := 1 }

Action α consists in an initial assignment of false (0) to time out, and then a while ψ do β loop (expressible in dynamic logic as (ψ?; β)∗ ; ¬ψ?), whose exit condition is that the bidding process has timed out (by means of the nondeterministic assignment time out := 1). Within the loop, a bidder is chosen non-deterministically to pass a bid via a wildcard assignment bidi :=?. If the bid is comprised between bidder i's true value and the highest bid so far, then it becomes the new high.

By means of action α we can specify in FO-DL a number of properties of auctions. For instance, we might want to say that throughout the auction, for every bidder, the values of bids are comprised between the highest offer so far and her true value:

Moreover, in FO-DL we can also compare values for the same variable at different points in the bidding process. As an example, we can express that true values do not change during the auction:

In (4) parameter x allows us to compare the value of t valuei before and after the execution of α.

Finally, in FO-DL we can specify that the value of the highest bid does not decrease throughout the auction:

Formulas (3)-(5) are simple specifications that nonetheless allow us to make comparisons between the values of variables at different points of the system's execution, which are typically not expressible in propositional languages. However, to verify properties such as (3)-(5), we cannot rely on standard model checking techniques because we are working with data-aware systems, for which the model checking problem is known to be undecidable in general [Deutsch et al., 2009]. In the next section we will develop a verification method adapted to the present framework and language.

3 Decidability via Finite Abstractions

In this section we introduce an abstraction-based technique to prove that the model checking problem in Def. 4 is indeed decidable. Then, we apply this result to the particular scenario of English auctions of Section 2.1. In the rest of the section we assume a (possibly finite) abstract domain U A ⊇ C.

Definition 5 (Abstract State) Given a (possibly finite) abstract domain U A ⊇ C, an abstract state is a function s : V → U A together with a total order ≤s defined on U A that extends the restriction ≤ |C of ≤ on C.

Notice that, differently from the standard states in Section 2, the total order ≤s depends on the particular abstract state s. In particular, for different s and s′ , ≤s may be different from ≤s′ . Nonetheless, each ≤s is an extension of restriction ≤ |C, that is, the order ≤ on C is preserved. Hence, for every c, c′ ∈ C, c ≤s c′ iff c ≤s′ c′ . Total extensions (for a finite U A) can be found constructively, using topological sorting algorithms [Cormen et al., 1990]. Hereafter, we do not discuss this matter further, and assume that suitable total extensions are always at hand.

Further, given a DaSM= 〈V, C, U〉 and U A ⊇ C, let the abstraction of M be the DaS MA = 〈V, C, U A〉. Next, we introduce a notion of isomorphism between states and their abstractions.

Definition 6 (Isomorphism) A state s ∈ M and an abstract state s′ ∈MA are isomorphic, or s ≃ s′ , iff for some bijection ι : adom(s) → adom(s′ ) ∪ C,

• (i) s′ = ι ◦ s;
• (ii) ι is the identity on C;
• (iii) ι preserves ≤, that is, for every u, u′ ∈ adom(s), u ≤ u′ iff ι(u) ≤s′ ι(u′ ).

Any bijection ι as above is a witness for s ≃ s′ , or s ι≃ s′ for short.

Intuitively, isomorphic states share the same relational structure. Observe that, as regards order ≤s′ , witness ι preserves the interpretation of individuals in the active domain s′ (V ) only (as well as the constant in C). This feature of isomorphisms is key to obtain finite abstractions.

Now we show that isomorphic states satisfy the same firstorder formulas φ as defined by the following BNF:

However, φ might contain free parameters interpreted outside the active domain. This remark motivates the following definition.

Definition 7 (Equivalent Interpretations) Given a state s ∈ M, an isomorphic abstract state s′ ∈ MA, and a formula φ, the interpretations σ : P →U and σ′ : P →U A are equivalent for φ w.r.t. s and s′ iff for some bijection θ : adom(s) ∪ σ(fr(φ)) → adom(s′ ) ∪ σ′ (fr(φ)),

• (i) the restriction θ|adom(s) is a witness for s ≃ s′ ;
• (ii) σ′ = θ ◦ σ;
• (iii) for every u, u′ ∈ adom(s) ∪ σ(fr(φ)), u ≤ u′ iff θ(u) ≤s′ θ(u′ ).

Again, as regards ≤s′ , a witness θ preserves only the order of individuals in s′ (V ) ∪ C ∪ σ′ (fr(φ)), which is a finite set. As customary in first-order logic, we can prove that equivalent interpretations on isomorphic states preserve first-order formulas [Abiteboul et al., 1995]. We report this result for our particular setting.

Lemma 1 Given a state s ∈ M, an isomorphic abstract state s′ ∈ MA, and an FO-formula φ, if interpretations σ and σ′ are equivalent for φ w.r.t. s and s′ , then (M, s, σ) |= φ iff (MA, s′ , σ′ ) |= φ.

We now prove that Lemma 1 can be lifted to the full language FO-DL. To do so, we need one more assumption. Given total order ≤, the corresponding strict linear order < is dense with no endpoints iff (i) for every u, u′ ∈ U, u < u′ implies that for some u′′ ∈ U, u < u′′ and u′′ < u′ ; and (ii) for every u ∈ U ′ , u < u′ and u′′ < u for some u′ , u′′ ∈ U. It is well-known that every non-empty countable dense linear order without endpoints is order-isomorphic to Q [Roitman, 1990, Theorem 27]. Hence, hereafter we assume U = Q as interpretation domain.

We can now prove the main preservation result of this paper. Hereafter we write Rα(s) = {s′ | Rα(s, s′ )}.

Theorem 2 Let M = 〈V, C, Q〉 be a DaS with abstraction MA = 〈V,C,U A〉. Then, consider a state s ∈ M, an isomorphic abstract state s′ ∈ MA, and an FO-DL formula φ. If |U A| ≥ |V | + |C| +#P(φ), then for all interpretations σ and σ′ equivalent for φ w.r.t. s and s′ ,

1. if φ is of the form [α]ψ, then
2. (a) for every state w ∈ Rα(s), there exists an abstract state w′ ∈ R′α(s′ ), isomorphic to w, such that σ and σ′ are equivalent for ψ w.r.t. w and w′ ;
3. (b) for every abstract w′ ∈ R′α(s′ ), there exists a state w ∈ Rα(s), isomorphic to w′ , such that σ and σ′ are equivalent for ψ w.r.t. w and w′ .

Sketch of Proof. We prove both item 1 and 2 by mutual induction on the structure of φ. We start by proving item 1, specifically by induction on the structure of α. As for the base case, let α ≡ v := t and consider interpretations σ and σ′ equivalent for φ w.r.t. s and s′ . If Rα(s, w) then w(v) = (s ◦ σ)(t), while the interpretation of the other variables remains the same. Then consider abstract state w′ such that w′ (v) = (s′ ◦ σ′ )(t) and w′ coincides with s′ on all other variables. Clearly w and w′ are isomorphic, as s and s′ are and σ and σ′ are equivalent. In particular, w′ can be chosen so that the total order ≤w′ preserves order ≤ on w′ (V ) ∪ C ∪ σ(fr(ψ)): if t is either a variable or a constant, then the result follows by condition (iii) in Def. 6; if t is a parameter, then it follows by (iii) in Def. 7. Finally, R′α(s′ ,w′ ) and by construction σ and σ′ are equivalent for ψ w.r.t. w and w′ .

Let α ≡ v :=? and again consider interpretations σ and σ′ equivalent for φ w.r.t. s and s′ . Let θ be a witness for s ≃ s′ . If Rα(s,w) then w(v) ∈ U. Since |U A| ≥ |V | + |C| +#P(φ), we can find a 'fresh' element u′ ∈ U A \ (s′ (V \ {v}) ∪C ∪ σ′ (fr(φ))) and set w′ (v) = u′ , while w′ coincides with s′ on all other variables. Then define θ′ as θ but θ′ (w(v)) = u′ . Clearly, θ′ is a witness for w ≃ w′ and σ′ = θ′ ◦ σ. Moreover, the total order ≤w′ can be completed so that item (iii) in Def. 7 is satisfied. Thus, R′α(s′ , w′ ) and σ and σ′ are equivalent for ψ w.r.t. w and w′ .

The inductive steps for α ≡ β′ ; β′′ and α ≡ β′ ∪ β′′ are immediate. The case for α ≡ β∗ can be proved by induction on the length of the path connecting states s and w such that R∗β (s, w), by using the induction hypothesis.

Finally, let α ≡ χ?. Then, Rα(s,w) implies that (M, s, σ) |= χ and w = s. Since σ and σ′ are equivalent for φ w.r.t. s and s′ , and |U A| ≥ |V |+|C|+#P(φ) ≥ |V |+ |C| +#P(χ), we have in particular that σ and σ′ are equivalent for χ (w.r.t. s and s′ ). By item 2 and the induction hypothesis we obtain that (M, s, σ) |= χ iff (MA, s′ , σ′ ) |= χ, that is, R′α(s′ , w′ ) for w′ = s′ .

The proof of item 1.(b) is similar, we only notice that in the base case for α ≡ v :=? we use the fact that the linear order < on Q is dense and without endpoints, to find u ∈ Q that simulates w′ (v) ∈ U A. We now move to prove item 2.

The base case for first-order formulas follows by Lemma 1; the inductive cases for propositional connectives are immediate. In particular, notice that, since |U A| ≥ |V | + |C| + #P(¬ψ) = |V | + |C| +#P(ψ) and |U A| ≥ |V | + |C| + #P(ψ1 ∧ ψ2) ≥ |V | + |C| +#P(φi), for i = 1, 2, the induction hypothesis holds.

For φ ≡ ∀xψ, (M, s, σ) |= ψ iff for all u ∈ adom(s), (M, s, σx u ) |= φ. If θ is a witness to the fact that σ and σ′ are equivalent for φ w.r.t. s and s′ , then interpretations σx u and σ′x θ(u) are equivalent for ψ (also w.r.t. s and s′ ). Moreover, |U A| ≥ |V | + |C| +#P(φ) = |V | + |C| +#P(ψ). Hence, the induction hypothesis holds and it follows that (MA, s′ , σ′x θ(u) ) |= φ. As u is arbitrary and θ is a bijection between adom(s) and adom(s′ ), we obtain (MA, s′ , σ′ ) |= φ.

Suppose that φ ≡ [α]ψ. As regards the ⇐ direction, (M, s, σ) ̸|= φ iff for some w ∈ Rα(s), (M, w, σ) ̸|= ψ. By item 1.a there exists w′ ∈ R′α(s′ ) such that w′ is isomorphic to w, and σ and σ′ are equivalent for ψ w.r.t. w and w′ . Since |U A| ≥ |V |+|C|+#P(φ) ≥ |V |+|C|+#P(ψ), by induction hypothesis (MA,w′ , σ′ ) ̸|= ψ, that is, (MA, s′ , σ′ ) ̸|= φ. The ⇒ direction is proved similarly, by using item 1.b.

By Theorem 2 a state s and its abstraction s′ satisfy the same formulas in FO-DL, whenever the abstract domain U A contains enough elements to mimick transitions from s. Most importantly, U A can be assumed to be finite. However, the linear order < on Q has to be dense, with no endpoints.

Furthermore, we say that DaS M and abstraction MA are bisimilar iff (i) for every s ∈M, there is an isomorphic s′ ∈ MA, and (ii) for every s′ ∈MA, there is an isomorphic s ∈ M. As a consequence of Theorem 2 we obtain the following result.

Corollary 3 Let M = 〈V,C,Q〉 be a DaS with bisimilar abstraction MA = 〈V, C, U A〉. For every FO-DL formula φ, if |U A| ≥ |V | + |C| +#P(φ) then M |= φ iff MA |= φ.

In particular, whenever U A is finite, the number of states in MA is finite as well. Therefore, by Corollary 3 we can verify an FO-DL formula φ on the infinite-state DaS M by model checking the finite abstractionMA (e.g. by translating to propositional DL).

Discussion. We briefly discuss the application of our results to the auction DaS M for n bidders in Section 2.1. Observe that for M = 〈V, {1, 2},Q〉, we have V = ⋃i≤n {bidi, t valuei} ∪ {high, time out}, and therefore |V | = 2(n+1), |C| = 2. Further, for formula (3), we have #P(3) = n2 . Hence, in order to verify (3) it is sufficient to consider an abstract domain U A of finite cardinality |U A| ≥ |V |+|C|+#P(3) = n(n+2)+4. Then, formula (3) can be verified on such abstraction MA, and finally the result can be transfered to M in virtue of Corollary 3.

Furthermore, Corollary 3 gives us some useful insight on a problem related to model checking. Given a class C of DaS and an FO-DL formula φ, the satisfiability problem consists in determining whether φ is satisfied in C, that is, true in some DaS belonging to C. We remarked earlier that every non-empty countable dense linear order without endpoints is order-isomorphic to Q. As a consequence, the satisfiability problem for the class of non-empty countable dense linear orders without endpoints can be reduced to the model checking problem for the rationals Q. In particular, we obtain the following result.

Corollary 4 The satisfiability problem of FO-DL formulas for the class of DaS whose interpretation domain U is a nonempty countable dense linear order without endpoints is decidable.

In future work we plan to extend these results to other classes of DaS and to determine the exact complexity of the model checking and satisfiability problems.

4 Conclusions

In this paper we introduced a formal framework for Dataaware Systems inspired by (first-order) dynamic logic. The data content of a DaS is modelled by a finite set of variables (and constants) that can range over a possibly infinite interpretation domain. As a result, DaS are infinite-state systems in general (Section 2). We showed that DaS are rich enough to express elaborate multi-agent scenarios, including auction-based mechanisms (Section 2.1), and then we considered the verification problem w.r.t. the first-order extension FO-DL of dynamic logic. The main theoretical result of the paper consists in showing that, under specific conditions, the model checking problem for DaS w.r.t. FO-DL is decidable. The decidability result is obtained by defining finite, bisimilar abstractions that preserve the interpretation of FO-DL (Section 3). Hence, to verify an FO-DL formula φ in a concrete, infinite-state DaSM, we build the finite abstraction MA, then model check φ on MA, and finally transfer the verification result toMby virtue of Corollary 3.

We envisage a number of extensions for the present contribution. Propositional Dynamic Logic is one of the success stories of formal methods applied to computer science, with a steady stream of fundamental contributions [Harel, 1984; Harel et al., 2000]. On the other hand, its first-order extensions are much less investigated. In particular, the well-known undecidability results in first-order logic have spawned a wealth of contributions in mathematical logic and theoretical computer science [B¨orger et al., 1997]. For firstorder dynamic logic the situation is even more complex, as many well-known results that hold for first-order logic, fail for its dynamic counterpart, e.g., L¨owenheim-Skolem theorem, completeness, compactness. However, in first-order dynamic logic there has not been a comparable push aimed at singling out decidable and tractable fragments. In future work we plan to individuate further classes of DaS and fragments of FO-DL that have a decidable model checking and satisfiability problems, and study their exact complexity. We deem results along this line valuable to improve the understanding of (first-order) dynamic logics, data-aware systems, and auction-based mechanisms.

Acknowledgments

F. Belardinelli acknowledges the support of the ANR JCJC Project SVeDaS (ANR-16-CE40-0021).