A Computationally-Grounded Semantics for Artifact-Centric Systems and Abstraction Results

1 Introduction

Considerable research in service-oriented computing, including in multi-agent systems approaches to it, has focused on tackling the orchestration and choreography problems [Alonso et al., 2004]. In a nutshell these involve offering a methodology for the seamless interaction of autonomous and distributed services thereby satisfying individual and overall goals in the system. Some of the most compelling contributions to both problems have focused on the use of verification technology. In these approaches orchestration is tackled by means of synthesis, whereas "vanilla" model checking is used to check choreography properties.

While approaches based on model checking are now relatively commonplace in services, recent prominent work [Cohn and Hull, 2009] has emphasised what appear to be severe limitations in the mainstream modelling as considered in the services literature. Specifically, it is of concern that current approaches typically focus either on the process side or on the data side, hence disregarding the interactions between these two equally relevant facets of the system. To overcome these limitations, the concepts of artifacts and artifact-centric systems (ACSs) have been put forward.

Artifacts are structures that "combine data and process in an holistic manner as the basic building block[s]" [Cohn and Hull, 2009], and ACSs are formal descriptions of (complex) workflow schemes based on artifacts.

As a result of treating both data and processes as "firstclass citizens", the usual service composition questions become intrinsically much harder and can no longer been solved by current verification methodology. This is an area where solutions inspired by theoretical work in Artificial Intelligence,

Fabio Patrizi

Department of Computing Imperial College London f.patrizi@imperial.ac.uk

including knowledge representation, have, in our opinion, a fundamental role to play, particularly when combined with verification approaches.

This paper is intended to provide a first foundational stepping stone in this direction. Inspired by well-known contributions in logic and knowledge representation [Fagin et al., 1995], we put forward a formalisations of artifact systems by providing them with a computationally-grounded [Wooldridge, 2000] semantics (Section 2) that we illustrate on a concrete scenario (Section 3). The semantics is used to interpret a quantified language that includes temporal and epistemic modalities to model the temporal evolution of the system's properties including the information the agents hold. In Section 4 we address the model checking problem, which, besides being interesting per se, provides a basis for solutions of many typical problems in this area, including orchestration and choreography. This is a difficult problem as both the quantification domain and the state-space are infinite. We make an initial, yet promising dent into this by giving abstraction results that, in some cases, permit the reduction of the problem to model checking on finite domains.

2 Formal Model

We recall the notion of database and then introduce artifact quantified interpreted systems (A-QIS), which we show to be well-suited to provide a semantics to ACSs.

Definition 1 (Database Schema) A database schema is a set D = {R1, . . . ,Rn}, where each Ri is a relation schema of the form Ri = ri(a1, . . . , aki ), and all ajs are pairwise distinct. For each relation schema Ri we refer to ri as the relation name, aj as the j-th relation attribute, and ki as Ri's (or ri's) arity.

Definition 2 (Database Instance) An instance (or interpretation) D of a database schema D over a possibly infinite interpretation domain V is a set of finite relations D = {R1, . . . , Rn} such that Ri ⊆ V ki , for i = 1, . . . , n. Each Ri is called instance (or interpretation) of (relation schema) Ri.

For a schema D, write ID(V ) (or simply ID, if V is clear from the context) for the set of all D's interpretations over V .

We capture ACSs by using ideas from Intepreted Systems semantics [Fagin et al., 1995] and extensions [Belardinelli and Lomuscio, 2009].

We assume a set Ag = {1, . . . ,m} of agents, a database schema D = {R1, . . . ,Rn}, and an alphabet A containing individual constants c1, c2, . . ., n-ary predicate letters P n 1 , P n 2 , . . . for n ∈ N, as well as all relation schemes R1, . . . ,Rn in D. Further, for each agent i ∈ Ag we introduce a set Li of local states li, l′i , . . ., a set ACTi of actions αi, α′i , . . ., and a protocol function Pi : Li -→ 2Acti . We consider local states, actions and a protocol function for the environment e as well. The set S ⊆ L1 ×. . .×Lm×Le contains the global states of the systems; while Act ⊆ Act1 × · · · ×Actm ×Acte and P = 〈P1, . . . , Pm, Pe〉 are the set of joint actions and the joint protocol respectively. We can now define artifact quantified interpreted systems (A-QIS).

