Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems

1 Introduction

Formalisms and techniques based on Multi-Agent Systems (MAS) have made a significant contribution in a number of application areas, including web-services [Singh and Huhns, 2005; Baldoni et al., 2012]. This has taken the form of MASbased architectures [Denti and Omicini, 1999; Omicini et al., 2008; Winikoff, 2009], monitoring methodologies [Lomuscio et al., 2011; Modgil et al., 2009], formal verification [Lomuscio et al., 2012], and many others.

Artifact-centric (AC) systems are a novel paradigm in webservices [Hull, 2008; Hull et al., 2011]. In the artifact approach, now used prominently in business-process modelling and case-based management, structured data and processes live together with equal importance in the service model and the interface descriptions. Structured data pose a considerable challenge from a verification perspective. They entail dealing with infinite state-spaces, which in turn require specification languages supporting quantification, such as first-order temporal logics.

Existing literature on the verification of AC systems [Hariri et al., 2012; Belardinelli et al., 2012b; Deutsch et al., 2009; Gerede and Su, 2007] makes it clear that the model checking problem is typically undecidable, irrespectively of the underlying formalisation. However, the state-of-the-art points to conditions that can be imposed on the semantics of AC systems to obtain decidability. In particular, a condition referred to as "uniformity" is shown to guarantee decidability of systems with bounded runs [Belardinelli et al., 2012a;

Alessio Lomuscio

Department of Computing Imperial College London a.lomuscio@imperial.ac.uk

2012b], even when considering infinite-state systems. The same condition is satisfied by definition by the systems introduced in [Hariri et al., 2012], thus guaranteeing the decidability of the model checking problem for bounded runs. In both cases decidability is shown by means of finite abstractions for infinite models.

A natural open question in the area is therefore whether uniformity is a necessary condition for deciding the model checking problem for AC systems. In this paper we show that this is not the case. Specifically, we show that a sound, albeit incomplete, finite abstraction technique can be given for bounded, non-uniform systems with respect to formulas in the universal fragment of the first-order computation tree logic FO-CTL. As we show, finite abstractions of infinite AC systems can be obtained by defining a suitable counterpart semantics [Brauner and Ghilardi, 2007; Corsi, 2001]. While our results for the universal fragment are positive, we also conclusively show that conditions such as uniformity are required for deciding the model checking problem against the full logic FO-CTL. To this end, we prove that model checking bounded, but non-uniform, AC systems against full FO-CTL is in general undecidable.

The rest of the paper is organised as follows. In Section 2 we fix our notation and give the syntax of the temporal specification language used as well as a semantics for AC systems in terms of artifact-centric quantified interpreted system (AC-QIS). Section 3 explores the model checking problem for bounded, non-uniform AC-QIS, thereby showing this to be undecidable in general. A counterpart semantics for AC systems and related simulation concepts are introduced in Section 4. Section 5 contains the main result of the paper concerning the derivation of finite abstractions for nonuniform, bounded AC-QIS against the universal fragment of FO-CTL. This also contains the decidability result. We conclude in Section 6 by discussing the results and pointing to future work.

2 Preliminaries

In this section we define artifact-centric quantified interpreted systems (AC-QIS), introduce a first-order version of the computation tree logic CTL, and present the model checking problem within this framework. Our notion of AC-QIS is based on [Belardinelli et al., 2011; 2012a], but here we abstract from the agents and their actions. We firstly introduce the basic terminology on databases that will be used throughout the paper as it appears in [Belardinelli et al., 2012a].

Definition 1 (Database schema and instance) A database schema is a finite set D = ¶P1◁q1↪ ▷ ▷ ▷ ↪ Pn◁qn♦ of predicate symbols Pi with arity qi 2 N.

Given a (possibly infinite) interpretation domain U, a Dinstance over U is a mapping D associating each predicate symbol Pi to a finite qi-ary relation on U, i.e., D(Pi) ✓ U qi .