Definition 3 (A-QIS) An artifact quantified interpreted system is a tuple P = 〈D, V, s0, τ, I〉 where:

• for each i ∈ Ag, Di is a view on D and Li = IDi (V ). Also, Le = ID(V );
• V is the interpretation domain of D;
• s0 ∈ S is the initial global state;
• τ : S -→ (Act -→ S) is the transition function, where τ(s)(α) is defined only if α ∈ P(s).
• I is an interpretation of the alphabet A such that: (i) for every constant c ∈ A, I(c) ∈ V ; and (ii) for every predicate letter P n ∈ A, I(P n , s) ⊆ V n . In particular, for each relation schema R, I(R, s) = R.

For s, s′ ∈ S we say that s′ is a successor of s, or s -→ s′ , if there exists α ∈ Act such that s′ = τ(s)(α). A run r is a sequence r = s0 -→ s1 -→ . . . such that si -→ si+1 . For n ∈ N, r(n) is the n-th element in the sequence, i.e., sn . For s, s′ ∈ S we say that s is epistemically indistinguishable from s′ for agent i, or s ∼i s′ , if si = s′i [Fagin et al., 1995].

Observe that A-QISs specialise quantified interpreted systems (QIS), as defined in [Belardinelli and Lomuscio, 2009]. In fact, a QIS can be seen as an A-QIS P = 〈V, s0, τ, I〉 with no database schema, so that the internal structure of local states is left unspecified.

2.1 The First-Order MAS Logic FO-CTLK

Given the set Ag of agents and the alphabet A, the first-order temporal epistemic language Lm contains all individual constants, predicate letters and relation schema in A, individual variables x1, x2, . . ., the connectives ¬ and →, the quantifier ∀, the branching time operators AX, AU and EU, the epistemic operator Ki for each agent i ∈ Ag, and the common knowledge operator C [Fagin et al., 1995]. Lm contains no functional symbols, so the only terms in the language are individual variables and constants.

Definition 4 Formulas in Lm are defined in BNF as follows:

The formulas AXφ and AφUφ′ (resp. EφUφ′ ) are read as "for all paths, at the next step φ" and "for all paths (resp. for some path), φ until φ′ ". Kiφ means "agent i knows φ"; while Cφ is read as "φ is common knowledge". The logical symbols ∧, ∨, ↔ and ∃, as well as the operators AG, AF, EG, EF, and EX are defined as standard. Finally, Eφ is defined as ∧i∈Ag Kiφ, and for n ∈ N, E0φ = φ and En+1φ = EEnφ.

By φ[⃗y] we mean that ⃗y = y1, . . . , yn are all φ's free variables; and φ[⃗y/⃗t] is the formula obtained by substituting simultaneously some, possibly all, free occurrences of ⃗y in φ with ⃗t = t1, . . . , tn while renaming bound variables. As standard, a sentence is a formula with no free variables.

In what follows we consider two fragments of Lm.

Definition 5 Formulas in the ∀ACTLK-fragment of Lm are defined in BNF as follows, where the logical symbols ∨, ∧, AU, and ∃ are taken as primitives:

where AφUφ′ is read as "for all paths, φ release φ′".

The ACTLK-fragment extends the ∀ACTLK-fragment with the following clause:

• if φ is a formula, then ∃xφ is also a formula.

We now define the semantics of Lm formulas in terms of A-QISs. Given an assignment σ from the set of variables in Lm to the individuals in V , the interpretation I σ (t) of an individual term t is defined as σ(t) if t is a variable, or I(t) if t is a constant. Also, σx a is the assignment that maps x to a and coincides with σ on all other variables.

Definition 6 The satisfaction relation |= for φ ∈ Lm, s ∈ S, and an assignment σ is inductively defined as follows:

A formula φ ∈ Lm is true in a state s, or (P, s) |= φ, if for all assignment σ, (P σ , s) |= φ; it is true in an A-QIS P, or P |= φ, if (P, s0) |= φ.

3 The Equipment Purchasing Scenario

We now introduce a scenario, inspired by a real Business Process use-case developed at IBM, which shows the artifactcentric approach at work. Although we do not formally define a general translation procedure from artifact-centric business processes to A-QIS, this formalisation exemplifies how this can be done and, therefore, demonstrates that A-QISs can effectively be employed to reason about real ACSs.

3.1 The Scenario

The employees of a company who need to purchase some equipment must follow a procedure, which involves the following agents: a requester, who needs to purchase the equipments; a buyer, who is in charge of buying the requested items; and some suppliers, who supply the equipment. The process begins when the requester fills out a requisition order with some line items referring to desired products (e.g., a laptop). The requester then submits the order to the buyer, who finds an appropriate supplier for each line item, and prepares a procurement order containing the relevant line items. Procurement orders are then submitted to suppliers, who can either reject or fulfil the received orders. In the former case, the buyer is notified; in the latter, the items are shipped.

Orders are captured by artifacts, i.e., structures containing data fields, and associated with sets of actions enabling data manipulation. Requisition orders contain fields: id, the requisition order identifier; itm, the line item(s) occurring in the order; p ord, the procurement order(s) associated with the requisition order; and status (see below). Procurement orders contain: id, the procurement order identifier; s id, the identifier of the supplier selected by the buyer; itm, the line item(s) occurring in the order; and status (see below).

The evolution of an artifact status field, in response to agent actions, is referred to as the artifact's lifecyle, which accounts for the stage of the process that the artifact is in. Figures 1(a) and 1(b) depict the lifecycles for request and procurement orders in the form of transition systems, where nodes are labelled by the status they represent, and transitions by pairs "ag, op", associating each action (op) with the agent (ag) that can execute it, R standing for requester, B for buyer, and S for supplier. Each request order has 3 possible statuses, namely crt (created), sbb (submitted to buyer), and cld (closed), and 5 transitions: R, create (the requester creates a request order); R, add li ro (the requester adds a line item to the created request order); R, sbm b (the requester submits the order to the buyer); B, prepare (the requester prepares a procurement order for this request order); B, close (the requester closes the request order, when all items are shipped). The lifecycle of procurement orders is similar, though not described here for brevity.

3.2 Formalisation

For simplicity we assume each requisition order contains at most one item; however, A-QISs are sufficiently expressive to overcome this limitation.

Agents. The set of agents is Agt = {1, 2, . . . , nS, e}, where: 1 represents the requester; 2 the buyer; 3, . . . , nS stand for the suppliers; and e represents the environment.

Interpretation Domain. We take V = IDA ∪ IDS ∪ LI as the interpretation domain, where: IDA is an infinite set of artifact identifiers, IDS = {3, . . . , nS} is the finite set of supplier identifiers (see below), and LI is the finite set of all line items, i.e. LI = {monitor, printer, phone}. All these sets are assumed disjoint. Moreover, we take the symbol - ∈ V to represent a null value.

Environment Database Schema. We define the A-QIS environment database schema De = {RO, PO}, where the relations RO and PO are intended to record the information about all request and procurement orders. Their schemes are as follows: RO(id, itm, p ord, status), where: id is the requisition order identifier, itm is the (single) line item occurring in the order, p ord is the (single) procurement order associated with the requisition order, and status is the current status of the order; PO(id, s id, itm, status), where: id is the procurement order identifier, s id is the identifier of the supplier selected by the buyer, itm is the (single) line item in the order, and status is the current order status.

Local States. To model the requester's (i.e., agent 1) localstate space we take the set ID1 (V ) of interpretations of the database D1 = {RO1}, where RO1's schema matches RO's. Similarly, buyer's (i.e., agent 2) local states are interpretations of the database D2 = {RO2, PO2} over V (ID2 (V )) where RO2's and PO2's schemes match RO's and PO's, respectively. As for agents 3, . . . , nS, the suppliers, local states are interpretations of databases Di = {POi} over V , i.e., IDi (V ), for i = 3, . . . , nS, where POi's schema is the same as PO's Finally, as set of environment local states we simply take IDe (V ).