The set D(U) contains all D-instances on the domain U. The active domain ad(D) of a D-instance D is the finite set of all individuals occurring in some predicate interpretation D(Pi). The primed version of a database schema D as above is the schema D0 = ¶P 01 ◁q1↪ ▷ ▷ ▷ ↪ P 0n◁qn♦. Finally, the disjoint union D ⊕ D0 of two D-instances D and D0 is the (D [ D0 )-instance s.t. (i) D ⊕ D0 (Pi) = D(Pi); and (ii) D ⊕ D0 (P 0 i ) = D0 (Pi). We can now introduce the notion of AC-QIS.

Definition 2 (AC-QIS) An artifact-centric quantified interpreted system is a tuple P = hD↪ U↪ S↪ D0↪ !i, where

• ÷ D is the database schema
• ÷ D0 2 D(U) is the initial state
• ÷ U is the interpretation domain
• ÷ !✓ D(U) ⇥D(U) is the transition relation
• ÷ S ✓ D(U) is the set of states reachable from D0 by !

Intuitively, an AC-QIS represents the evolution of a database instance D0 according to the transition relation !. A run r from D 2 S is an infinite sequence D0 ! D1 ! · · · , for D0 = D. For n 2 N, rn = Dn . A state D0 is reachable from D if there exists a run r from r0 = D s.t. ri = D0 for some i ≥ 0. In what follows we assume that the transition relation ! is serial, while S is the set of states reachable from D0. Notice that S can be infinite. Hence, the AC-QIS are infinite-state systems in general.

AC-QIS can be seen as a generalisation of the ArtifactCentric Multi-Agent Systems (AC-MAS) in [Belardinelli et al., 2012a], as the former abstract from the agents and their actions, which determine the transition relation for AC-MAS. AC-QIS are first-order temporal structures that can be used to interpret a quantified version of CTL.

Definition 3 (FO-CTL) Given a set Var of individual variables and a set Con ✓ U of individual constants, the FO-CTL formulas ' on the predicate symbols in a database schema D are defined as follows:

where Pi 2 D and ~t is a qi-tuple of terms, i.e., elements in Var [ Con.

The language FO-CTL is a first-order extension of CTL, where the only function symbols are constants. Free and bound variables are defined as standard, as well as the formulas EX', AF', AG', EF', and EG'. The sublanguage FO-ACTL is the restriction of FO-CTL to the universal modalities AX and AU defined as follows:

An assignment is a function σ : Var 7! U. We denote by σx u the assignment s.t. (i) σx u (x) = u; and (ii) σx u (x0 ) = σ(x0 )

for x0 6= x. Also, we assume a Herbrand interpretation of constants, that is, σ(c) = c for all c 2 Con.

Definition 4 (Semantics of FO-CTL) We define whether an AC-QIS P satisfies a formula ' in a D-instance D according to assignment σ as follows:

(P σ ↪ rk ) ♣= '0 , and for all j, 0  j < k

(P σ ↪D) ♣= A'U'0 iff for all r, if r0 =D then there is k ≥ 0 s.t.

Notice that we adopt an active domain semantics, where quantifiers range over the active domain ad(D) of D.

Finally, we present the model checking problem for ACQIS with respect to the specification language FO-CTL.

Definition 5 (Model Checking Problem) Given an AC-QIS P and an FO-CTL formula ', determine whether there is an assignment σ0 such that (P σ0 ↪D0) ♣= '.

In general, the model checking problem for AC-QIS is undecidable. In [Belardinelli et al., 2012a] the same problem is proved to be decidable for bounded and uniform ACMAS, a subclass of AC-QIS. We introduce both notions in relation to AC-QIS. To do so, we define a notion of isomorphism between D-instances: the D-instances D and D0 are isomorphic, or D ' D0 , iff there exists a bijection ◆ : ad(D) [ Con 7! ad(D0 ) [ Con s.t. (i) ◆ is the identity on Con; and (ii) for every Pi 2 D, for every ~u 2 U qi , ~u 2 D(Pi) iff ◆(~u) 2 D0 (Pi).

Definition 6 (Boundedness and Uniformity) An AC-QIS P is bounded iff there is b 2 N s.t. for all D 2 S, ♣ad(D)♣  b. An AC-QIS P is uniform iff for every D↪D0 ↪D00 2 S, D000 2 D(U), if D ! D0 and D ⊕D0 ' D00 ⊕D000 , then D00 ! D000 .

We remark that boundedness places a restriction on the number of elements appearing in the active domain of each D-instance, not on the number of D-instances in S, which might as well be infinite. Uniformity can intuitively be seen as a fullness condition on AC-QIS: all pairs of D-instances isomorphic to a pair of temporally related D-instances are also temporally related. In [Belardinelli et al., 2012a] both features were shown to entail a decidable model checking problem through abstraction.

3 Undecidability for Bounded AC-QIS

In this section we show that in general the model checking problem for bounded AC-QIS is undecidable. We assume standard definitions of Turing machines and reductions [Papadimitriou, 1994]. Let T = hQ↪ ⌃↪ q0↪ qh↪ δi be a deterministic Turing machine, where Q is the finite set of states, ⌃

is the finite alphabet, q0 2 Q is the initial state, qh 2 Q is the halting state, and δ is the transition function. We assume δ to be a function Q ⇥ ⌃ ! Q ⇥ ⌃ ⇥ ¶L↪ R♦ with δ(q↪ c) = (q0 ↪ c0 ↪ d) representing a transition from state q to state q0 , with symbols c and c0 being read and written respectively, and head direction Left or Right respectively. W.l.o.g. T uses only the righthand half of the tape.

Given the Turing machine T with input string in = in0↪ ▷ ▷ ▷ ↪ ink 2 ⌃⇤ , we define the AC-QIS PT ↪in = hD↪U↪ S↪D0↪!i as follows. Let D be the database schema ¶C◁2↪Q◁1↪ S◁1↪H◁0♦; while U = N [Q[ ⌃. Further, let Dn↪m ⇢ D(U) be the set of D-instances Dn↪m containing exactly one pair (n↪m) in the interpretation of the predicate symbol C, for n↪m 2 N, that is, D(C) = ¶(n↪m)♦. Intuitively, D(C) = ¶(n↪m)♦ indicates that D represents the nth cell in the m-th step of the computation of T on input in; while Q and S encode the state and symbol in the cell respectively. Finally, H is a boolean variable expressing whether the reading/writing head is pointing to the cell.

The initial state D0 is defined, by using infix notation for relations, as D0↪0 = ¶C(0↪ 0)↪Q(q0)↪ S(in0)↪>♦. The transition relation ! for PT ↪in is given as follows: (i) D0↪0 ! D1↪0 where D1↪0 = ¶C(1↪ 0)↪Q(q0)↪ S(in1)↪?♦; (ii) for 1  n < k, Dn↪0 ! Dn+1↪0 if Dn+1↪0 = ¶C(n + 1↪ 0)↪ Q(q0)↪ S(inn+1)↪ ?♦; (iii) for n ≥ k, Dn↪0 ! Dn+1↪0 if Dn+1↪0 = ¶C(n + 1↪ 0)↪ Q(q0)↪ ;↪ ?♦.

• iff:÷ δ(q↪ c) = (q0 ↪ c0 ↪ d), Dn↪m(Q) = ¶q♦, Dn↪m(S) = ¶c♦, Dn↪m(H) = > and Dn↪m+1(Q) = ¶q0 ♦, Dn↪m+1(S) = ¶c0 ♦, Dn↪m(H) = ?; or

Moreover, for n↪m 2 N, d 2 ¶L↪R♦, Dn↪m ! Dn↪m+1

• ÷ δ(q↪ c) = (q0 ↪ c0 ↪ L), Dn+1↪m(Q) = ¶q♦, Dn+1↪m(S) = ¶c♦, Dn+1↪m(H) = >, Dn↪m(Q) = ¶q00 ♦, Dn↪m(S) = ¶c00 ♦, Dn↪m(H) = ? and Dn↪m+1(Q) = ¶q0 ♦, Dn↪m+1(S) = ¶c00 ♦, Dn↪m+1(H) = >; or
• ÷ δ(q↪ c) = (q0 ↪ c0 ↪R), Dn-1↪m(Q) = ¶q♦, Dn-1↪m(S) = ¶c♦, Dn-1↪m(H) = >, Dn↪m(Q) = ¶q00 ♦, Dn↪m(S) = ¶c00 ♦, Dn↪m(H) = ? and Dn↪m+1(Q) = ¶q0 ♦, Dn↪m+1(S) = ¶c00 ♦, Dn↪m+1(H) = >; or
• ÷ Dn-1↪m(H) = Dn+1↪m(H) = ?, Dn↪m(Q) = ¶q00 ♦, Dn↪m(S) = ¶c00 ♦, Dn↪m(H) = ? and Dn↪m+1(Q) = ¶q00 ♦, Dn↪m+1(S) = ¶c00 ♦, Dn↪m+1(H) = ?.

As standard S in PT ↪in is the set of all D-instances reachable from D0. Notice that by definition of the transition relation, ! mimicks the transition function δ. The D instances D0↪0↪ ▷ ▷ ▷ ↪Dk↪0 contain the input as the interpretation of the predicate symbol S; at the beginning of the computation the head is on the initial cell D0↪0. The D instances D0↪m↪ D1↪m↪ ▷ ▷ ▷ mimick the m-th step of the computation of T on in. Further, for each m 2 N, there exists exactly one n 2 N s.t. Dn↪m(H) = >. This reflects the fact that the Turing machine is deterministic.

By the definition of D0 and ! it can readily be seen that the AC-QIS PT ↪in is bounded. In fact, for all D 2 S, ♣ad(D)♣  4. Thus, PT ↪in is indeed a bounded AC-QIS. We can now prove the following result on the AC-QIS PT ↪in.

Lemma 1 PT ↪in ♣= EF Q(qh) iff the Turing machine T halts on input in.

Proof (sketch). The proof relies on the fact that ! represents faithfully the transition function δ. ( If T halts on input in, then there exists a step in the computation of T on input in, say the m-th, where T enters state qh while reading the n-th cell, say. By the definition of PT ↪in this means that for Dn↪m 2 S, Dn↪m(Q) = ¶qh♦. Hence, PT ↪in ♣= EF Q(qh). ) If PT ↪in ♣= EF Q(qh) then there exists Dn↪m 2 S s.t. Dn↪m(Q) = ¶qh♦. Since the transition relation !mimicks the transition function δ, for each k 2 N, the sequence D0↪k↪D1↪k↪ ▷ ▷ ▷ represents the k-th step in the computation of T on input in. In particular, Dn↪m(Q) = ¶qh♦ implies that T reaches the halting state at the m-th step, while reading the n-th cell. Thus, the Turing machine T halts on input in.

As a consequence of the undecidability of the halting problem, we obtain the main result of this section.

Theorem 2 Model checking bounded AC-QIS against FOCTL specifications is undecidable.

Notice that the AC-QIS PT ↪in obtained from the Turing machine T and input in is not uniform. To see this, suppose that δ(q↪ c) = (q0 ↪ c0 ↪ d), Dn↪m = h¶(n↪m)♦↪ ¶q♦↪ ¶c♦↪>i and Dn↪m+1 = h¶(n↪ m + 1)♦↪ ¶q0 ♦↪ ¶c0 ♦↪ ?i. By definition of the transition relation ! we have that Dn↪m ! Dn↪m+1. Moreover, for Dn0 ↪m0 = h¶(n0 ↪m0 )♦↪ ¶q00 ♦↪ ¶c00 ♦↪>i and Dn0 ↪m00 = h¶(n0 ↪m00 )♦↪ ¶q000 ♦↪ ¶c000 ♦↪?i we have that Dn↪m ⊕ Dn↪m+1 ' Dn0 ↪m0 ⊕ Dn0 ↪m00 . However, it is not the case that Dn0 ↪m0 ! Dn0 ↪m00 whenever m00 6= m0 + 1. As a result, the AC-QIS PT ↪in is not uniform in general; therefore the technique developed in [Belardinelli et al., 2012a; Hariri et al., 2012] cannot be applied here.

In the following section we show that, notwithstanding this undecidability result, a decidable, although incomplete, model checking procedure can be given if the specifications are restricted to the universal fragment of FO-CTL.

4 Counterpart Semantics

In this section we introduce a semantics for FO-CTL based on counterpart models. Then, we define a notion of simulation for these systems and show that the simulation relation preserves the interpretation of formulas in the universal fragment of FO-CTL. We firstly introduce counterpart models as a generalisation of AC-QIS.

Definition 7 (c-model) A counterpart model is a tupleM= hS↪ s0↪ !↪ U↪ C↪ Ii s.t. (i) S is a non-empty set of states; (ii) s0 is the initial state; (iii) ! is a serial binary transition relation on S; and (iv) for s↪ s0 2 S,

• ÷ U(s) is a non-empty set of individuals;
• ÷ I is a first-order interpretation, i.e., (i) if P n is an n-ary predicate symbol and s 2 S, then I(P n ↪ s) is an n-ary relation on U(s); and (ii) if c 2 Con, then I(c↪ s) 2 U(s).
• ÷ Cs↪s0 is a serial counterpart relation on U(s) ⇥U(s0 );

Similarly to AC-QIS, the active domain ad(s) of a state s is defined as the set of all individuals occurring in some predicate interpretation I(P n ↪ s). Counterpart models can be thought of as generalisations of AC-QIS, as an AC-QIS can be seen as a c-model on a finite language, where the counterpart relation is the identity, and constants are interpreted as themselves:

Remark 1 Let M = hS↪ s0↪!↪U↪C↪ Ii be a c-model and D a database schema containing some predicate symbols interpreted by I. If for all s↪ s0 2 S, (i) the counterpart relation Cs↪s0 is the identity; and (ii) I(c↪ s) = c, then MD = hD↪ Ss2S U(s)↪ S↪ s0↪ !i is an AC-QIS.

On the other hand, any AC-QIS P can be seen as a cmodel:

Remark 2 Let P = hD↪U↪ S↪D0↪!i be an AC-QIS and consider MP = hS↪ D0↪ !↪ U 0 ↪ C↪ Ii, where for all D↪ D0 2 S (i) U 0 (D) = U; (ii) CD↪D0 is the identity relation; (iii) I(c↪D) = c; and (iv) I(P n ↪D) = D(P n ). Then MP is a c-model.

The notion of run is defined as for AC-QIS. The relation C⇤ is the transitive closure of C, i.e., C ⇤ s↪s0(a↪ a0 ) iff there is a sequence s0 ! ▷ ▷ ▷ ! sk s.t. s0 = s, sk = s0 , and there are a0 ↪ ▷ ▷ ▷ ↪ ak s.t. a0 = a, ak = a0 , and Csi ↪si+1(ai ↪ ai+1 ) for i < k.

To define satisfaction for FO-CTL formulas in counterpart models, we consider typed languages and finitary assignments. This is standard when working in counterpart semantics [Brauner and Ghilardi, 2007; Corsi, 2001]. Specifically, every variable xj 2 Var is a term of type n, or n-term, for n ≥ j; while every constant c 2 Con is an n-term.

• ÷ if P m is an m-ary predicate symbol and ~t is an m-tuple of n-terms, then P m(~t) is an (atomic) n-formula;

Definition 8 (FO-CTLT ) The typed language FO-CTLT contains all n-formulas φ : n, for n 2 N, defined as follows:

• ÷ if ↪ 0 are n-formulas, then ≻ , ! 0 are n-formulas;
• ÷ if ↪ 0 are m-formulas and ~t is an m-tuple of n-terms, then (AX )(~t), (A U 0 )(~t), (E U 0 )(~t) are n-formulas;
• ÷ if is an (n+1)-formula, then 8xn+1 is an n-formula;

The other logical operators are defined as standard. The formula AXφ : n is a shorthand for (AXφ)(x1↪ ▷ ▷ ▷ ↪ xn) : n; similarly for AφUφ0 : n and EφUφ0 : n. In what follows we consider also the sublanguage FO-ACTLT , which is obtained by restricting FO-CTLT to the universal modalities AX and AU. Also, FOT is the non-modal fragment of FO-CTLT .

The meaning of a typed formula φ : n at a state s can intuitively be understood as a subset of U(s)n , i.e., the set of n-tuples satisfying φ : n at s. Therefore, the definition of satisfaction is given by means of finitary assignments, where an n-assignment in s is an n-tuple ~a of elements in U(s). Let t be an n-term, the valuation ~a(t) for the n-assignment ~a is equal to aj if t = xj; otherwise, ~a(t) = an whenever t = c.

Definition 9 (Semantics of FO-CTLT ) The satisfaction relation ♣= for a state s 2 M, a typed formula φ : n and an n-assignment ~a is inductively defined as follows:

where ~a · a⇤ is the (n + 1)-assignment ha1↪ ▷ ▷ ▷ ↪ an↪ a⇤ i. An n-formula φ is true at a state s, or (M↪ s) ♣= φ, iff it is satisfied by every n-assignment; φ is true on a c-model M, orM ♣= φ, iff (M↪ s0) ♣= φ.

Notice that by considering c-models where the counterpart relation is the identity and constants are interpreted as themselves, we have that the relation of satisfaction in Def. 9 reduces to the notion in Def. 4. Thus, c-models can really be seen as a generalisation of AC-QIS. We state this result formally. Firstly, we define a translation ⇡n, for n 2 N, from FO-CTL to FO-CTLT . Given an FO-CTL formula φ and n greater than or equal to the maximum k such that xk occurs in φ, the n-formula ⇡n(φ) in FO-CTLT is inductively defined as follows:

Notice that ⇡n simply renames bound variables in φ. We can now state the following result on the relation between an AC-QIS P and the corresponding c-models MP .

Lemma 3 Let P be an AC-QIS, φ[~x] 2 FO-CTL with free variables ~x, and σ(~x) = ~a. We have that

This result allows us to model check an AC-QIS by verifying the corresponding c-model.

We now present a notion of simulation for counterpart models and we show that it preserves the satisfaction of formulas in FO-ACTLT . Firstly, we introduce some preliminary definitions. In what follows we consider the c-models M = hS↪ s0↪!↪ U↪ C↪ Ii and M0 = hS0 ↪ s00 ↪!0 ↪ U 0 ↪ C 0 ↪ I 0 i, with s 2 S and s0 2 S0 .

Definition 10 A state s0 simulates s, or s ⪯ s0 , iff there exists a surjective mapping ◆ : U(s) ! U 0 (s0 ) s.t. (i) for every constant c, I(c↪ s) = ◆(I(c↪ s0 )); (ii) for every Pi, ~u 2 U(s)qi , ~u 2 I(Pi↪ s) iff ◆(~u) 2 I(Pi↪ s0 ).

Any function ◆ as above is a witness for s ⪯ s0 . We write s ◆⪯ s0 to state this explicitly.

Definition 11 Let ~a 2 U(s)n and ~a0 2 U 0 (s0 )n be nassignments, (s0 ↪~a0 ) simulates (s↪~a), or (s↪~a) ⪯ (s0 ↪~a0 ), iff for some witness ◆, (i) s ◆⪯ s0 ; and (ii) ◆(~a) =~a0 .

We overload the symbol ⪯ for representing the relations in Def. 10 and 11; the difference will be clear from the context. Notice that ⪯ is a transitive relation. Also, simulations preserve the interpretation of FO-formulas:

Lemma 4 If (s↪~a) ⪯ (s0 ↪~a0 ), then for each n-formula φ in FOT ,

Proof (sketch). By induction on the length and type of φ.

We now introduce the notion of simulation on c-models, which is then used to extend the result in Lem. 4 to FOACTLT .

Definition 12 (Simulation) A c-model M0 simulates M, or M ⪯ M0 , iff (i) for every ~a00 2 U 0 (s00 )n there exists ~a0 2 U(s0)n s.t. (s0↪~a0) ⪯ (s00 ↪~a00 ); and (ii) if (s↪~a) ⪯ (s0 ↪~a0 ) then for every t, ~b 2 U(t)n , if s ! t and Cs↪t(~a↪~b), then there are t0 2 S0 , ~b0 2 U(t0 )n s.t. s0 ! t0 , Cs0 ↪t0(~a0 ↪~b0 ), and (t↪~b) ⪯ (t0 ↪~b0 ).

We use the same symbol ⪯ to express a simulation between c-models and states; the difference will be clear from the context. Also notice that, since, according to Remark 2, AC-QIS are a specific subclass of c-models, the definition of simulation for the latter applies also to the former. Further, the simulation relation on c-models preserves the satisfaction of formulas in FO-ACTLT .

Theorem 5 Suppose that M ⪯ M0 and (s↪~a) ⪯ (s0 ↪~a0 ), then for each n-formula φ in FO-ACTLT , we have

Proof (sketch). By induction on the length and type of φ. The base case and the inductive cases for propositional connectives and quantifiers are proved as in Lem. 4. For φ = (AX )(~t), suppose that (M~a ↪ s) 6♣= φ. Then, there exists a run r,~b 2 U(r1 ) s.t. r0 = s, Cs↪r1(~a(ti)↪ bi) and (M~b ↪ r1 ) 6♣= . By definition of simulation there are t0 2 S0 , ~b0 2 U 0 (t0 )n s.t. s0 !0 t0 , C 0s0 ↪t0(~a0 (ti)↪ b0i ), and (r1 ↪~b) ⪯ (t0 ↪~b0 ). Notice that by seriality s0 !0 t0 can be extended to an infinite run r0 s.t. r00 = s0 and r01 = t0 . Further, by induction hypothesis we have that (M0~b0 ↪ r01 ) 6♣= . Thus, (M0~a0 ↪ s0 ) 6♣= φ. The case for φ = (A U 0 )(~t) is proved similarly.

From Thm. 5 we immediately obtain the following result.

Corollary 6 If M⪯M0 , then for every n-formula φ 2 FOACTLT , ~a00 2 U 0 (s00 )n , there exists ~a0 2 U(s0)n s.t.

Proof (sketch). By the definition of simulation for every ~a00 2 U 0 (s00 )n there exists ~a0 2 U(s0)n s.t. (s0↪~a0) ⪯ (s00 ↪~a00 ). Moreover, by Thm. 5 we obtain that (M0~a00↪ s00 ) ♣= φ implies (M~a0 ↪ s0) ♣= φ.

By Lem. 3 and Cor. 6 we can solve the model checking problem for an AC-QIS P and an FO-ACTL formula φ by considering a c-modelM0 that is similar toMP. By Cor. 6, if (M0 ~ a0 0 ↪ s00 ) ♣= ⇡n(φ) for some n-assignment ~ a0 0, then there exists ~a0 2 U(s0) s.t. (M~a0 P ↪ s0) ♣= ⇡n(φ). Moreover, by Lem. 3, if (M~a0 P ↪ s0) ♣= ⇡n(φ) then (P σ ↪ s0) ♣= φ for some assignment σ that agrees with ~a0 on the free variables in φ. Thus, a positive solution to the model checking problem for the abstract c-model M0 implies a positive solution also for the concrete AC-QIS P. In the following section we analyse the conditions under which the abstract c-model M0 is finite.

5 Finite Abstractions

In this section we introduce the abstraction of a c-model M and show that it is similar to M. Further, we identify the conditions under which such abstraction is finite, thus allowing the verification of infinite-state AC-QIS by the results in Section 4.

Firstly, we define [s] as the equivalence class of s according to the symmetric closure ⇡ of the relation ⪯. Further, for s 2 [t], [s↪ a][t] is the equivalence class of (s↪ a) according to the symmetric closure ⇡ of ⪯. Notice that we overload the symbol ⇡ as we did with ⪯; the distinction will be clear from the context. Also, ⇡ is not to be confused with the isomorphism relation '.

Definition 13 (Abstraction) Given a c-model M = hS↪ s0↪!↪U↪C↪ Ii, the abstraction of M is a tuple M0 = hS0 ↪ s00 ↪!0 ↪U 0 ↪C 0 ↪ I 0 i s.t. (i) S0 = ¶[s] ♣ s 2 S♦; (ii) s00 = [s0]; and for every [s]↪ [s0 ] 2 S0 ,

• ÷ [s] !0 [s0 ] iff there are u 2 [s], v 2 [s0 ] s.t. u ! v
• ÷ C 0 [s]↪[s0 ] = ¶([s↪ a][s]↪ [s0 ↪ b][s0 ]) ♣ there are (u↪ a0 ) 2 [s↪ a][s], (v↪ b0 ) 2 [s0 ↪ b][s0 ] and Cu↪v(a0 ↪ b0 )♦
• ÷ U([s]) = ¶[s↪ a][s] ♣ a 2 U(s)♦
• ÷ I 0 (c↪ s) = [s↪ I(c↪ s)][s] and ~ [s↪ a][s] 2 I 0 (P↪ [s]) iff ~a 2 I(P↪ s).

It can be shown that the abstraction of a c-model M is also a c-model. In particular, the interpretation I 0 is welldefined as it is independent from the specific representative: if (s0 ↪ a0 ) 2 ~ [s↪ a][s] , then (s0 ↪ a0 ) ⇡ (s↪ a). In particular, ~a 2 I(P↪ s) iff ~a0 2 I(P↪ s0 ).

Given a c-model M and its abstraction M0 , we define a mapping f : M!M0 s.t. f(s↪~a) = ([s]↪ ~ [s↪ a][s] ). We now prove that the mapping f defines a simulation relation.

Theorem 7 LetMbe a c-model andM0 its abstraction. The relation F((s↪~a)↪ f(s↪~a)) is a simulation between M and M0 .

Proof (sketch). Firstly notice that for every ~ [s0↪ a0][s0] 2 U 0 (s00 )n there exists ~a0 2 U(s0)n and F((s0↪~a0)↪ f(s0↪~a0)). To we show that (s↪~a) ⪯ f(s↪~a), we define a mapping ◆ : U(s) ! U 0 ([s]) s.t. ◆(a) = [s↪ a][s] for a 2 U(s). It is clear that s ◆⪯ [s] by the definition of I 0 . Thus, (s↪~a) ⪯ f(s↪~a). Finally, suppose that for t 2 S and ~b 2 U(t)n , we have that s ! t and Cs↪t(~a↪~b). By the definition of M0 we clearly see that [s] ! [t]. Also, for every a 2 ~a,

(a) The AC-QIS P

(b) The c-modelM0

b 2~b, (s↪ a) 2 [s↪ a][s], (t↪ b) 2 [t↪ b][t] and Cs↪t(a↪ b). Hence, C[s]↪[t]( ~ [s↪ a][s] ↪ ~ [t↪ b][t] ), and F((t↪~b)↪ f(t↪~b)).

By Cor. 6 and Thm. 7 we obtain the following result.

Corollary 8 Let M be a c-model and M0 its abstraction . For every n-formula φ in FO-ACTLT , for every ~a0 2 U(s0),

Now we investigate the problem of determining sufficient conditions for the abstraction of a c-model M to be finite. This will allow the verification of an infinite-state AC-QIS P by model checking the finite abstraction of MP .

Proof (sketch). Notice that if P is bounded, then there exists b 2 N s.t. for every D 2 S, ♣ad(D)♣  b. This means that there is only a finite number of equivalence classes [D] according to relation ⇡. Hence, S0 is finite. Further, since the active domain of each D is finite, there is only a finite number of equivalence classes [D↪ a][D], for a 2 U. Thus, each U([D]) is also finite.

Theorem 9 If P is a bounded AC-QIS, then the abstraction M0 of the c-modelMP is finite.

As a consequence of Cor. 8 and Thm. 9, to verify an FOACTL formula φ on a bounded AC-QIS P, we can model check ⇡n(φ) 2 FO-ACTLT on the finite abstraction of MP. We illustrate the procedure above by an example. Consider the AC-QIS P in Fig. (a), where (i) D = ¶P◁1♦; (ii) U = N; (iii) S = ¶Dn ♣ n 2 N and Dn(P) = ¶n♦♦; (iv) D0 is the initial state; (v) for all n 2 N, Dn ! Dn+1. Firstly, notice that the AC-QIS P is not uniform, as D1 ⊕D2 ' D1 ⊕D3 and D1 ! D2, but not D1 ! D3. Thus, the techniques developed in [Belardinelli et al., 2012a] cannot be applied. Consider also the following specifications in FO-ACTL: χ = 8xAG(P(x) ! AX≻P(x)) and ✓ = 8xAG(P(x) ! AXAG≻P(x)). Since P is infinite-state, χ and ✓ cannot be model checked directly on P.

To define the abstractionM0 of P we observe that for every i↪ j 2 N, Dj ⪯ Di by the witness ◆ that maps j into i, and N ∩ ¶j♦ into N ∩ ¶i♦. Hence, S0 = ¶S♦ and S !0 S. Further, for every i↪ j 2 N, (Dj↪ j) ⪯ (Di↪ i); while for i0 6= i↪ j 0 6= j, (Dj↪ j 0 ) ⪯ (Di↪ i0 ). Hence, we obtain two equivalence classes a = ¶(Dn↪ n) ♣ n 2 N♦ and b = ¶(Dn↪ n0 ) ♣ n 6= n0 ♦. Then the counterpart relation is defined as CS↪S = ¶(a↪ b)↪ (b↪ b)↪ (b↪ a)♦, corresponding respectively to the transitions (Dn↪ n) ! (Dn+1↪ n), (Dn↪ n0 ) ! (Dn+1↪ n0 ) for n0 6= n, n0 6= n + 1, and (Dn-1↪ n) ! (Dn↪ n). Finally, we have I(P↪ S) = ¶a♦. The abstract c-model M0 is illustrated in Fig. (b). We can now model check the typed versions of χ and ✓, namely χT = 8x1AG(P(x1) ! AX≻P(x1)) and

✓T = 8x1AG(P(x1) ! AXAG≻P(x1)), onM0 . Clearly, (M0 ↪ S) ♣= χT , while (M0 ↪ S) 6♣= ✓T . Hence, by Lem. 3 and Cor. 8 we can derive that (P↪ D0) ♣= χ; while nothing can be said about ✓ in P.

We conclude by remarking that in general the abstraction of an AC-QIS as defined in Def. 13 is not an AC-QIS, but a c-model. This motivates the introduction of c-models.

6 Conclusions and FurtherWork

As remarked earlier, a considerable amount of work has focused on the development of verification methodologies for artifact-centric systems [Belardinelli et al., 2012a; 2012b; Deutsch et al., 2009; Gerede and Su, 2007; Hariri et al., 2012]. The-state-of-the-art in the area involves constructing finite abstractions of the artifact-system's infinite state space. So far work in the literature has shown that this process can be conducted whenever the artifact system is bounded and "uniform". In this paper we showed that there are noteworthy cases where this condition can be relaxed. Specifically, we demonstrated that in the case of universal specifications, finite abstractions can be constructed for bounded but non-uniform systems. This leads us to the following considerations.

From the theoretical point of view, it is of interest to ascertain whether a necessary condition exists for finite abstractions. Our current results show that uniformity is not necessary for partial decision procedures, but that at the same time, bounded systems do not in general admit finite abstractions. Still, none of these results are "tight" and it is an open problem whether the existence of finite abstractions can be characterised in terms of system conditions.

From an application standpoint, while uniformity covers a wide range of systems, the corresponding condition on the underlying databases, namely genericity [Abiteboul et al., 1995], is satisfied only by a restricted number of systems. It follows that a large class of data-aware systems, such as those implemented by GSM [Heath et al., 2011], are not "amenable" (in the sense of [Belardinelli et al., 2012b]), hence may generate non-uniform models. Therefore, only the techniques introduced in this paper may be used to model check them. It would be of interest to implement the methodology of this paper into a toolkit for the practical verification of artifact-centric systems. The model checker GSMC [Gonzalez et al., 2012] already targets the verification of artifactcentric systems, but it presently offers no support for data and deals with finite state spaces only. We leave both points above for further work.

Acknowledgements

This research was partly funded by the EC FP7 under grant n. 257593 (ACSI), and by the EPSRC under grant EP/I00520X.