Actions. For conciseness, without loss of generality, we use parametric actions. A parametric action of the form a(p1, . . . , pq), where a is the action name and p1, . . . , pq are its parameters, represents a family of actions containing one ground action per distinct parameter assignment of values from V . As a convention, for an action parameter p, we denote the generic value assigned to p as p. Agents' action sets are defined as follows. For agent 1, we take Act1 = {create, add li ro(id, li), sbm b(id)}, where: create is meant to create a new request order (with unique identifier); add li ro(id, li) is meant to add line item li to the request order identified by id; and sbm b(id) is meant to submit the request order identified by id to the buyer. The action sets for the other agents are similar, but omitted here. As for the environment, we simply have Acte = ∅.

Protocol Functions. We only report the buyer's protocol function, the other agents' are similar, while, Acte being empty, no protocol is defined for the environment. The buyer's protocol P2 : ID2 (V ) -→ 2Act2 is as follows (D2 = {RO2, PO2}). prepare(id, s id) ∈ P2(D2) if there exists a tuple 〈id, itm, p ord, sbb〉 ∈ RO2, and either p ord = - or there exists a tuple 〈p ord, s id, itm, s〉 ∈ PO2 s.t. s ∈ {prp, rej}. This formalises that the buyer can prepare a new procurement order for an existing request order only if the request order is in status sbb, and either no corresponding procurement order has been prepared yet, or, if it has, it is either in status prp (prepared) or rej (rejected). close(id) ∈ P2(D2) if there exists two tuples: 〈id, itm, p ord, sbb〉 ∈ RO2 with p ord ̸= -, and 〈p ord, itm, s id, acc〉 ∈ PO2, that is, the buyer can close only existing request orders whose associated procurement order is accepted; and sbm s(id) ∈ P2(D2)

if there exists a tuple 〈id, s id, itm, prp〉 ∈ PO2, i.e., the buyer can submit (to a supplier) only prepared procurement orders.

Interpretation Function. The interpretation function I is simply defined as the identity on the environment's local state, that is, for s = 〈D1,D2,D3, . . . ,DnS ,De〉 ∈ S, I(s) = De.

Initial State. As for the (global) initial state, we assume all relations are initially empty.

Global Transition Function. First, we define some dependencies between the agents' local states and the environment's. For a global state s = 〈D1,D2,D3, . . . ,DnS ,De〉, with D1 = {RO1}, Di = {POi}, for i = 3, . . . , nS, and De = {RO, PO}, we have: RO1 = RO, D2 = De, and for each i = 3, . . . , nS, 〈id, s id, itm, status〉 ∈ POi iff s id = i and 〈id, s id, itm, status〉 ∈ PO. For simplicity, given a current global state s and a joint action a, we define the successor global state s′ = τ(a)(s) by defining its environment component D′e = {RO′ , PO′ }, as all other components are derivable through the above dependencies. For brevity, we describe only one action.

For a = 〈create,-,-, . . . ,-〉, D′e in s′ is such that PO′e = POe, and RO′e = ROe ∪ {〈id′ ,-,-, crt〉}, with id′ ∈ IDA such that there is no other tuple 〈id, itm, p ord, status〉 ∈ RO such that id = id′ . Informally, when the requester creates a new order, a new request order artifact is created, with a unique identifier.

Once the system has been modelled, it is possible to verify particular specifications on it. For instance, the system described above satisfies formula ϕ1 = AG(∀idr, itm, p ROe(idr, itm, p, cld) → ∃s K2POe(p, s, itm, acc)), which states that a request order can be in state closed only if the buyer knows that the corresponding procurement order has been actually accepted by some supplier (this corresponds to the precondition of action close according to protocol P2). This property intuitively corresponds to a specification that should indeed be satisfied in the scenario considered. Other epistemic specifications of interest can be similarly formalised.

4 Model checking and Abstraction

We would like to be able to verify automatically any formula ϕ in L on a given A-QIS, i.e., to give an effective methodology for answering the model checking query P |= ϕ. The (considerable) difficulty resides in the fact that P is, in general, an infinite structure. To make inroads into this problem we give an abstraction technique for A-QIS by extending the results presented in [Cohen et al., 2009] to the case of infinite models. We present the results obtained in their fullest generality by giving them on structures built on arbitrary sets, rather than specific database views (Def. 3). This corresponds to the general class of quantified interpreted systems (QIS) as defined in [Belardinelli and Lomuscio, 2009]. Given A-QIS are a subclass of QIS, all the results here proved also hold for A-QIS.

4.1 Simulation

The standard notion of simulation for reactive systems states that a system simulates another if every behaviour of the latter is a behaviour of the former [Clarke et al., 1994]. Since ACTL operators quantify over all behaviours (runs), any ACTL property that holds in the simulating system holds also in the simulated system. To extend this preservation property to ∀ACTLK, we require that any epistemic possibility in the simulated system is matched by an epistemic possibility in the simulating system. Similar conditions apply to individuals.

Definition 7 (Sublanguage) Let L and L′ be first-order temporal epistemic languages as in Def. 4, with alphabets A and A′ respectively. L′ is a sub-language of L, or L′ ⊆ L, if A′ ⊆ A.

We now define the notion of simulation for QIS.

Definition 8 (Simulation) Let P = 〈V, s0, τ, I〉 be a QIS on the set Ag of agents and the language L, and let P ′ = 〈V ′ , s′0 , τ ′ , I ′ 〉 be a QIS on the same set Ag of agents and a sub-language L′ ⊆ L. A simulation between P and P ′ is a pair of relations ≃ ⊆ S × S ′ and ≈ ⊆ V × V ′ such that:

• (a) s0 ≃ s′0 ;
• (b) if a ∈ V then there exists a′ ∈ V ′ such that a ≈ a′ ; and if s ≃ s′ then:
• (c) if s -→ u then s′ -→′ u′ for some u′ such that u ≃ u′ ;
• (d) if s ∼i u then s′ ∼′i u′ for some u′ such that u ≃ u′ ;
• (e) for all P n ∈ L′ , if ⃗a ≈ ⃗a′ then ⃗a ∈ I(P n , s) iff ⃗a′ ∈ I ′ (P n , s′ );
• (f) for all c ∈ L′ , I(c) ≈ I ′ (c);

where -→ and -→′ are the transition relations in P and P ′ respectively. If there is a simulation pair between P and P ′ , we say that P ′ simulates P, or P ⪯ P ′ .

According to (a) the initial state in P has to be matched by the initial state in P ′ . Similarly for (b) and individuals. According to (c) and (d) every temporal and epistemic transition in P has to be matched by a transition in P ′ . According to (e) and (f) related states must agree on the sub-language L′ .

Any ∀ACTLK property is preserved from the simulating QIS P ′ to the QIS P being simulated:

Lemma 1 Assume that P ′ simulates P. For any ∀ACTLKformula φ ∈ L′ , if P ′ |= φ then P |= φ.

Lemma 1 follows directly from the following remark:

The proof, omitted here, is by induction on the length of φ.

Differently from the propositional level, we can define a strengthening of the notion of simulation, so that also existential formulas are also preserved.

Definition 9 (Simulation+) A simulation+ between P and P ′ is a pair of relations ≃ ⊆ S × S ′ and ≈ ⊆ V × V ′ such that:

• (a) ≃ and ≈ are a simulation pair between P and P ′ ;
• (b) if a′ ∈ V ′ then there exists a ∈ V such that a ≈ a′ .

If there is a simulation+ pair between P and P ′ , we say that P ′ simulates+ P, or P ⪯+ P ′ .

We can now prove the following strengthening of Lemma 1.

Lemma 2 Assume that P ′ simulates+ P. For any ACTLKformula φ ∈ L′ , if P ′ |= φ then P |= φ.

The result follows from (1), where the inductive case for the existential quantifier makes use of clause (b) in Def. 9. We omit the complete proof for reasons of space.

In the rest of the paper we focus on simulation+ and the ACTLK-fragment.

4.2 Existential Abstraction of QIS

In systems with large state spaces, it is infeasible to verify design requirements by considering all reachable states, even if represented symbolically [Burch et al., 1992]. In existential abstraction [Clarke et al., 1994], one reduces a large, possibly infinite reactive system - referred to as the concrete system - into a possibly smaller reactive system - referred to as the abstract system - by partitioning the system states into equivalence classes. Each equivalence class, called an abstract state, forms a state in the abstract system.

Here, we extend existential abstraction to quantified interpreted systems by abstracting each agent i and the quantification domain V separately. Formally, the abstract QIS is defined as a quotient construction as follows. Assume a quantified interpreted system P over the set Ag of agents and the language L. For each i ∈ Ag assume the equivalence relations ≡i ⊆ Li×Li and ≡i ⊆ ACTi×ACTi. Further, assume an equivalence relation ≡ ⊆ V × V . For l ∈ Li, write [l] for the equivalence class of l w.r.t. ≡i, and [α] for the equivalence class of α ∈ ACTi w.r.t. ≡i. Similarly, [a] is the equivalence class of a ∈ V w.r.t. ≡. Write [s] for 〈[s1], . . . , [sn]〉 and write [⃗α] for 〈[α1], . . . , [αn]〉. Finally, let L′ ⊆ L be a sublanguage of L that does not distinguish between equivalent local states and individuals, i.e.,

• (*) for all P n ∈ L′ , if s ≡ s′ and ⃗a ≡ ⃗a′ then ⃗a ∈ I(P n , s) iff ⃗a′ ∈ I(P n , s′ ).

Definition 10 (Quotient QIS) The quotient of P is the QIS P ′ on the set Ag of agents and the sub-language L′ ⊆ L such that:

1. V ′ = {[a] | a ∈ V };
2. L′i = {[l] | l ∈ Li};
3. ACT ′ i = {[α] | α ∈ ACTi};
4. P ′ i = {〈[l], [α]〉 | 〈l, α〉 ∈ Pi};
5. τ ′ = {〈[s], [⃗α], [s′ ]〉 | 〈s, ⃗α, s′ 〉 ∈ τ};
6. s′0 = [s0];
7. for all P n ∈ L′ , [⃗a] ∈ I ′ (P n , [s]) iff ⃗a ∈ I(P n , s);
8. for all c ∈ L′ , I ′ (c) = [I(c)].

Note that the interpretation I is well defined by condition (*) on the sub-language L′ . Observe that Def. 10 does not specify how the equivalence relations are chosen. This issue is addressed in Section 4.3 below. The important property of quotient systems, however, is that specifications are preserved from abstract systems to concrete ones. This is because the abstract system simulates+ the original system.

Lemma 3 If P ′ is a quotient of P, then P ′ simulates+ P.

Proof sketch. We show that the relations ≃ = {〈s, [s]〉 | s ∈ V } and ≈ = {〈a, [a]〉 | a ∈ V } are a simulation+ pair for P and P ′ . Simulation requirements (a) and (b) follow from 6 and 1 in Def. 10 respectively. Requirement (c) follows from 4 and 5; while requirement (d) follows by the definition of equivalence classes. Simulation requirements (e) and (f) follow from 7 and 8 respectively. Finally, the simulation+ requirements (b) in Def. 9 trivially hold.

Since the abstract system simulates+ the concrete system, design requirements expressed in ACTLK are preserved.

Theorem 4 (Preservation) Let P ′ be a quotient of the QIS P. For any ACTLK-formula φ in L′ ⊆ L, if P ′ |= φ then P |= φ.

When applying the theorem, the challenge is to choose suitable equivalence relations ≡i on local states and actions. We provide a partial answer in the following section.

4.3 Constructive Abstraction

In this section we introduce a methodology for defining the equivalence relations defined in the previous section. In what follows we fix a sub-language L′ of the first-order temporal epistemic language Lm, and a QIS P. We first define equivalences on the set V n of n-tuples of individuals.

Definition 11 (Equivalence on tuples) Let s ∈ S and let ⃗a, ⃗b be n-tuples in V n . We say that ⃗a and⃗b are equivalent in s, or ⃗a ∼s ⃗b, if for all P n ∈ L′ , ⃗a ∈ I(P n , s) iff ⃗b ∈ I(P n , s).

We can easily check that the relation ∼s is indeed an equivalence relation for every s ∈ S.

Definition 12 (Equivalence on individuals) Let s ∈ S and let a, b be individuals in V . We say that a and b are equivalent in s, or a ≡s b, if for all ⃗a, ⃗a′ ∈ V n , if ⃗a′ is obtained from⃗a by uniformly substituting a with b, then ⃗a ∼s ⃗a′ .

From the fact that ∼s is an equivalence relation we can derive that also ≡s is an equivalence relation for s ∈ S.

We now define the equivalence relation on states.

Definition 13 (Equivalence on states) Two states s, s′ ∈ S are equivalent , or s ≡ s′ , if for all P n ∈ L′ , for all ⃗a ∈ V n , ⃗a ∈ I(P n , s) iff ⃗a ∈ I(P n , s′ ).

We can now introduce the abstract model obtained from the QIS P.

Definition 14 (Abstract model) Given the QIS P = 〈V, s0, τ, I〉 we define an abstract model M′ = 〈V ′ , [s0], τ ′ , I ′ 〉 such that:

• S ′ = {[s] | s ∈ S};
• for each [s] ∈ S ′ , V ′ ([s]) = {[a]s | a ∈ V };
• for any [s], [s′ ] ∈ S, [s] -→ [s′ ] if s -→ s′ ;
• for P n ∈ L′ , ⃗ [a]s ∈ I ′ (P n , [s]) iff ⃗a ∈ I(P n , s).

By definition of the individuals in each V ′ ([s]) we can prove that the interpretation I ′ is well-defined and independent from the particular choice of representatives for the equivalence classes in V ′ ([s]).

Hereafter we introduce the satisfaction relation for the abstract model.

Definition 15 The satisfaction relation |= for φ ∈ L′ , [s] ∈ M′ , and an assignment σ is defined as in Def. 6, but for the following clauses:

Now, we can prove the following result onM′ .

Lemma 5 The abstract model M′ simulates+ P

Proof sketch. The proof consists in showing that the relations ≃ = {〈s, [s]〉 | s ∈ S} and ≈ = {〈a, [a]s〉 | a ∈ V, s ∈ S} are a simulation+ pair for P andM′ , and it is similar to Lemma 3.

The next result is immediate from Lemmas 2 and 5.

Lemma 6 For every ACTLK-formula φ in L′ , if M′ |= φ then P |= φ.

Thus, we have obtained an effective way of constructing the quotient system M′ starting from P and L′ . More in detail, given a ∀ACTLK-formula φ to be model checked on P, L′ can be thought of as the sub-language of L consisting of all predicate letters and constants in φ.

Finally, we observe that if a QIS P has infinitely many states and individuals, then also the abstract model M′ will in general be infinite both in states and individuals. However, the construction above does in some cases generate finite approximations.

The proof is immediate by definition ofM′ fromP.

We have therefore identified a non-trivial case (infinite S and finite V ) in which the technique presented above generates a feasible model checking problem. Additionally, observe that in the case of finite S and infinite V if all state interpretations are finite (e.g., I maps states into database instances) we also obtain, as result of the abstraction process, a finite V ′ inM ′ .

5 Conclusions

In this paper we have put forward a computationallygrounded semantics for artifact systems and illustrated its use in the context of a temporal epistemic specification language. This is intended to provide a basis for model checking these systems in combination with suitable abstraction techniques. We have provided a first set of results in this context and shown that, at least in certain cases of interest, finite abstractions of artifact-systems can be obtained. A limitation of the results presented is that not in all cases finite abstractions are generated. In verification this is known to be a very severe challenge and is therefore to be expected to appear here as well. To surmount these difficulties, our future work includes the development of techniques such as data independence [Wolper, 1986] in the context of A-QIS, and the investigation on abstraction schemes similar to [Deutsch et al., 2009] by relaxing the completeness requirement.

In service-oriented computing, to the best of our knowledge, very few attempts exist to reduce data-aware infinite state systems to finite ones. Noteworthy examples are [Deutsch et al., 2009], [Berardi et al., 2005], and [Cangialosi et al., 2010], where different restrictions on input models and less expressive specifications are used. Furthermore, these works focus on finding decidable fragments from the synthesis and verification point of view, whereas the approach here presented offers a first foundational basis for data abstraction in ACSs for practical model checking.

Acknowledgements. The research leading to these results has received funding from the EC FP7 under grant agreements n. 235329 and n. 257593, and from the EPRSC grant EP/I00520X.