# verification_of_agentbased_artifact_systems__6fd5773e.pdf

Journal of Artificial Intelligence Research 51 (2014) Submitted 04/14; published 10/14

Verification of Agent-Based Artifact Systems

Francesco Belardinelli BELARDINELLI@IBISC.FR Laboratoire Ibisc, Universit e d Evry, France Alessio Lomuscio A.LOMUSCIO@IMPERIAL.AC.UK Department of Computing, Imperial College London, UK Fabio Patrizi FABIO.PATRIZI@DIS.UNIROMA1.IT Dipartimento di Ingegneria Informatica, Automatica e Gestionale A. Ruberti Universit a di Roma La Sapienza , Italy

Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycles, accounting respectively for the relational structure of the artifacts states and their possible evolutions over time. In this paper we put forward artifact-centric multi-agent systems, a novel formalisation of artifact systems in the context of multi-agent systems operating on them. Differently from the usual process-based models of services, we give a semantics that explicitly accounts for the data structures on which artifact systems are defined. We study the model checking problem for artifact-centric multi-agent systems against specifications expressed in a quantified version of temporal-epistemic logic expressing the knowledge of the agents in the exchange. We begin by noting that the problem is undecidable in general. We identify a noteworthy class of systems that admit bisimilar, finite abstractions. It follows that we can verify these systems by investigating their finite abstractions; we also show that the corresponding model checking problem is EXPSPACE-complete. We then introduce artifact-centric programs, compact and declarative representations of the programs governing both the artifact system and the agents. We show that, while these in principle generate infinite-state systems, under natural conditions their verification problem can be solved on finite abstractions that can be effectively computed from the programs. We exemplify the theoretical results here pursued through a mainstream procurement scenario from the artifact systems literature.

1. Introduction

Much of the work in the area of reasoning about knowledge involves the development of formal techniques for the representation of epistemic properties of rational actors, or agents, in a multiagent system (MAS). The approaches based on modal logic are often rooted on interpreted systems (Parikh & Ramanujam, 1985), a computationally grounded semantics (Wooldridge, 2000) used for the interpretation of several temporal-epistemic logics. This line of research was thoroughly explored in the 1990s leading to a significant body of work (Fagin, Halpern, Moses, & Vardi, 1995; Meyer & van der Hoek, 1995). A recent topic of interest has been the development of automatic techniques, including model checking (Clarke, Grumberg, & Peled, 1999), for the verification of temporal-epistemic specifications for the autonomous agents in a MAS (Gammie & van der Meyden, 2004; Lomuscio, Qu, & Raimondi, 2009; Kacprzak, Nabialek, Niewiadomski, Penczek, P olrola, Szreter, Wozna, & Zbrzezny, 2008). This has led to developments in a number of areas traditionally outside artificial intelligence, knowledge representation and MAS, including

c 2014 AI Access Foundation. All rights reserved.

BELARDINELLI, LOMUSCIO & PATRIZI

security (Dechesne & Wang, 2010; Ciobaca, Delaune, & Kremer, 2012), web-services (Lomuscio, Penczek, Solanki, & Szreter, 2011) and cache-coherence protocols in hardware design (Baukus & van der Meyden, 2004). The ambition of the present paper is to offer a similar change of perspective in the area of artifact systems (Cohn & Hull, 2009), a growing topic in Service-Oriented Computing (SOC). Artifacts are structures that combine data and process in an holistic manner as the basic building block[s] (Cohn & Hull, 2009) of systems descriptions. Artifact systems are services constituted by complex workflow schemes based on artifacts which the agents interact with. The data component is given by the relational databases underpinning the artifacts in a system, whereas the workflows are described by lifecycles associated with each artifact schema. While in the standard service paradigm services are made public by exposing their process interfaces, in artifact systems both the data structures and the lifecycles are advertised. Services are composed in a hub where operations on the artifacts are executed. Implementations of artifact systems, such as the IBM engine BARCELONA (Heath et al., 2013), provide a hub where service choreography and service orchestration (Alonso, Casati, Kuno, & Machiraju, 2004) are carried out. Artifact systems are beginning to drive new application areas, such as case management systems (Marin, Hull, & Vacul ın, 2013). However, we identify two shortcomings in the present stateof-the-art. Firstly, the artifact systems literature (Bhattacharya, Gerede, Hull, Liu, & Su, 2007; Deutsch, Hull, Patrizi, & Vianu, 2009; Hull, 2008; Nooijen, Fahland, & Dongen, 2013) focuses exclusively on the artifacts themselves. While there is obviously a need to model and implement the artifact infrastructure, in order to be able to reason comprehensively about artifact systems, there is also a need to account for the agents implementing the services in the system, as it is normally done in the area of reasoning about services (Baresi, Bianculli, Ghezzi, Guinea, & Spoletini, 2007). Secondly, there is a pressing demand to provide the hub with automatic choreography and orchestration capabilities. It is well-known that choreography techniques can be leveraged on automatic model checking techniques; orchestration can be recast as a synthesis problem, which, in turn, can also benefit from model checking technology. However, while model checking and its applications are relatively well-understood in plain process-based modelling, the presence of data makes these problems much harder and virtually unexplored. Additionally, infinite domains in the underlying databases lead to infinite state-spaces and undecidability of the model checking problem. The aim of this paper is to make a concerted contribution to both problems above. Firstly, we provide a computationally grounded semantics to systems comprising the artifact infrastructure and the agents operating on it. We use this semantics to interpret a temporal-epistemic language with first-order quantifiers to reason about the evolution of the hub as well as the knowledge of the agents in the presence of evolving, structured data. We observe that the model checking problem for these structures is undecidable in general and analyse a notable decidable fragment. For these we derive finite abstractions to infinite-state artifact systems, thereby presenting a technique for their effective verification. We evaluate this methodology by studying its computational complexity and by demonstrating its use on a well-known scenario from the artifact systems literature.

1.1 Artifact-Centric Systems

Service-oriented computing is concerned with the study and development of distributed applications that can be automatically discovered and composed by means of remote interfaces. A point of distinction over more traditional distributed systems is the interoperability and connectedness of ser-

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

vices and the shared format for both data and remote procedure calls. Two technology-independent concepts permeate the service-oriented literature: orchestration and choreography (Alonso et al., 2004; Singh & Huhns, 2005). Orchestration involves the ordering of actions of possibly different services, facilitated by a controller or orchestrator, to achieve a certain overall goal. Choreography concerns the distributed coordination of different actions through publicly observable events to achieve a certain goal. A MAS perspective (Wooldridge, 2001) is known to be particularly helpful in service-oriented computing in that it allows us to ascribe information states and private or common goals to the various services. Under this view the agents of the system implement the services and interact with one another in a shared infrastructure or environment. A key theoretical problem in SOC is to devise effective mechanisms to verify that service composition is correct against some specification. Techniques based on model checking (Clarke et al., 1999) and synthesis (Berardi, Cheikh, Giacomo, & Patrizi, 2008) have been put forward to solve the composition and orchestration problem for services described and advertised at interface level through finite state machines (Calvanese, De Giacomo, Lenzerini, Mecella, & Patrizi, 2008). More recently, attention has turned to services described by languages such as WS-BPEL (Alves et al., 2007), which provide potentially unbounded variables in the description of the service process. Again, model checking approaches have successfully been used to verify complex service compositions (Bertoli, Pistore, & Traverso, 2010; Lomuscio, Qu, & Solanki, 2012). While WS-BPEL provides a model for services with variables, the data referenced by them is non-permanent. The area of data-centric workflows (Hull et al., 2009; Nigam & Caswell, 2003) evolved as an attempt to provide support for permanent data, typically present in the form of underlying databases. Although usually abstracted away, permanent data is of central importance to services, which typically query data sources and are driven by the answers they obtain; see, e.g., (Berardi, Calvanese, De Giacomo, Hull, & Mecella, 2005). Therefore, a faithful model of a service behaviour cannot, in general, disregard this component. In response to this, proposals have been made in the workflows and service communities in terms of declarative specifications of datacentric services that are advertised for automatic discovery and composition. The artifact-centric approach (Cohn & Hull, 2009) is now one of the leading emerging paradigms in the area. Artifactcentric systems can be presented along four dimensions (Hull, 2008; Hull et al., 2011). Artifacts are the holders of all structured information available in the system. In a businessoriented scenario this may include purchase orders, invoices, payment records, etc. Artifacts may be created, amended, and destroyed at run time; however, abstract artifact schemas are provided at design time to define the structure of all artifacts to be manipulated in the system. Intuitively, external events cause changes in the system, including in the value of artifact attributes. The evolution of artifacts is governed by lifecycles. These capture the changes that an artifact may go through from creation to deletion. Intuitively, a purchase order may be created, amended and operated on before it is fulfilled and its existence in the system terminated: a lifecycle associated with a purchase order artifact formalises these transitions. Services are seen as the actors operating on the artifact system. They represent both human and software actors, possibly distributed, that generate events on the artifact system. Some services may own artifacts, and some artifacts may be shared by several services. However, not all artifacts, or parts of artifacts, are visible to all services. Views and windows respectively determine which parts of artifacts and which artifact instances are visible to which service. An artifact hub is a system that maintains the artifact system and processes the events generated by the services.

BELARDINELLI, LOMUSCIO & PATRIZI

Services generate events on the artifact system according to associations. Typically these are declarative descriptions providing the precondition and post-conditions for the generation of events. These generate changes in the artifact system according to the artifact lifecycles. Events are processed by a well-defined semantics (Damaggio, Hull, & Vacul ın, 2011; Hull et al., 2011) that governs the sequence of changes an artifact system may undertake upon consumption of an event. Such a semantics, based on the use of Prerequisite-Antecedent-Consequent (PAC) rules, ensures acyclicity and full determinism in the updates on the artifact system. GSM is a declarative language that can be used to describe artifact systems. BARCELONA is an engine that executes GSM-based artifact systems (Heath et al., 2013). The above is a partial and incomplete description of the artifact paradigm. We refer to the literature for more details (Cohn & Hull, 2009; Hull, 2008; Hull et al., 2011). As it will be clear in the next section, in line with the agent-based approach to services, we will use agent-based concepts to model services. The artifact system will be represented as an environment, constituted by evolving databases, upon which the agents operate; lifecycles and associations will be modelled by local and global transition functions. The model is intended to incorporate all artifact-related concepts including views and windows. In view of the above in this paper we address the following questions. How can we give a transition-based semantics for artifacts and agents operating on them? What language should we use to specify properties of the agents and the artifacts themselves? Can we verify whether or not an artifact system satisfies certain properties? As this will be shown to be undecidable, can we find suitable fragments on which this question can always be answered? If so, what is the resulting complexity? Can we provide declarative specifications for the agent programs so that these can be verified by model checking? Lastly, can this technique be used on mainstream scenarios from the SOC literature?

1.2 Related Work

As stated above, virtually all current literature on artifact-centric systems focuses on properties and implementations of the artifact systems as such. Little or no attention is given to the actors of the system, whether they are human or artificial agents. A few formal techniques have, however, been put forward to verify the core, non-agent aspects of the system; in the following we briefly compare these to this contribution. To our knowledge the verification of artifact-centric business processes was first discussed by Bhattacharya et al. (2007), where reachability and deadlocks are phrased in the context of artifactcentric systems and complexity results for the verification problem are given. Even disregarding the agent-related aspects here investigated, the present contribution differs markedly from their work by employing a more expressive specification language and by putting forward effective abstraction procedures for verification. Gerede and Su (2007) study a verification technique for artifact-centric systems against a variant of computation-tree logic. The decidability of the verification problem is proven for the language considered under the assumption that the interpretation domain is bounded. Decidability is also shown for the unbounded case by making restrictions on the values that quantified variables can range over. In the work here presented we also work on unbounded domains, but do not require the restrictions present therein: we only insist on the fact that the number of distinct values in the system does not exceed a given threshold at any point in any run. Most importantly, the interplay

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

between quantification and modalities here considered allows us to bind and use variables in different states. This is a major difference as this feature is very expressive and known to lead potentially to undecidability. In a related line of research the verification problem for artifact systems against two variants of first-order linear-time temporal logic is considered (Deutsch et al., 2009; Damaggio, Deutsch, & Vianu, 2012). Decidability of the verification problem is retained by imposing syntactic restrictions on both the system description and the specification to check. This effectively limits the way in which new values introduced at every computational step can be used by the system. Properties based on arithmetic operators are also considered (Damaggio et al., 2012). While there are elements of similarity between these approaches and the one we put forward here, including the fact that the concrete interpretation domain is replaced by an abstract one, there are also significant differences. Firstly, our setting is branching-time and not linear-time thereby resulting in different expressive power. Secondly and most importantly, differently from similar contributions (Deutsch et al., 2009; Damaggio et al., 2012), we impose no constraints on nested quantifiers or on their interaction with temporal modalities. In contrast, Damaggio et al. admit only a guarded form of quantification on state formulas, and universal quantification at the outermost syntactic level of the formula, over the free variables of state formulas. These two restrictions represent a major, crucial difference with respect to the present work, in that the former syntactical restrictions prevent representing the interaction between data at different states, which is instead expressible in the present work. Our branching time setting also requires a different abstraction technique. Indeed, the approach above (Deutsch et al., 2009; Damaggio et al., 2012) is based on the construction of a counterexample to the formula to be checked, a fact that is technically made possible by two key factors: (i) the exclusive use of universal quantification over paths, guaranteed by the use of linear-time logics; (ii) the syntactic restriction on quantifiers over values, which permits only universal quantifiers to include temporal modalities within their scope. None of such features is required in our work. Namely, we allow both existential and universal quantification over paths to be present (although in a CTL fashion), and we do not put any restriction on the use of first-order quantifiers. Additionally, the abstraction results we present here are given in general terms on the semantics of declarative programs and do not depend on a particular presentation of the system. Finally, following an approach similar to ours, Bagheri Hariri et al. (2013) give conditions for the decidability of the model checking problem for data-centric dynamic systems, i.e., dynamic systems with relational states. In this case the specification language used is a first-order version of the µ-calculus. While our temporal fragment is subsumed by the µ-calculus, the two specification languages have different expressive power, since we use indexed epistemic modalities as well as a common knowledge operator. To retain decidability, like we do here, the authors assume a constraint on the size of the states. However, differently from this contribution, Bagheri Hariri et al. also assume limited forms of quantification whereby only individuals persisting in the system evolution can be quantified over. We do not make this restriction here. Irrespective of what above, the most important feature that characterises our work is that the set-up is entirely based on epistemic logic and multi-agent systems. We use agents to represent the autonomous services operating in the system and agent-based concepts play a key role in the modelling, the specifications, and the verification techniques put forward. Differently from all approaches presented above we are not only concerned with whether the artifact system meets a particular specification. Instead, we also wish to consider what knowledge the agents in the system acquire by interacting among themselves and with the artifact system during a system run.

BELARDINELLI, LOMUSCIO & PATRIZI

Additionally, the abstraction methodology put forward is modular with respect to the agents in the system, that is, first we define abstract agents and then compose them together to obtain the abstract system. These features enable us to give constructive procedures for the generation of finite abstractions for artifact-centric programs associated with infinite models. We are not aware of any work in the literature tackling any of these aspects.

This paper combines and expands our preliminary results on artifact-centric systems (Belardinelli, Lomuscio, & Patrizi, 2011a, 2011b, 2012a, 2012b). In particular, the technical set up of artifacts and agents is different from that of our preliminary studies and makes it more natural to express artifact-centric concepts such as views. Differently from our previous attempts, we here incorporate an operator for common knowledge and provide constructive methods to define abstractions. We also consider the complexity of the verification problem, previously unexplored, and evaluate the technique in detail on a case study.

1.3 Scheme of the Paper

The rest of the paper is organised as follows. In Section 2 we introduce artifact-centric multiagent systems (AC-MAS), the semantics we will be using throughout the paper to describe agents operating on an artifact system. In the same section we put forward FO-CTLK, a first-order logic with knowledge and time to reason about the evolution of the knowledge of the agents and the artifact system. This enables us to propose a satisfaction relation based on the notion of bounded quantification, define the model checking problem, and highlight some properties of isomorphic states. An immediate result we will explore concerns the undecidability of the model checking problem for AC-MAS in their general setting. Section 3 is devoted to identifying a subclass of AC-MAS that admits a decidable model checking problem against full FO-CTLK specifications. The key finding here is that bounded and uniform AC-MAS, a class identified by studying a strong bisimulation relation, admit finite, truth-preserving abstractions for any FO-CTLK specification. In Section 3.4 we explore the verification problem further and also investigate its complexity thereby showing it to be EXPSPACE-complete. We turn our attention to artifact programs in Section 4 by defining the concept of artifact-centric programs. We define them through natural, first-order preconditions and post-conditions in line with the artifact-centric approach. We give a semantics to them in terms of AC-MAS and show that their generated models are precisely those uniform AC-MAS studied earlier in the paper. It follows that, under some boundedness conditions which can be naturally expressed, the model checking problem for artifact-centric programs is decidable and can be executed on finite models. Section 4.2 reports a scenario from the artifact systems literature. This is used to exemplify the technique by providing finite abstractions that can be effectively verified. We conclude in Section 5 where we consider the limitations of the approach and point to further work.

2. Artifact-Centric Multi-agent Systems

In this section we formalise artifact-centric systems and state their verification problem. As data and databases are equally important constituents of artifact systems, our formalisation of artifacts relies on them as underpinning concepts. However, as discussed in the previous section, we here give prominence to agent-based concepts. As such, we define our systems as comprising both the artifacts and the agents interacting with it.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

A standard paradigm for logic-based reasoning about agents is interpreted systems (Parikh & Ramanujam, 1985; Fagin et al., 1995). In this setting agents are endowed with private local states and evolve by performing actions according to an individual protocol. As data play a key part, as well as to allow us to specify properties of the artifact system, we will define the agents local states as evolving database instances. We call this formalisation artifact-centric multi-agent systems (ACMAS). AC-MAS enable us to represent naturally and concisely concepts much used in the artifact paradigm such as the one of view discussed earlier. Our specification language will include temporal-epistemic logic but also quantification over a domain so as to represent the data. This is an usual verification setting, so we will formally define the model checking problem for this set up.

2.1 Databases and First-Order Logic

As discussed above, we use databases as the basic building blocks for defining the states of the agents and the artifact system. We here fix the notation and terminology used. We refer to the literature for more details on databases (Abiteboul, Hull, & Vianu, 1995).

Definition 2.1 (Database Schemas) A (relational) database schema D is a set {P1/q1, . . . , Pn/qn} of relation symbols Pi, each associated with its arity qi N.

Instances of database schemas are defined over interpretation domains, i.e., sets of individuals.

Definition 2.2 (Database Instances) Given a countable interpretation domain U and a database schema D, a D-instance over U is a mapping D associating each relation symbol Pi D with a finite qi-ary relation over U, i.e., D(Pi) Uqi.

The set of all D-instances over a countable interpretation domain U is denoted by D(U). We simply refer to instances whenever the database schema D is clear by the context. The active domain of an instance D, denoted as adom(D), is the set of all individuals in U occurring in some tuple of some predicate interpretation D(Pi). Observe that, since D contains a finite number of relation symbols and each D(Pi) is finite, so is adom(D). Also, in the rest of the paper we assume that the interpretation domains are always countable without explictly mentioning this fact. To fix the notation, we recall the syntax of first-order formulas with equality and no function symbols. Let Var be a countable set of individual variables and Con be a finite set of individual constants. A term is any element t Var Con.

Definition 2.3 (FO-formulas over D) Given a database schema D, the formulas ϕ of the firstorder language LD are defined by the following BNF grammar:

ϕ ::= t = t | Pi(t1, . . . , tqi) | ϕ | ϕ ϕ | xϕ

where Pi D, t1, . . . , tqi is a qi-tuple of terms and t, t are terms.

We assume = to be a special binary predicate with fixed obvious interpretation. To summarise, LD is a first-order language with equality over the relational vocabulary D with no function symbols and with finitely many constant symbols from Con. Observe that considering a finite set of constants is not a limitation. Indeed, since we will be working with finite sets of formulas, Con can always be defined so as to be able to express any formula of interest.

BELARDINELLI, LOMUSCIO & PATRIZI

In the following we use the standard abbreviations , , , and =. Also, free and bound variables are defined as standard. For a formula ϕ we denote the set of its variables as var(ϕ), the set of its free variables as free(ϕ), and the set of its constants as con(ϕ). We write ϕ( x) to list explicitly in arbitrary order all the free variables x1, . . . , xℓof ϕ. By slight abuse of notation, we treat x as a set, thus we write x = free(ϕ). A sentence is a formula with no free variables. Given an interpretation domain U such that Con U, an assignment is a function σ : Var 7 U. For an assignment σ, we denote by σ x u the assignment such that: (i) σ x u (x) = u; and (ii) σ x u (x ) = σ(x ), for every x Var different from x. For convenience, we extend assignments to constants so that σ(t) = t, if t Con; that is, we assume a Herbrand interpretation of constants. We can now define the semantics of LD.

Definition 2.4 (Satisfaction of FO-formulas) Given a D-instance D, an assignment σ, and an FO-formula ϕ LD, we inductively define whether D satisfies ϕ under σ, written (D, σ) |= ϕ, as follows:

(D, σ) |= Pi(t1, . . . , tqi) iff σ(t1), . . . , σ(tqi) D(Pi) (D, σ) |= t = t iff σ(t) = σ(t ) (D, σ) |= ϕ iff it is not the case that (D, σ) |= ϕ (D, σ) |= ϕ ψ iff (D, σ) |= ϕ or (D, σ) |= ψ (D, σ) |= xϕ iff for all u adom(D), we have that (D, σ x u ) |= ϕ

A formula ϕ is true in D, written D |= ϕ, iff (D, σ) |= ϕ, for all assignments σ.

Observe that we adopt an active-domain semantics, that is, quantified variables range only over the active domain of D. We claim that this form of quantification is sufficient to express specifications of interest (see Section 4.2) while retaining decidability. Also notice that constants are interpreted rigidly; so, two constants are equal if and only if they are syntactically the same. In the rest of the paper, we assume that every interpretation domain includes Con. Also, as a usual shortcut, we write (D, σ) |= ϕ to express that it is not the case that (D, σ) |= ϕ. Finally, we introduce the operator on D-instances that will be used later in the paper. Let the primed version of a database schema D be the schema D = {P 1/q1, . . . , P n/qn} obtained from D by syntactically replacing each predicate symbol Pi with its primed version P i of the same arity.

Definition 2.5 ( Operator) Given two D-instances D and D , we define D D as the (D D )- instance such that D D (Pi) = D(Pi) and D D (P i) = D (Pi).

Intuitively, the operator defines a disjunctive join of the two instances, where relation symbols in D are interpreted according to D, while their primed versions are interpreted according to D .

2.2 Artifact-Centric Multi-agent Systems

In the following we introduce the semantic structures that we will use throughout the paper. We define an artifact-centric multi-agent system as a system comprising an environment representing all artifacts and a finite set of agents interacting with such environment. As agents have views of the artifact state, i.e., projections of the status of particular artifacts, we assume that the building blocks of their private local states are also modelled as database instances. In line with the interpreted systems semantics (Fagin et al., 1995) not everything in the agents states needs to be present in the environment; a portion of it may be entirely private and not replicated in other agents states. So, we start by introducing the notion of agent.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Definition 2.6 (Agent) Given an interpretation domain U, an agent is a tuple A = D, Act, Pr , where:

D is the local database schema;

Act is the finite set of action types α( p), where p is the tuple of abstract parameters;

Pr : D(U) 7 2Act(U) is the local protocol function, where Act(U) is the set of ground actions of the form α( u) where α( p) Act and u U| p| is a tuple of ground parameters.

Intuitively, at a given time each agent A is in some local state l D(U) that represents all the information agent A has at its disposal. In this sense we follow the standard approach to multiagent systems (Fagin et al., 1995), but require that this information is structured as a database. Again, following standard literature we assume that the agents are autonomous and proactive and perform the actions in Act according to the protocol function Pr, which returns the set of grounded actions enabled in any local state. In the definition above we use the term abstract parameters to denote variables, i.e., the language in which particular action parameters are given; we use the term ground parameters to refer to their concrete values. We assume that the agents interact among themselves and with an environment comprising all artifacts in the system. As artifacts are entities involving both data and processes, we can see them as collections of database instances paired with actions and governed by special protocols. Without loss of generality we can assume the environment state to be a single database instance including all artifacts in the system. From a purely formal point of view this allows us to represent the environment as a special agent. Of course, in any specific instantiation the environment and the agents will be different entities, exactly in line with the standard propositional version of interpreted systems. We can therefore define the synchronous composition of agents with the environment.

Definition 2.7 (Artifact-Centric Multi-agent Systems) Given an interpretation domain U and a set Ag = {A0, . . . , An} of agents Ai = Di, Acti, Pri defined on U, an artifact-centric multiagent system (or AC-MAS) is a tuple P = Ag, s0, τ where:

s0 Q Ai Ag Di(U) is the initial global state;

τ : Q Ai Ag Di(U) Act(U) 7 2 Q Ai Ag Di(U) is the global transition function, where Act(U) = Act0(U) Actn(U) is the set of global (ground) actions, and τ( l0, . . . , ln , α0( u0), . . . , αn( un) ) is defined whenever αi( ui) Pri(li) for every i n.

As we will see in later sections, AC-MAS are the natural extension of interpreted systems to the first order to account for environments constituted of artifact-centric systems. They can be seen as a specialisation of quantified interpreted systems (Belardinelli & Lomuscio, 2012), a general extension of interpreted systems to the first-order case. In the formalisation above the agent A0 is typically referred to as the environment E. The environment normally includes all artifacts in the system (notably by assuming that D0 S 0<i n Dn), as well as additional information to facilitate communication between the agents and the hub, e.g., messages in transit etc. In what follows we consider D0 = S 0<i n Dn for simplicity; this modelling choice does not impact the results presented later on. At any given time an AC-MAS is described by a tuple of database instances, representing all the agents in the system as well as the artifact

BELARDINELLI, LOMUSCIO & PATRIZI

system. A single interpretation domain for all database schemas is given. Note that this does not break the generality of the representation as we can always extend the domain of all agents and the environment before composing them into a single AC-MAS. The global transition function defines the evolution of the system through synchronous composition of actions for the environment and all agents in the system. Much of the interaction we are interested in modelling involves message exchanges with payload, hence the action parameters, between agents and the environment, i.e., agents operating on the artifacts. However, note that the formalisation above does not preclude us from modelling agent-toagent interactions, as the global transition function does not rule out successors in which only some agents change their local state following some actions. Also observe that essential concepts such as views are easily expressed in AC-MAS by insisting that the local state of an agent includes part of the environment s, i.e., the artifacts the agent has access to. Not all AC-MAS need to have views defined, so it is also possible for the views to be empty. Other artifact-based concepts such as lifecycles are naturally expressed in AC-MAS. As artifacts are modelled as part of the environment, a lifecycle is naturally encoded in AC-MAS simply as the sequence of changes induced by the transition function τ on the fragment of the environment representing the lifecycle in question. We will show an example of this in Section 2.4. Some technical remarks now follow. To simplify the notation, we denote a global ground action as α( u), where α = α0(p0), . . . , αn(pn) and u = u0, . . . , un , with each ui of appropriate size. We define the transition relation on Q Ai Ag Di(U) Q Ai Ag Di(U) such that s s if and only if there exists α( u) Act(U) such that s τ(s, α( u)). If s s , we say that s is a successor of s. A run r from s S is an infinite sequence s0 s1 , with s0 = s. For n N, we take r(n) .= sn. A state s is reachable from s if there exists a run r from the global state r(0) = s such that r(i) = s , for some i 0. We assume that the relation is serial, i.e., for every global state s there exists s such that s s . This can be easily obtained by assuming that each agent has a skip action enabled at each local state and that performing skip induces no changes in any of the local states. We introduce S as the set of states reachable from the initial state s0 according to the transition relation . Notice that assuming a unique initial state does not hinder the generality of the approach, as for any finite set I of states we can encode in τ transitions from s0 to the states in I. As in plain interpreted systems (Fagin et al., 1995), we say that two global states s = l0, . . . , ln and s = l 0, . . . , l n are epistemically indistinguishable for agent Ai, written s i s , if li = l i. Differently from interpreted systems the local equality is evaluated on database instances. For convenience we will use also the concept of temporal-epistemic (t.e., for short) run. Formally a t.e. run r from a state s S is an infinite sequence s0 ; s1 ; . . . such that s0 = s and si si+1 or si k si+1, for some k Ag. A state s is said to be temporally-epistemically reachable (t.e. reachable, for short) from s if there exists a t.e. run r from the global state r(0) = s such that for some i 0 we have that r(i) = s . Obviously, temporal-epistemic runs include purely temporal runs as a special case. Also, notice that we admit U to be infinite, thereby allowing the possibility of the set of states S to be infinite. Indeed, unless we specify otherwise, we will assume to be working with infinite-state AC-MAS. Finally, for technical reasons it is useful to refer to the global database schema D = D0 Dn of an AC-MAS. Every global state s = l0, . . . , ln is associated with the (global) D-instance Ds D(U) such that Ds(Pi) = S j Ag lj(Pi), for Pi D. We omit the subscript s whenever s is clear from the context and we write adom(s) for adom(Ds). The justification for this choice comes from the fact that we think of each agent as having a partial, although truthful, view of the

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

global state. If the same relation appears in several agent database schemas, possibly with different interpretations, it means that each agent is aware of only a subset of the total extension of the relation. We maintain that this modeling choice is justified by the application to artifact systems, as it will become apparent in Section 2.4. Notice that for every s S, the Ds associated with s is unique, while the converse is not true in general. Finally, we lift the disjoint union operator to global states so that s s .= l0 l 0, . . . , ln l n . It can be seen that Ds Ds and Ds s represent in fact the same D D -instance.

2.3 Model Checking

We now define the problem of verifying an artifact-centric multi-agent system against a specification of interest. By following the artifact-centric model, we wish to give data the same prominence as processes. To deal with data and the underlying database instances, our specification language needs to include first-order logic. Further, we require temporal logic to describe the system execution. Lastly, we use epistemic logic to express the information the agents have at their disposal. Hence, we define a first-order temporal-epistemic specification language to be interpreted on AC-MAS. The specification language will be used in Section 4 to formalise properties of artifact-centric programs.

Definition 2.8 (The Logic FO-CTLK) The first-order CTLK (or FO-CTLK) formulas ϕ over a database schema D are inductively defined by the following BNF:

ϕ ::= φ | ϕ | ϕ ϕ | xϕ | AXϕ | AϕUϕ | EϕUϕ | Kiϕ | Cϕ

where φ LD and 0 < i n.

The notions of free and bound variables for FO-CTLK extend straightforwardly from LD, as well as functions var, free, and con. As usual, the temporal formulas AXϕ and AϕUϕ (resp. EϕUϕ ) are read as for all runs, at the next step ϕ and for all runs (resp. some run), ϕ until ϕ . The epistemic formulas Kiϕ and Cϕ intuitively mean that agent Ai knows ϕ and it is common knowledge among all agents that ϕ respectively. We use the abbreviations EXϕ, AFϕ, AGϕ, EFϕ, and EGϕ as standard. Observe that free variables can occur within the scope of modal operators, thus admitting the unconstrained alternation of quantifiers and modal operators, thereby allowing us to refer to elements in different modal contexts. The semantics of FO-CTLK formulas is defined as follows.

Definition 2.9 (Satisfaction for FO-CTLK) Consider an AC-MAS P, an FO-CTLK formula ϕ, a state s P, and an assignment σ. We inductively define whether P satisfies ϕ in s under σ, written (P, s, σ) |= ϕ, as follows:

(P, s, σ) |= ϕ iff (Ds, σ) |= ϕ, if ϕ is an FO-formula (P, s, σ) |= ϕ iff it is not the case that (P, s, σ) |= ϕ (P, s, σ) |= ϕ ϕ iff (P, s, σ) |= ϕ or (P, s, σ) |= ϕ

(P, s, σ) |= xϕ iff for all u adom(s), (P, s, σ x u ) |= ϕ (P, s, σ) |= AXϕ iff for all runs r, if r(0) = s, then (P, r(1), σ) |= ϕ (P, s, σ) |= AϕUϕ iff for all runs r, if r(0) = s, then there is k 0 s.t. (P, r(k), σ) |= ϕ , and for all j, 0 j < k implies (P, r(j), σ) |= ϕ (P, s, σ) |= EϕUϕ iff for some run r, r(0) = s and there is k 0 s.t. (P, r(k), σ) |= ϕ ,

BELARDINELLI, LOMUSCIO & PATRIZI

and for all j, 0 j < k implies (P, r(j), σ) |= ϕ (P, s, σ) |= Kiϕ iff for all s S, s i s implies (P, s , σ) |= ϕ (P, s, σ) |= Cϕ iff for all s S, s s implies (P, s , σ) |= ϕ

where is the transitive closure of S 1 i n i.

A formula ϕ is said to be true at a state s, written (P, s) |= ϕ, if (P, s, σ) |= ϕ for all assignments σ. Moreover, ϕ is said to be true in P, written P |= ϕ, if (P, s0) |= ϕ. A key concern in this paper is to explore the model checking of AC-MAS against first-order temporal-epistemic specifications (Grohe, 2001).

Definition 2.10 (Model Checking Problem) Given an AC-MAS P and a FO-CTLK formula ϕ the model checking problem consists in finding an assignment σ such that (P, s0, σ) |= ϕ.

It is easy to see that whenever U is finite the model checking problem is decidable as P is a finitestate system. In general, however, this is not the case. To see this, notice that, by assuming computability, both the agents protocol functions Pri and the AC-MAS transition function τ, can be finitely represented (e.g., as Turing machines). Since all other components of agents and AC-MAS definitions are finite, it follows that all AC-MAS, in particular infinite-state ones, admit a finite representation. Assuming fixed the representation formalism, we have the following result.

Theorem 2.11 The model checking problem for AC-MAS w.r.t. FO-CTLK is undecidable.

Proof (sketch). This can be proved by showing that every Turing machine T whose tape contains an initial input I can be simulated by an artifact system PT,I. The problem of checking whether T terminates on that particular input can be reduced to checking whether PT,I |= ϕ, where ϕ encodes the termination condition. The detailed construction is similar to that of the work of Deutsch, Sui, and Vianu (2007, Thm. 4.10).

Given the general setting in which the model checking problem is defined above, the negative result is not surprising. In the following we identify semantic restrictions for which the problem is decidable.

2.4 The Order-to-Cash Scenario

We analyse a business process inspired by a concrete IBM customer use case (Hull et al., 2011). The order-to-cash scenario describes the interactions of a number of agents in an e-commerce situation relating to the purchase and delivery of a product. The agents in the artifact-centric system consist of a manufacturer, some customers, and some suppliers. The process begins when a customer prepares and submits a purchase order (PO), i.e., a list of products the customer requires, to the manufacturer. Upon receiving a PO, the manufacturer prepares a material order (MO), i.e., a list of components needed to assemble the requested products. The manufacturer then selects a supplier and forwards him the relevant material order. Upon receiving an MO a supplier can either accept or reject it. In the former case he then proceeds to deliver the requested components to the manufacturer. In the latter case he notifies the manufacturer of his rejection. If an MO is rejected, the manufacturer deletes it and then prepares and submits a new MO. When the manufacturer receives the delivered components, he assembles the product and, provided the order has been paid

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

PO id prod code offer status

MO id prod code price status

Products prod code budget

Materials mat code cost

Figure 1: The Data Model for the Order-to-Cash Scenario.

prepared pending paid shipped create PO submit PO pay ship PO delete PO

(a) Purchase Order lifecyle

preparation submitted

accepted shipped

create MO done MO

(b) Material Order lifecyle

Figure 2: Lifecycles of the artifacts involved in the order-to-cash scenario.

for, delivers it to the customer. Any manufacturer order which is directly or indirectly related to a PO can be deleted only after the PO is deleted. We can encode the order-to-cash business process as an artifact-centric multi-agent system, where the artifact data models are represented as database schemas and their evolution is characterised by an appropriate set of operations. It is natural to identify two artifact types, representing the PO and the MO. We reserve a distinguished relation for each artifact type. In addition, we introduce static relations to store product and material information. As a result, the data model of the order-to-cash scenario with associated attributes can be given as in Figure 1. The intended meaning of relations is self-explanatory. Note the presence of the attribute status in the relations corresponding to artifact classes. An intuitive representation of the artifact lifecycles, i.e., the evolution of some key records in the artifacts states, capturing only the dependence of actions from the artifact statuses, is shown in Figure 2. For example, a purchase order, with initial status prepared, is created by the agent customer through the action create PO. Once the order is submitted to the agent manufacturer, the PO status changes to pending. The other transitions labelled by pay, ship PO and delete PO, act similarly, according to their semantics, on the status of the purchase order. Note that this is an incomplete representation of the business process, as the interaction between actions and the artifact data content is not represented.

BELARDINELLI, LOMUSCIO & PATRIZI

We now formally encode the scenario as an AC-MAS. For the sake of presentation in what follows we assume to be dealing with three agents only: one customer c, one manufacturer m and one supplier s. The database schema Di for each agent i {c, m, s} can be given as:

Customer c: Dc = {Products(prod code, budget), PO(id, prod code, offer, status)};

Manufacturer m: Dm = {PO(id, prod code, offer, status), MO(id, prod code, price, status)};

Supplier s: Ds = {Materials(mat code, cost), MO(id, prod code, price, status)}.

We consider the infinite set Uotc of alphanumeric strings as the interpretation domain, and introduce a parametric action for each transition in the lifecycles in Figure 2. Also, we assume that in the initial state the only non-empty relations are Products and Materials, which contain background information, such as a catalogue of available products. We can now define the agents in the order-to-cash scenario as follows.

Definition 2.12 the agents Ac, Am and As are given as

Ac = Dc, Actc, Prc , where (i) Dc is as above; (ii) Actc = {create PO(id, pcode), submit PO(id), pay(id), delete PO(id)}; and (iii) Prc respects the intended meaning of the customer s actions. For instance, create PO(id, pcode) Prc(lc) iff the interpretation lc(Products) of the relation Products in the local state lc contains a tuple pcode, b for some budget b.

Am = Dm, Actm, Prm , where (i) Dm is as above; (ii) Actm = {create MO(id, price), done MO(id), ship PO(id), delete MO(id)}; and (iii) Prm respects the intended meaning of the manufacturer s actions. For instance, create MO(po id, price) Prm(lm) iff the interpretation lm(MO) of the relation MO in the local state lm does not contain a tuple po id, pc, pr, preparation for the same PO id po id.

As = Ds, Acts, Prs , where (i) Ds is as above; (ii) Acts = {accept MO(id), reject MO(id), ship MO(id)}; and (iii) Prc respects the intended meaning of the suppliers actions. For instance, accept MO(mo id) Prs(ls) iff ls(MO) does not contain a tuple with id mo id and status accepted.

Further, we can now define the AC-MAS induced by the set of agents Agotc = {Ac, Am, As} according to Definition 2.7.

Definition 2.13 Given the set of agents Agotc = {Ac, Am, As}, the AC-MAS Potc = Agotc, s0 otc, τotc is such that

s0 otc = lc, lm, ls is the initial global state, where the only non-empty relations are Products and Materials in lc and ls respectively;

τotc is the global transition function defined so as to respect the intended meaning of the evolution of the order-to-cash scenario. For instance, consider the global action

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

α( u) = create PO(pc), done MO(m), accept MO(m ) enabled by the respective protocols in a global state s. By the definition of the actions create PO(pc), done MO(m), and accept MO(m ) we have that li(s) Pri for i {c, m, s} implies that the Products relation contains information about the product pc. Also, the interpretation of the relation MO contains the tuples m, p, pr, preparation and m , p , pr , submitted for some products p and p . Hence, s τotc(s, α( u)) iff the interpretation of the relation PO in s extends Ds(PO) with the tuple id, pc, b, prepared , where id is a fresh id. The tuples for the material orders m and m are updated in Ds (MO) by becoming m, p, pr, submitted and m , p , pr , accepted , respectively. No other element is changed in the transition.

Clearly, the function τotc given above can easily be completed to encode the artifacts lifecycles as given in Figure 2. In section 4.2 we will give a succinct encoding of Potc in terms of an artifactcentric program. We can now investigate properties of the present business process by using specifications in FO-CTLK. For instance, the following formula intuitively specifies that the manufacturer m knows that each material order MO has to match a corresponding purchase order PO:

ϕmatch = AG id, pc ( pr, s MO(id, pc, pr, s) Km o, s PO(id, pc, o, s ))

The next specification states that given a material order MO, the customer will eventually know that the corresponding PO will be shipped.

ϕfulfil = AG id, pc ( pr, s MO(id, pc, pr, s) EF Kc o PO(id, pc, o, shipped))

Further, we may be interested in checking whether or not budget and costs are always kept secret from the supplier s and the customer c respectively, and whether the customer (resp., the supplier) knows this fact:

ϕbudget = Kc pc AG b Ks Products(pc, b)

ϕcost = Ks mc AG c Kc Materials(mc, c)

Other interesting specifications describing properties of the artifact system and the agents operating in it can be similarly formalised in FO-CTLK, thereby providing the engineer with a valuable tool to assess the implementation. Observe that the AC-MAS for the order-to-cash scenario has an infinite number of states thereby making it difficult to investigate by means of traditional model checking techniques. We will return to this scenario in Subsection 4.2 where we will investigate how it may still be verified. Before doing so we develop a methodology for associating finite abstractions to infinite AC-MAS.

3. Abstraction for Artifact-Centric Multi-agent Systems

In the previous section we have observed that model checking AC-MAS against FO-CTLK is undecidable in general. It is clearly of interest to isolate decidable settings. In what follows we identify semantic constraints resulting in a decidable model checking problem. The investigation is carried out on a rather natural subclass of AC-MAS that we call bounded, as defined below. Our goal for proceeding in this manner is to identify finite abstractions of infinite-state AC-MAS so that verification of programs that admit bounded AC-MAS as models can be conducted on them, rather than on the original infinite-state AC-MAS. We will see this in detail in Section 4.

BELARDINELLI, LOMUSCIO & PATRIZI

The key concept that enables us to achieve the above is uniformity. Uniform AC-MAS are systems for which the behaviour does not depend on the actual data present in the states. This means that the system contains all possible transitions that are enabled according to parametric action rules, thereby resulting in a full transition relation. This notion is related to genericity in databases (Abiteboul et al., 1995). Here we use the term uniformity as we refer to transition systems and not databases. To achieve finite abstractions we proceed as follows. We first propose an adaptation of the notion of isomorphism to our setting; then we introduce bisimulations; finally in Subsection 3.2 we show how this notion can be exploited to guarantee that uniform AC-MAS satisfy the same FO-CTLK formulas. We then use this result to show that bounded, uniform systems admit finite abstractions (Subsection 3.3). The complexity of the model checking problem is analysed in Subsection 3.4. In the rest of the section we let P = Ag, s0, τ and P = Ag , s 0, τ be two AC-MAS and assume, unless stated differently, that s = l0, . . . , ln S, and s = l 0, . . . , l n S .

3.1 Isomorphisms

We now investigate the concept of isomorphism on AC-MAS. This will be needed in later sections to define finite abstractions of infinite-state AC-MAS.

Definition 3.1 (Isomorphism) Two local states l, l D(U) are isomorphic, written l l , iff there exists a bijection ι : adom(l) Con 7 adom(l ) Con such that:

(i) ι is the identity on Con;

(ii) for every Pi D, u Uqi, we have that u l(Pi) iff ι( u) l (Pi).

When this is the case, we say that ι is a witness for l l . Two global states s S and s S are isomorphic, written s s , iff there exists a bijection ι : adom(s) Con 7 adom(s ) Con such that for every j Ag, ι is a witness for lj l j.

Notice that isomorphisms preserve the interpretation of constants in Con as well as of predicates in the local states up to renaming of the corresponding terms. Any function ι as above is called a witness for s s . Obviously, the relation is an equivalence relation. Given a function f : U 7 U defined on adom(s), f(s) denotes the instance in D(U ) obtained from s by renaming each u adom(s) as f(u). If f is also injective (thus invertible) and the identity on Con, then f(s) s.

Example As an example of isomorphic states, consider an agent with local database schema D = {P1/2, P2/1}, let U = {a, b, c, . . .} be an interpretation domain, and fix the set Con = {b} of constants. Let l be the local state such that l(P1) = { a, b , b, d } and l(P2) = {a} (see Figure 3). Then, the local state l such that l (P1) = { c, b , b, e } and l (P2) = {c} is isomorphic to l. This can be easily seen by considering the isomorphism ι, where: ι(a) = c, ι(b) = b, and ι(d) = e. However, the state l where l (P1) = { f, d , d, e } and l (P2) = {f} is not isomorphic to l. Indeed, although a bijection exists that maps l into l , it is easy to see that none can be such that ι (b) = b. Note that, while isomorphic states have the same relational structure, two isomorphic states do not necessarily satisfy the same FO-formulas as satisfaction depends also on the values assigned to free variables. To account for this, we introduce the following notion.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

l(P1) a b b d

l (P1) c b b e

l (P1) f d d e

Figure 3: Examples of isomorphic and non-isomorphic local states.

Definition 3.2 (Equivalent assignments) Given two states s S and s S , and a set of variables V V ar, two assignments σ : V ar 7 U and σ : V ar 7 U are equivalent for V w.r.t. s and s iff there exists a bijection γ : adom(s) Con σ(V ) 7 adom(s ) Con σ (V ) such that:

(i) γ|adom(s) Con is a witness for s s ;

(ii) σ |V = γ σ|V .

Intuitively, equivalent assignments preserve both the (in)equalities of the variables in V and the constants in s, s up to renaming. Note that, by definition, the above implies that s, s are isomorphic. We say that two assignments are equivalent for an FO-CTLK formula ϕ, omitting the states s and s when clear from the context, if these are equivalent for free(ϕ). We can now show the following standard result in first-order (non-modal) logic, i.e., isomorphic states satisfy exactly the same FO-formulas (Abiteboul et al., 1995).

Proposition 3.3 Given two isomorphic states s S and s S , an FO-formula ϕ, and two assignments σ and σ equivalent for ϕ, we have that

(Ds, σ) |= ϕ iff (Ds , σ ) |= ϕ

Moreover, if ψ is an FO-sentence,

Ds |= ψ iff Ds |= ψ

Thus, isomorphic states cannot be distinguished by FO-sentences. This enables us to use this notion, when defining simulations.

3.2 Bisimulations

Plain bisimulations are known to be satisfaction preserving in a modal propositional setting (Blackburn, de Rijke, & Venema, 2001). In the following we explore the conditions under which this applies to AC-MAS as well. We introduce a notion of bisimulation, based on isomorphisms, and later explore its properties in the context of uniform AC-MAS.

Definition 3.4 (Simulation) A relation R on S S is a simulation if s, s R implies:

2. for every t S, if s t then there exists t S s.t. s t , s t s t , and t, t R;

3. for every t S, for every 0 < i n, if s i t then there exists t S s.t. t i t , s t s t , and t, t R.

BELARDINELLI, LOMUSCIO & PATRIZI

Figure 4: Bisimilar AC-MAS not satisfying the same FO-CTLK formulas.

Definition 3.4 has many similarities with the standard notion of simulation in the propositional setting. In particular, the co-inductive structure of the definition requires similar states to satisfy some local property and to preserve this along corresponding transitions. However, differently from the propositional case, we here insist that s t s t ; this ensures that similar transitions in AC-MAS preserve isomorphic disjoint unions. A state s S is said to simulate s S, written s s , iff there exists a simulation R s.t. s, s R. When no ambiguity arises, we simply say that s and s are similar. Note that similar states are isomorphic, as condition (2) above ensures that s s . The similarity relation can be shown to be the largest simulation, reflexive and transitive on S S . Further, we say that P

simulates P, written P P , if s0 s 0. Simulations can naturally be extended to bisimulations, as follows.

Definition 3.5 (Bisimulation) A relation B on S S is a bisimulation iff both B and B 1 = { s , s | s, s B} are simulations.

Two states s S and s S are said to be bisimilar, written s s , iff there exists a bisimulation B such that s, s B. It can be shown that is the largest bisimulation, and an equivalence relation, on S S . We say that P and P are bisimilar, written P P iff so are s0 and s 0. It is instructive to note that bisimilar systems do not preserve FO-CTLK formulas. This is markedly different from the modal propositional case.

Example Consider Figure 4, where Con = and P and P are given as follows. For a number n of agents equal to 1, we define D = D = {P/1} and U = N; s0(P) = s 0(P) = {1}; τ = { s, s | s(P) = {i}, s (P) = {i + 1}}; τ = { s, s | s(P) = {i}, s (P) = {(i mod 2) + 1}}. Notice that S D(N) and S D(N). Clearly we have that P P . Now, consider the constant-free FO-CTLK formula ϕ = AG( x(P(x) AXAG P(x))). It can be easily seen that P |= ϕ while P |= ϕ. The above shows that, differently from the propositional case, bisimilarity is not a sufficient condition to guarantee the preservation of FO-CTLK formulas. Intuitively, this is a consequence of the fact that bisimilar AC-MAS do not preserve value associations along runs. For instance, the value 1 in P is associated infinitely many times with the odd values occurring in P. By quantifying across states we are able to express this fact and can therefore distinguish the two structures. This is a difficulty as, intuitively, we would like to use bisimulations to demonstrate the existence of finite abstractions. However, as we show later, this happens on the class of uniform AC-MAS, defined below.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Definition 3.6 (Uniformity) An AC-MAS P is said to be uniform iff for every s, t, s S, t D(U),

1. if t τ(s, α( u)) and s t s t for some witness ι, then for every constant-preserving bijection ι that extends ι to u, we have that t τ(s , α(ι ( u)));

2. if s i t and s t s t , then s i t .

This definition captures the idea that actions take into account and operate only on the relational structure of states and action parameters, irrespective of the actual data they contain (apart from a finite set of constants). Intuitively, uniformity expresses that if t can be reached by executing α( u) in s, and we replace the same element v with v in s, u and t, obtaining s , u and t , then t can be reached by executing α( u ) in s . In terms of the underlying Kripke structures, i.e., the frames induced on S by relations and i for Ai Ag, this means that the systems are full up to , that is, in all uniform AC-MAS the states t identified above are indeed part of the system and reachable from s . A similar condition is required on the epistemic relation. A property of uniform systems is that the latter requirement is implied by the former, as shown by the following result.

Proposition 3.7 If an AC-MAS P satisfies req. 1 in Def. 3.6 and adom(s0) Con, then req. 2 is also satisfied.

Proof. If s t s t , then there is a witness ι : adom(s) adom(t) Con 7 adom(s ) adom(t ) Con that is the identity on Con (hence on adom(s0)). Assume s i t, thus li(s) = li(t), and li(s ) = ι(li(s)) = ι(li(t)) = li(t ). Notice that this does not guarantee that s i t , as we need to prove that t S. This can be done by showing that t is reachable from s0. Since t is reachable from s0, there exists a run s0 s1 . . . sk s.t. sk = t. Extend now ι to a total and injective function ι : adom(s0) adom(sk) Con 7 U. This can always be done because |U| |adom(s0) adom(sk) Con|. Now consider the sequence ι (s0), ι (s1), . . . , ι (sk). Since adom(s0) Con then ι(s0) = s0 and, because ι extends ι, we have that ι (s0) = ι(s0) = s0. Further, ι (sk) = ι(t) = t . By repeated applications of req. 1 we can show that ι (sm+1) τ(ι (sm), α(ι ( u))) whenever sm+1 τ(sm, α( u)), for m < k. Hence, the sequence is actually a run from s0 to t . Thus, t S, and s i t .

Thus, as long as adom(s0) Con, to check whether an AC-MAS is uniform, it is sufficient to take into account only the transition function. A further distinctive feature of uniform systems is that all isomorphic states are bisimilar.

Proposition 3.8 If an AC-MAS P is uniform, then for every s, s S, s s implies s s .

Proof. We prove that B = { s, s S S | s s } is a bisimulation. Observe that since is an equivalence relation, so is B. Thus B is symmetric and B = B 1. Therefore, proving that B is a simulation proves also that B 1 is a simulation; hence, that B is a bisimulation. To this end, let s, s B, and assume s t for some t S. Then, t τ(s, α( u)) for some α( u) Act(U). Consider a witness ι for s s . By cardinality considerations ι can be extended to a total and injective function ι : adom(s) adom(t) { u} Con 7 U. Consider ι (t) = t ; it follows that ι

is a witness for s t s t . Since P is uniform, t τ(s , α(ι ( u))), that is, s t . Moreover, ι is a witness for t t , thus t, t B. Next assume that s, s B and s i t, for some t S.

BELARDINELLI, LOMUSCIO & PATRIZI

By reasoning as above we can find a witness ι for s s , and an extension ι of ι s.t. t = ι (t) and ι is a witness for s t s t . Since P is uniform, s i t and t, t B.

This result intuitively means that submodels generated by isomorphic states are bisimilar. Next we prove some partial results, which will be useful in proving our main preservation theorem. The first two guarantee that under appropriate cardinality constraints the bisimulation preserves the equivalence of assignments w.r.t. a given FO-CTLK formula.

Lemma 3.9 Consider two bisimilar and uniform AC-MAS P and P , two bisimilar states s S and s S , and an FO-CTLK formula ϕ. For every assignments σ and σ equivalent for ϕ w.r.t. s and s , we have that:

1. for every t S s.t. s t, if |U | |adom(s) adom(t) Con σ(free(ϕ))|, then there exists t S s.t. s t , t t , and σ and σ are equivalent for ϕ w.r.t. t and t .

2. for every t S s.t. s i t, if |U | |adom(s) adom(t) Con σ(free(ϕ))|, then there exists t S s.t. s i t , t t , and σ and σ are equivalent for ϕ w.r.t. t and t .

Proof. To prove (1), let γ be a bijection witnessing that σ and σ are equivalent for ϕ w.r.t. s and s . Suppose that s t. Since s s , by definition of bisimulation there exists t S s.t. s t , s t s t , and t t . Now define Domj .= adom(s) adom(t) Con, and partition it into:

Domγ .= adom(s) Con (adom(t) σ(free(ϕ));

Domι .= adom(t) \ Domγ.

Let ι : Domι 7 U \ Im(γ) be an invertible total function. Observe that |Im(γ)| = |adom(s ) Con σ (free(ϕ))| = |adom(s) Con σ(free(ϕ))|, thus from the fact that |U | |adom(s) adom(t) Con σ(free(ϕ))| we have |U \ Im(γ)| |Dom(ι )|, which guarantees the existence of ι . Next, define j : Domj 7 U as follows:

j(u) = γ(u), if u Domγ ι (u), if u Domι

Obviously, j is invertible. Thus, j is a witness for s t s t , where t = j(t). Since s t s t and is an equivalence relation, we obtain that s t s t . Thus, s t , as P is uniform. Moreover, σ and σ are equivalent for ϕ w.r.t. t and t , by construction of t . To check that t t , observe that, since t t and P is uniform, by Prop. 3.8 it follows that t t . Thus, since t t and is transitive, we obtain that t t . The proof for (2) has an analogous structure and therefore is omitted.

It can be proven that this result is tight, i.e., that if the cardinality requirement is violated, there exist cases where assignment equivalence is not preserved along temporal or epistemic transitions. Lemma 3.9 easily generalises to t.e. runs.

Lemma 3.10 Consider two bisimilar and uniform AC-MAS P and P , two bisimilar states s S and s S , an FO-CTLK formula ϕ, and two assignments σ and σ equivalent for ϕ w.r.t. s and s . For every t.e. run r of P, if r(0) = s and for all i 0, |U | |adom(r(i)) adom(r(i + 1)) Con σ(free(ϕ))|, then there exists a t.e. run r of P s.t. for all i 0:

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

(i) r (0) = s ;

(ii) r(i) r (i);

(iii) σ and σ are equivalent for ϕ w.r.t. r(i) and r (i).

(iv) for every i 0, if r(i) r(i + 1) then r (i) r (i + 1), and if r(i) j r(i + 1), for some j, then r (i) j r (i + 1).

Proof. Let r be a t.e. run satisfying the lemma s hypothesis. We inductively build r and show that the conditions above are satisfied. For i = 0, let r (0) = s . By hypothesis, r is s.t. |U | |adom(r(0)) adom(r(1)) Con σ(free(ϕ))|. Thus, since r(0) ; r(1), by Lemma 3.9 there exists t S s.t. r (0) ; t , r(1) t , and σ and σ are equivalent for ϕ w.r.t. r(1) and t . Let r (1) = t . Lemma 3.9 guarantees that the transitions r (0) ; t and r(0) ; r(1) can be chosen so that they are either both temporal or both epistemic with the same index. The case for i > 0 is similar. Assume that r(i) r (i) and σ and σ are equivalent for ϕ w.r.t. r(i) and r (i). Since r(i) ; r(i + 1) and |U | |adom(r(i)) adom(r(i + 1)) Con σ(free(ϕ))|, by Lemma 3.9 there exists t S s.t. r (i) ; t , σ and σ are equivalent for ϕ w.r.t. r(i + 1) and t , and r(i + 1) t . Let r (i + 1) = t . It is clear that r is a t.e. run in P , and that, by Lemma 3.9, the transitions of r can be chosen so as to fulfil requirement (iv).

We can now prove that FO-CTLK formulas cannot distinguish bisimilar and uniform AC-MAS. This is in marked contrast with the earlier example in this section which related to bisimilar but non-uniform AC-MAS.

Theorem 3.11 Consider two bisimilar and uniform AC-MAS P and P , two bisimilar states s S and s S , an FO-CTLK formula ϕ, and two assignments σ and σ equivalent for ϕ w.r.t. s and s . If

1. for every t.e. run r s.t. r(0) = s, for all k 0 we have |U | |adom(r(k)) adom(r(k + 1)) Con σ(free(ϕ))| + |var(ϕ) \ free(ϕ)|; and

2. for every t.e. run r s.t. r (0) = s , for all k 0 we have |U| |adom(r (k)) adom(r (k + 1)) Con σ (free(ϕ))| + |var(ϕ) \ free(ϕ)|;

(P, s, σ) |= ϕ iff (P , s , σ ) |= ϕ.

Proof. The proof is by induction on the structure of ϕ. We prove that if (P, s, σ) |= ϕ then (P , s , σ ) |= ϕ. The other direction can be proved analogously. The base case for atomic formulas follows from Prop. 3.3. The inductive cases for propositional connectives are straightforward. For ϕ xψ, assume that x free(ψ) (otherwise consider ψ, and the corresponding case), and no variable is quantified more than once (otherwise rename variables). Let γ be a bijection witnessing that σ and σ are equivalent for ϕ w.r.t. s and s . For u adom(s), consider the assignment σ x u . By definition, γ(u) adom(s ), and σ x γ(u) is well-defined. Note that free(ψ) = free(ϕ) {x}; so σ x u and σ x γ(u) are equivalent for ψ w.r.t. s and s . Moreover, |σ x u (free(ψ))| |σ(free(ϕ))| + 1, as u may not occur in σ(free(ϕ)). The same considerations apply to σ . Further, |var(ψ) \ free(ψ)| = |var(ϕ) \ free(ϕ)| 1, as var(ψ) = var(ϕ),

BELARDINELLI, LOMUSCIO & PATRIZI

free(ψ) = free(ϕ) {x}, and x / free(ϕ). Thus, both hypotheses (1) and (2) remain satisfied if we replace ϕ with ψ, σ with σ x u , and σ with σ x γ(u) . Therefore, by the induction hypothesis, if (P, s, σ x u ) |= ψ then (P , s , σ x γ(u) ) |= ψ. Since u adom(s) is generic and γ is a bijection, the result follows. For ϕ AXψ, assume by contradiction that (P, s, σ) |= ϕ but (P , s , σ ) |= ϕ. Then, there exists a run r s.t. r (0) = s and (P , r (1), σ ) |= ψ. Since |var(ϕ) \ free(ϕ)| 0, by Lemma 3.10, there exists a run r s.t. r(0) = s, and for all i 0, r(i) r (i) and σ and σ are equivalent for ψ w.r.t. r(i) and r (i). Since r is a run s.t. r(0) = s, it satisfies hypothesis (1). Moreover, the same hypothesis is necessarily satisfied by all the t.e. runs r s.t. for some i 0, r (0) = r(i) (otherwise, the t.e. run r(0) ; ; r(i) ; r (1) ; r (2) ; would not satisfy the hypothesis for r); the same considerations apply w.r.t hypothesis (2) and for all the t.e. runs r s.t. r (0) = r (i), for some i 0. In particular, these hold for i = 1. Thus, we can inductively apply the lemma, by replacing s with r(1), s with r (1), and ϕ with ψ (observe that var(ϕ) = var(ψ) and free(ϕ) = free(ψ)). But then we obtain (P, r(1), σ) |= ψ, thus (P, r(0), σ) |= AXψ. This is a contradiction. For ϕ EψUφ, assume that the only variables common to ψ and φ occur free in both formulas (otherwise rename the quantified variables). Let r be a run s.t. r(0) = s, and there exists k 0 s.t. (P, r(k), σ) |= φ, and (P, r(j), σ) |= ψ for 0 j < k. By Lemma 3.10 there exists a run r s.t. r (0) = s and for all i 0, r (i) r(i) and σ and σ are equivalent for ϕ w.r.t. r (i) and r(i). From each bijection γi witnessing that σ and σ are equivalent for ϕ w.r.t. r (i) and r(i), define the bijections γi,ψ = γi|adom(r(i)) Con σ(free(ψ)) and γi,φ = γi|adom(r(i)) Con σ(free(φ)). Since free(ψ) free(ϕ), free(φ) free(ϕ), it can be seen that γi,ψ and γi,φ witness that σ and σ are equivalent for respectively ψ and φ w.r.t. r (i) and r(i). By the same argument used for the AX case above, hypothesis (1) holds for all the t.e. runs r s.t. r (0) = r(i), for some i 0, and hypothesis (2) holds for all the t.e. runs r s.t. r (0) = r (i). Now observe that |σ(free(φ))|, |σ(free(ψ))| |σ(free(ϕ))|. Moreover, by the assumption on the common variables of ψ and φ, (var(ϕ) \ free(ϕ)) = (var(ψ) \ free(ψ)) (var(φ) \ free(φ)), thus |var(ϕ) \ free(ϕ)| = |(var(ψ) \ free(ψ)| + |(var(φ) \ free(φ)|, hence |(var(ψ) \ free(ψ)|, |(var(φ) \ free(φ)| |var(ϕ) \ free(ϕ)|. Therefore hypotheses (1) and (2) hold also with ϕ uniformly replaced by either ψ or φ. Then, the induction hypothesis applies for each i, by replacing s with r(i), s with r (i), and ϕ with either ψ or φ. Thus, for each i, (P, r(i), σ) |= ψ iff (P , r (i), σ ) |= ψ, and (P, r(i), σ) |= φ iff (P , r (i), σ ) |= φ. Therefore, r is a run s.t. r (0) = s , (P , r (k), σ ) |= φ, and for every j, 0 j < k implies (P , r (j), σ ) |= ψ, i.e., (P , s , σ ) |= EψUφ. For ϕ AψUφ, assume by contradiction that (P, s, σ) |= ϕ but (P , s , σ ) |= ϕ. Then, there exists a run r s.t. r (0) = s and for every k 0, either (P , r (k), σ ) |= φ or there exists j s.t. 0 j < k and (P , r (j), σ ) |= ψ. By Lemma 3.10 there exists a run r s.t. r(0) = s, and for all i 0, r(i) r (i) and σ and σ are equivalent for ϕ w.r.t. r(i) and r (i). Similarly to the case of EψUφ, it can be shown that σ and σ are equivalent for ψ and φ w.r.t. r(i) and r (i), for all i 0. Further, assuming w.l.o.g. that all variables common to ψ and φ occur free in both formulas, it can be shown, as in the case of EψUφ, that the induction hypothesis holds on every pair of runs obtained as suffixes of r and r , starting from their i-th state, for every i 0. Thus, (P, r(i), σ) |= ψ iff (P , r (i), σ ) |= ψ, and (P, r(i), σ) |= φ iff (P , r (i), σ ) |= φ. But then r is s.t. r(0) = s and for every k 0, either (P, r(k), σ) |= φ or there exists j s.t. 0 j < k and (P, r(j), σ) |= ψ, that is, (P, s, σ) |= AψUφ. This is a contradiction. For ϕ Kiψ, assume by contradiction that (P, s, σ) |= ϕ but (P , s , σ ) |= ϕ. Then, there exists s s.t. s i s and (P , s , σ ) |= ψ. By Lemma 3.10 there exists s s.t. s s , s i s ,

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

and σ and σ are equivalent for ψ w.r.t. s and s . Thus, by an argument analogous to that used for the case of AX, we can apply the induction hypothesis, obtaining (P, s , σ) |= ψ. But then (P, s, σ) |= Kiψ, which is a contradiction. Finally, for ϕ Cψ, assume by contradiction that (P, s, σ) |= ϕ but (P , s , σ ) |= ϕ. Then, there exists an s s.t. s s and (P , s , σ ) |= ψ. Again by Lemma 3.10 there exists s s.t. s s , s s , and σ and σ are equivalent for ψ w.r.t. s and s . Thus, by an argument analogous to that used for the case of Ki, we can apply the induction hypothesis, obtaining (P, s , σ) |= ψ. But then (P, s, σ) |= Cψ, which is a contradiction.

We can now easily extend the above result to the model checking problem for AC-MAS.

Theorem 3.12 Consider two bisimilar and uniform AC-MAS P and P , and an FO-CTLK formula ϕ. If

1. for all t.e. runs r s.t. r(0) = s0, and for all k 0, |U | |adom(r(k)) adom(r(k + 1)) Con| + |var(ϕ)|, and

2. for all t.e. runs r s.t. r (0) = s 0, and for all k 0, |U| |adom(r (k)) adom(r (k + 1)) Con| + |var(ϕ)|

P |= ϕ iff P |= ϕ.

Proof. Equivalently, we prove that if (P, s0, σ) |= ϕ for some σ, then there exists a σ

s.t. (P , s 0, σ ) |= ϕ, and viceversa. To this end, observe that hypotheses (1) and (2) imply, respectively, hypotheses (1) and (2) of Theorem 3.11. Further, notice that, by cardinality considerations, given the assignment σ : V ar 7 U, there exists an assignment σ : V ar 7 U s.t. σ and σ are equivalent for ϕ w.r.t. s0 and s 0. Thus, by applying Theorem 3.11 we have that if there exists an assignment σ s.t. (P, s0, σ) |= ϕ, then there exists an assignment σ s.t. (P , s 0, σ ) |= ϕ. The converse can be proved analogously, as the hypotheses are symmetric.

This result shows that uniform AC-MAS can in principle be verified by model checking a bisimilar one. Note that this applies to an infinite AC-MAS P, as well. In this case the results above enable us to show that the verification question can be posed on the corresponding, possibly finite P as long as U , as defined above, is sufficiently large for P to bisimulate P. A noteworthy class of infinite systems for which these results prove particularly powerful is that of bounded AC-MAS, which, as discussed in the next subsection, always admit a finite abstraction.

3.3 Finite Abstractions

We now define a notion of finite abstraction for AC-MAS, and prove that, under uniformity, abstractions are bisimilar to the corresponding concrete model. We are particularly interested in finite abstractions; so we operate on a special class of infinite models that we call bounded.

Definition 3.13 (Bounded AC-MAS) An AC-MAS P is b-bounded, for b N, if for all s S, |adom(s)| b.

BELARDINELLI, LOMUSCIO & PATRIZI

An AC-MAS is b-bounded if none of its reachable states contain more than b distinct elements. Observe that bounded AC-MAS may be defined on infinite domains. Furthermore, note that a bbounded AC-MAS may contain infinitely many states, all bounded by b. So b-bounded systems are infinite-state in general. Notice also that the value b constrains only the number of distinct individuals in a state, not the size of the state itself, intended as the amount of memory required to accommodate the individuals. Indeed, the infinitely many elements in a domain U need an unbounded number of bits to be represented (e.g., as finite strings), so, even though each state is guaranteed to contain at most b distinct elements, nothing can be said about how large the actual space required by such elements is. Conversely, memory-bounded AC-MAS are finite-state (hence b-bounded, for some b). Since b-bounded AC-MAS are in general memory-unbounded, they cannot be verified by trivially generating and checking all their possibly infinite executions. However, we will show later that any b-bounded and uniform infinite-state AC-MAS admits a finite-state abstraction which can be used to verify it. We introduce abstractions in a modular manner by first introducing a set of abstract agents from a concrete AC-MAS.

Definition 3.14 (Abstract agent) Let A = D, Act, Pr be an agent defined on the interpretation domain U. Given an interpretation domain U , the abstract agent of A on U is the agent A = D , Act , Pr such that:

2. Act = Act;

3. α( u ) Pr (l ), with l D (U ), iff there exist l D(U) and α( u) Pr(l) s.t. l l, for some witness ι, and u = ι ( u), for some bijection ι extending ι to u.

Given a set Ag of agents defined on U, Ag denotes the set of corresponding abstractions on U of the agents in Ag.

We remark that the abstract agent A is an agent in line with Definition 2.6. Notice that the protocol of A is defined on the basis of its corresponding concrete agent A and requires the existence of a bijection between the elements in the corresponding local states and the action parameters. Thus, in order for a ground action of A to have a counterpart in A , the last requirement of Definition 3.14 constrains U to contain a sufficient number of distinct values. As it will become apparent later, the size of U determines how closely an abstract system can simulate its concrete counterpart. Notice also that, in general, an agent may not be an abstraction of itself on U, as for instance data may impact the agent s protocol. Next, we combine the notion of uniformity with that of boundedness. Our aim is to identify conditions under which the verification of an infinite AC-MAS can be reduced to the verification of a finite one. The main result here is given by Corollary 3.19 which guarantees that, in the context of bounded AC-MAS, uniformity is a sufficient condition for bisimilar finite abstractions to be satisfaction-preserving. In the following we assume that any AC-MAS P is such that adom(s0) Con. If this is not the case, Con can be extended so as to include all the (finitely many) elements in adom(s0). We start by formalising the notion of abstraction.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Definition 3.15 (Abstract AC-MAS) Let P = Ag, s0, τ be an AC-MAS and Ag the set of abstract agents obtained as in Definition 3.14 for some interpretation domain U . The AC-MAS P = Ag , s 0, τ is said to be an abstraction of P iff:

t τ (s , α( u )) iff there exist s, t S and α( u) Act(U) such that s t s t , for some witness ι, t τ(s, α( u)), and u = ι ( u) for some bijection ι extending ι to u.

It can be checked that P , as defined above, is indeed an AC-MAS as it satisfies the relevant conditions on protocols and transitions in Definition 2.7. Indeed, if t τ (s , α( u )), then there exist s, t S, and α( u) such that t τ(s, α( u)), s t s t for some witness ι, and u = ι ( u ) for some bijection ι extending ι. This means that αi( ui) Pri(li) for i n. By definition of Pr i we have that αi( u i) Pr i(l i) for i n. The definition requires abstractions to have initial states isomorphic to their concrete counterparts; specifically they have to be equal as adom(s0) Con. Moreover, the second constraint entails that a transition in the concrete model exists if and only if the same transition, up to renaming of the involved values, exists in the abstraction. So, for example, a copy action in the concrete model has a corresponding copy action in the abstract model. Crucially, this condition requires that the domain U contains enough elements to bisimulate the concrete states and action effects. This will be made precise in Lemma 3.17. Obviously, if U has finitely many elements, then S has finitely many states. Observe also that by varying U we obtain different abstractions. Finally, notice that an AC-MAS is not necessarily an abstraction of itself. This issue is addressed in Lemma 3.16. Next, we investigate the relationship between an AC-MAS and its abstractions. A first useful result states that every finite abstraction is uniform, independently of the properties of the AC-MAS they abstract.

Lemma 3.16 Every abstraction P of an AC-MAS P is uniform. Moreover, if P is uniform and U = U, then P = P.

Proof. Consider s, t, s S , t D(U ), and α( u) Act (U ) s.t. t τ (s, α( u)) and s t s t , for some witness ζ. We need to show that P admits a transition from s to t . Since P is an abstraction of P, given the definition of τ , there exist s , t S and α( u ) Act(U) s.t. t τ(s , α( u )), s t s t, for some witness ι, and u = ι ( u ), for some constantpreserving bijection ι extending ι to u . Consider u U | u| such that u = ζ ( u), for some constant-preserving bijection ζ extending ζ to u. Obviously, the composition ζ ι is a constantpreserving bijection such that u = ζ (ι ( u )). Moreover, it can be restricted to a witness for s t s t . But then, since P is an abstraction of P, this implies that t τ (s , α( u )). Thus, P is uniform. Moreover, to prove that P is an abstraction of itself every time P is uniform and U = U, we notice that if the transition t τ(s, α( u)) is in P, then it is also in P by the definition of abstraction. Also, if the transition t τ (s , α( u )) appears in P , then there exist s, t S and α( u) Act( U) s.t. s t s t for some witness ι, t τ(s, α( u)), and u = ι ( u) for some constant-preserving bijection ι extending ι to u. Finally, since P is uniform it is the case that the transition t τ (s , α( u )) is in P as well.

BELARDINELLI, LOMUSCIO & PATRIZI

This lemma provides sufficient conditions under which an AC-MAS is an abstraction of itself, namely being uniform and having the same interpretation domain. The second result below guarantees that every uniform, b-bounded AC-MAS is bisimilar to any of its abstractions, provided these are built over a sufficiently large interpretation domain. In the following, we take NAg = NAg = P Ai Ag maxα( x) Acti{| x|}, i.e., NAg is the sum of the maximum number of parameters contained in the action types of each agent in Ag.

Lemma 3.17 Consider a uniform, b-bounded AC-MAS P over an infinite interpretation domain U, and an interpretation domain U such that Con U . If |U | 2b + |Con| + NAg, then any abstraction P of P over U is bisimilar to P.

Proof. Let B = { s, s S S | s s }. We prove that B is a bisimulation such that s0, s 0 B. We start by proving that B is a simulation relation. To this end, observe that since s0 = s 0, then s0 s 0, and s0, s 0 B. Next, consider s, s B, thus s s . Assume that s t, for some t S. Then, there must exist α( u) Act(U) such that t τ(s, α( u)). Moreover, since |U | 2b + |Con| + NAg, P Ai Ag | ui| NAg, and |adom(s) adom(t)| 2b, the witness ι for s s can be extended to S Ai Ag ui as a bijection ι . Now let t = ι (t). By the way ι has been defined, it can be seen that s t s t . Further, since P is an abstraction of P, we have that t τ (s , α( u )) for u = ι ( u), that is, s t in P . Therefore, there exists t S such that s t , s t s t , and t, t B. As regards the epistemic relation, assume s i t for some i {1, . . . , n} and t S. By definition of i, li(s) = li(t). Since |U | 2b + |Con|, any witness ι for s s can be extended to a witness ι for s t s t , where t = ι (t). Obviously, li(s ) = li(t ). Thus, to prove that s i t , we are left to show that t S , i.e., that t is reachable in P from s 0 = s0. To this end, observe that since t S, there exists a purely temporal run r such that r(0) = s0 and r(k) = t, for some k 0. Thus, there exist α1( u1) . . . , αk( uk) such that r(j + 1) τ(r(j), αj+1( uj+1)), for 0 j < k. Since |U | 2b + |Con|, we can define, for 0 j < k, a function ιj that is a witness for r(j) r(j +1) ιj(r(j)) ιj(r(j +1)). In particular, this can be done starting from j = k 1, defining ιk 1 so that ιk 1(r(k)) = ιk 1(t) = t , and proceeding backward to j = 0, so that, for 0 j < k, we have ιj(r(j + 1)) = ιj+1(r(j + 1)). Observe that since adom(s0) Con, necessarily i0(r(0)) = i0(s0) = s0 = s 0. Moreover, as |U | 2b + |Con| + NAg, each ιj can be extended to a bijection ι j, to the elements occurring in uj+1. Thus, given that P is an abstraction of P, for 0 j < k, we have that ι j(r(j + 1)) τ(ι j(r(j)), α(ι j( uj+1))). Hence, the sequence ι 0(r(0)) ι k 1(r(k)) is a run of P , and, since t = ι k 1(r(k)), t is reachable in P . Therefore s i t . Further, since t t , by definition of B, it is the case that t, t B, hence B is a simulation. To prove that B 1 is a simulation, given s, s B (thus s s ), assume that s t , for some t S . Obviously, there exists α( u ) Act(U ) such that t τ (s , α( u )). Because P is an abstraction of P, there exist s , t S and α( u ) Act(U) such that s t s t , for some witness ι, and t τ(s , α( u )), with u = ι ( u ), for some bijection ι extending ι to u . Observe that s s , thus, by transitivity of we have s s . The fact that there exists t S such that s t easily follows from the uniformity of P. Thus, since t t, we have t, t B. For the epistemic relation, assume s i t for some t S and 0 < i n. Let ι be a witness for s s, and let ι be an extension of ι that is a witness for s t s t. For t = ι (t ), it can be seen that li(s) = li(t). Observe that t S . Using an argument analogous to the one above, but exploiting the fact that P is uniform, that P is certainly b-bounded, and that |U| > 2b + |Con| + NAg as U is infinite, we can show that t S by constructing a run r of P such that r(k) = t, for some k 0.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Then s i t. Further, since t t, we have t, t B. Therefore, B 1 is a simulation. So, P and P are bisimilar.

This result allows us to prove our main abstraction theorem.

Theorem 3.18 Consider a b-bounded and uniform AC-MAS P over an infinite interpretation domain U, an FO-CTLK formula ϕ, and an interpretation domain U such that Con U . If |U | 2b + |Con| + max{|vars(ϕ)|, NAg}, then for any abstraction P of P over U , we have that:

P |= ϕ iff P |= ϕ.

Proof. By Lemma 3.16, P is uniform. Thus, by the hypothesis on the cardinalities of U and U , Lemma 3.17 applies, so P and P are bisimilar. Obviously, also P is b-bounded. Thus, since P and P are b-bounded, and by the cardinality hypothesis on U and U , Theorem 3.12 applies. In particular, notice that for every temporal-epistemic run r s.t. r(0) = s0, and for all k 0, we have that |U | |adom(r(k)) adom(r(k+1)) Con|+|var(ϕ)|, as |adom(r(k))| b by b-boundedness. Therefore, P |= ϕ iff P |= ϕ.

It follows that by using a sufficiently large number of abstract values in U , we can reduce the verification of an infinite, bounded, and uniform AC-MAS to the verification of a finite one.

Corollary 3.19 Given a b-bounded and uniform AC-MAS P over an infinite interpretation domain U, and an FO-CTLK formula ϕ, there exists an AC-MAS P over a finite interpretation domain U

such that P |= ϕ iff P |= ϕ.

It should also be noted that U can simply be taken to be any finite subset of U (including Con) satisfying the cardinality requirement above. By doing so, the finite abstraction P can be defined simply as the restriction of P to U . Thus, every infinite, b-bounded and uniform AC-MAS is bisimilar to a finite subsystem, which then satisfies the same formulas. Note that we are not concerned with the actual construction of the finite abstraction. This is because we intend to construct it directly from an artifact-centric program, as we will do in Section 4. Before that, we explore the complexity of the model checking problem.

3.4 The Complexity of Model Checking Finite AC-MAS against FO-CTLK Specifications

We now analyse the complexity of the model checking problem for finite AC-MAS with respect to FO-CTLK specifications. The input of the problem consists of an AC-MAS P on a finite domain U and an FO-CTLK formula ϕ; the output is an assignment σ such that (P, s0, σ) |= ϕ, whenever the property is satisfied. Hereafter we follow standard literature for basic notions and definitions (Grohe, 2001). To encode an AC-MAS P we use a tuple EP = U, D, s0, Φτ , where U is the (finite) interpretation domain, D is the global database schema, s0 is the initial state, and Φτ = {φ α1, . . . , φ αm} is a set of FO-formulas, each capturing the transitions associated with a ground joint action αi. Since U is finite, so is the set of ground actions, thus Φτ. Each ϕ αi is a FO-formula over the alphabet DAg D Ag, where DAg = {P j i /qi | Pi/qi D, j n} is the set containing one distinct relation symbol P j i , for each agent j n and the relation symbol Pi D. We take Φτ such that s τ(s, α)

BELARDINELLI, LOMUSCIO & PATRIZI

iff DAg D Ag |= φ α, for s, s D(U), such that for every Pi D and j n, lj(Pi) = DAg(P j i ) and l j(Pi) = D Ag(P j i ). As an example, for D = {P} (thus DAg = {P j | j n}) and an action type α with no parameters, consider the formula φ α = Vn j=0 x P j (x) P j(x), which intuitively captures all transitions in which in the successor state predicate P contains all and only those elements of U that in the current state are not in P. It can be proved that every transition relation τ can be represented as discussed above, and that, given EP, the size ||P|| .= |S|+|τ| of the encoded AC-MAS P is such that ||P|| |Act| |U|pmax 23ℓqmax, where: pmax is the largest number of parameters in some action type of Act, ℓis the number of relation symbols in D, and qmax is the largest arity of such symbols. This corresponds to a doubly exponential bound for ||P|| w.r.t. ||EP|| .= |U| + ||D|| + |Φτ|, where ||D|| = P Pk D qk,

for qk the arity of Pk. Specifically, we have ||P|| 23 2||EP ||4 . We carry out the complexity analysis on the basis of the input above; clearly the same results apply for equally compact inputs such as the AC programs to be presented in Section 4. We consider the combined complexity of the input, that is, ||EP|| + ||ϕ||. We say that the combined complexity of model checking finite AC-MAS against FO-CTLK specifications is EXPSPACE-complete if the problem is in EXPSPACE, i.e., there is a polynomial p(x) and an algorithm solving the problem in space bounded by 2p(||EP||+||ϕ||), and the problem is EXPSPACEhard, i.e., every EXPSPACE problem can be reduced to model checking finite AC-MAS against FO-CTLK specifications.

Theorem 3.20 The model checking problem for finite AC-MAS succinctly presented as above against FO-CTLK specifications is EXPSPACE-complete.

Proof. To show that the problem is in EXPSPACE, recall that ||P|| is at most doubly exponential w.r.t. the size of the input, thus so is |S|. We describe an algorithm that works in NEXPSPACE; this combines the algorithm for model checking the first-order fragment of FO-CTLK and that for the temporal-epistemic fragment. Since NEXPSPACE = EXPSPACE, the result follows. Given an ACMAS P and an FO-CTLK formula ϕ, we guess an assignment σ and check whether (P, s0, σ) |= ϕ. This can be done by induction according to the structure of ϕ. If ϕ is atomic, this check can be done in polynomial time w.r.t. the size of the state it is evaluated on, that is, exponential time w.r.t. ||EP||. If ϕ is of the form xψ, then we can apply the algorithm for model checking first-order (non-modal) logic, which works in PSPACE. Finally, if the outmost operator in ϕ is either a temporal or epistemic modality, then we can extend the automata-based algorithm to model check propositional CTL (Kupferman, Vardi, & Wolper, 2000; Lomuscio & Raimondi, 2006), which works in logarithmic space in |S|. However, we remarked above that |S| is generally doubly exponential in ||EP||. Thus, this step can be performed in space singly exponential in ||EP||. All these steps can be performed in time polynomial in the size of ϕ. As a result, the total combined complexity of model checking finite AC-MAS is in NEXPSPACE = EXPSPACE. To prove that the problem is EXPSPACE-hard we show a reduction from any problem in EXPSPACE. We assume standard definitions of Turing machines and reductions (Papadimitriou, 1994). If A is a problem in EXPSPACE, then there exists a deterministic Turing machine TA = Q, Σ, q0, F, δ , where Q is the finite set of states, Σ the machine alphabet, q0 Q the initial state, F the set of accepting states, and δ the transition function, that solves A using at most space 2p(|in|) on a given input in, for some polynomial function p. As standard, we assume δ to be a

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

relation on (Q Σ Q Σ D), with D = {L, R}, and q, c, q , c , d δ representing a transition from state q to state q , with characters c and c read and written respectively , and head direction d ((L)eft and (R)ight). Without loss of generality, we assume that TA uses only the righthand half of the tape. From TA and in, we build an encoding EP = D, U, s0, Φτ of an AC-MAS P induced by a single (environment) agent AE = DE, Act E, Pr E defined on U = Σ Q {0, 1}, where: (i) DE = {P/p(|in|)+ 1, Q/1, H/p(|in|), F/1}; (ii) Act E is the singleton {αE}, with αE parameterfree; (iii) αE Pr E(l E) for every l E D(U). Intuitively, the states of P correspond to configurations of TA, while τ mimics δ. To define EP, we let D = DE. The intended meaning of the predicates in D is as follows: the first p(|in|) elements of a P-tuple encode (in binaries) the position of a non-blank cell, and the (p(|in|) + 1)-th element contains the symbol appearing in that cell; Q contains the current state q of TA; H contains the position of the cell the head is currently on; F contains the final states of TA, i.e., F = F. The initial state s0 represents the initial configuration of TA, that is, for in = in0 inℓ: s(Q) = {q0}; s(H) = { 0, . . . , 0 }; and s(P) = { BIN(i), ini | i {0, . . . , ℓ}}, where BIN(i) stands for the binary encoding in p(|in|) bits of the integer i. Observe that p(|in|) bits are enough to index the (at most) 2p(|in|) cells used by TA. As to the transition relation, we define Φτ = {φαE}, where (we avoid suband superscripts in predicate symbols, i.e., D = DAg as no ambiguity can arise with only one agent):

q,c,q ,c ,d δ ( x F(x) F (x)) (1)

Q(q) ( x Q(x) x = q) Q (q ) ( x Q (x) x = q ) (2)

p(H( p) ( x H(x) x = p) (P( p, c) (c = 2 x P( p, x)))) (3)

p (d = R SUCC( p, p )) (d = L SUCC( p , p)) H ( p ) ( x H (x) x = p ) (4)

(P ( p, c ) (c = 2)) ( x P ( p, x) x = c ) (5)

( x, y(P( x, y) ( x = p) P ( x, y)) ( x, y P ( x, y) (P( x, y) ( x = p y = c )))) (6)

The symbol 2 represents the content of blank cells, while SUCC( x, x ) = Vp(|in|) i=1 (x i = 0 x i = 1) (x i = 1 ((x i = 0 Vi 1 j=1 xj = 1) (x i = 1 Vi 1 j=1 xj = 1))) is a formula capturing that x is the successor of x, for x and x interpreted as p(|in|)-bit binary encodings of integers (observe that {0, 1} U). Such a formula can obviously be written in polynomial time w.r.t. p(|in|), as well as EP, and in particular s0 and φαE. Formula φαE is obtained as a disjunction of subformulas, each referring to a transition of δ. For each subformula, i.e., transition q, c, q , c , d : line 1 expresses that F, which encodes the final states of the machine, does not change along the transition (this formula could be moved out of the big disjunction); line 2 encodes that the machine will be in exactly one state, q , after the transition takes place; line 3 expresses that the symbol read by the head is c (possibly blank); line 4 captures that the head moves in direction d; line 5 states that the head writes symbol c on the cell, before moving; finally, line 6 states that the content of the tape does not change, except for the cell that the head is on. The obtained transition function is such that τ(s, αE) = s iff, for δ(q, c) = (q , c , d) in TA, we have that: s (P) is obtained from s(P) by overwriting with c (if not blank) the symbol in position (p(|in|) + 1) of the tuple in s(P) beginning with the p(|in|)-tuple s(H) (that is, c by definition of φαE); by updating s(H) according to d, that is by increasing or decreasing the value it contains; and

BELARDINELLI, LOMUSCIO & PATRIZI

by setting s (Q) = {q }. The predicate F does not change. Observe that cells not occurring in P are interpreted as if containing 2 and when 2 is to be written on a cell, the cell is simply removed from P. It can be checked that, starting with s = s0, by iteratively generating the successor state s

according to Φτ, i.e., s s.t. s s |= φαE, one obtains a (single) P-run that is a representation of the computation of TA on in, where each pair of consecutive P-states corresponds to a computation step. In particular, at each state, Q contains the current state of TA. It should be clear that ϕ = EF( x Q(x) F(x)) holds in P iff TA accepts in. Thus, by model checking ϕ on P, we can check whether TA accepts in. This completes the proof of EXPSPACE-hardness.

Note that the result above is given in terms of the data structures in the model, i.e., U and D, and not the state space S itself. This accounts for the high complexity of model checking AC-MAS, as the state space is doubly exponential in the size of the data. By analysing the refined bound on the size of ||P|| (||P|| |Act| |U|pmax 23ℓqmax), it can be seen that the double exponential is essentially due to the number of parameters in action types, the number of relation symbols occurring in D, and their respective arities. Thus, for fixed database schema and set of action types, the resulting space complexity is reduced to singly exponential. While EXPSPACE-hardness indicates intractability, we note that this is to be expected given that we are dealing with quantified structures which are in principle prone to high complexity. Recall also from Section 3.3 that the size of the interpretation domain U of the abstraction P is linear in the bound b, the number of constants in Con, the size of φ, and NAg. Hence, model checking bounded and uniform AC-MAS is EXPSPACE-complete with respect to these elements, whose size will generally be small. Thus, we believe that in several cases of practical interest model checking AC-MAS may be entirely feasible.

4. Artifact-Centric Programs

We have so far developed a formalism that can be used to specify and reason about temporalepistemic properties of models representing artifact-centric systems. We have identified a notable class of models that admit finite abstractions. As we remarked in the Introduction, however, artifact systems are typically implemented through declarative languages such as GSM (Hull et al., 2011). It is therefore of interest to investigate the verification problem, not just on a Kripke semantics such as AC-MAS, but on actual programs. As discussed, while GSM is a mainstream declarative language for artifact-centric environments, alternative declarative approaches exist. In what follows for the sake of generality we ground our discussion on a very wide class of declarative languages and define the notion of artifact-centric program. Intuitively, an artifact-centric program (or AC program) is a declarative description of a whole multi-agent system, i.e., a set of services, that interact with the artifact system (see the discussion in the Introduction). Since artifact systems are also typically implemented declaratively (Heath et al., 2013), AC programs will be used to encode both the artifact system itself and the agents in the system. This also enables us to import into the formalism the previously discussed features of views and windows typical in GSM and other languages. The rest of this section is organised as follows. We begin in Subsection 4.1 by defining AC programs and giving their semantics in terms of AC-MAS. We then show that any AC-MAS that results from an AC program is uniform. As long as the generated AC-MAS is bounded, by using the results of Section 3.3, we deduce that any AC program admits an AC-MAS as its finite model. In this

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

context it is important to give constructive procedures for the generation of the finite abstraction; we provide such a procedure here. This enables us to state that, under the assumptions we identify, AC programs admit decidable verification by means of model checking their finite model. In Section 4.2 we ground and exemplify the constructions above on the Order-to-Cash Scenario introduced in Subsection 2.4.

4.1 Verifying Artifact-Centric Programs

We start by defining the abstract syntax of AC programs.

Definition 4.1 (AC Programs) An artifact-centric program (or AC program) is a tuple ACP = D, U, Σ, Ψ , where:

D is the program s database schema;

U is the program s interpretation domain;

Σ = {Σ0, . . . , Σn} is the set of agent programs Σi = Di, li0, Acti , where:

Di D is agent i s database schema;

li0 Di(U) is agent i s initial state (as a database instance);

Acti is a set of local actions α( x), where α is the action name and x are the action parameter names; without loss of generality, we assume that no two action types use the same parameter names;

each local action α( x) is associated with a precondition πα( x)( y), i.e., an FO-formula over Di, where y x are free variables.

Ψ = {ψ α( x)( z) | α( x) = α1( x1), . . . , αn( xn) Act1 Actn, x = x1, . . . , xn , z x} represents the AC program s transitions expressed as a set of postconditions, i.e., FOformulas over action parameters as free variables. The formulas in Ψ are defined over the alphabet DAg D Ag, where DAg = {P j i /qi | Pi/qi D, j n} is the set containing one distinct relation symbol P j i , for each agent j n and relation symbol Pi D.

AC programs are defined modularly by giving all the agents programs, including their action preconditions and postconditions. Notice that preconditions use relation symbols from the local database only, while the program s transitions Ψ refer to the local relations for all agents in an unconstrained way. More precisely, postconditions are global, i.e., they are associated with global actions, rather than local ones. Indeed, a formula ψ α( x)( z) describes the effects of the execution of the global action α( z) (under a particular assignment to the parameters) where each agent i executes αi( zi). As reported below, this accounts for the intuition that in choosing the next action, an agent can only rely on information locally stored, while its actions, as a result of mutual interactions, may change the local state of any agent, i.e., they affect the global state of the system. Obviously, this does not prevent the possibility of specifying actions that affect local states only. This is in line with the AC-MAS semantics and the literature on interpreted systems. Given a tuple x of variables and a tuplue u of elements from U such that | x| = | u|, by σ( x) = u we denote an assignment that binds the i-th component of u to the i-th component of x. For a joint action α( x) given as above, we let con( α) = S i n con(πi) con(ψ), var( α) = S i n var(πi)

BELARDINELLI, LOMUSCIO & PATRIZI

var(ψ), and free( α) = x. An execution of α( x) with ground parameters u U| x| is the ground action α( u), where v (resp. w) is obtained by replacing each yi (resp. zi) with the value occurring in u at the same position as yi (resp. zi) in x. Such replacements make both each πi( v) and ψ( w) ground, that is, first-order sentences. Finally, we define the set Con ACP of all constants mentioned in the AC program ACP, i.e., Con ACP = Sn i=1 adom(li0) S α Act con( α). The semantics of an AC program is given in terms of the AC-MAS induced by the agents that the program implicitly defines. Formally, this is captured by the following definition.

Definition 4.2 (Induced Agents) Given an AC program ACP = D, U, Σ, Ψ , an agent A = Di, Acti, Pri is induced by ACP on the interpretation domain U iff for the agent program Σi = Di, li0, Acti Σ we have that:

for every li Di(U) and ground action α( u) such that α( x) Acti, it is the case that α( u) Pri(li) iff (li, σ) |= πα( x)( y), for σ( x) = u (recall that y x).

Note that induced agents are agents as formalised in Definition 2.6. Agents defined as above are composed to give the AC-MAS associated with an AC program.

Definition 4.3 (Induced AC-MAS) Given an AC program ACP = D, U, Σ, Φ and the set Ag = {A0, . . . , An} of all agents induced by ACP, the AC-MAS induced by ACP is the tuple PACP = Ag, s0, τ , where:

s0 = l00, . . . , ln0 is the initial global state;

τ is the global transition function defined by the following condition: s τ(s, α( u)), where s = l0, . . . , ln , s = l 0, . . . , l n , α( u) = α1( u0), . . . , αn( un) , u = u0, . . . , un , iff for every i {0, . . . , n},

(li, σi) |= παi( xi)( yi) for σi( xi) = ui;

adom(s ) adom(s) u con(ψ α( x));

(DAg D Ag, σ) |= ψ α( x)( z), for an assignment σ such that σ( x) = u, and DAg, D Ag are the DAg-instances such that, for every Pi D and j n, DAg(P j i ) = lj(Pi) and D Ag(P j i ) = l j(Pi).

Given an AC program ACP, its induced AC-MAS represents the program s execution tree and encodes all the data in the system. Intuitively, this is obtained by iteratively executing at each state, starting from the initial one, all possible ground actions. Observe that all actions performed are enabled by the respective protocols and that transitions can introduce only a bounded number of new elements in the active domain, i.e., those bound to the action parameters. It follows from the above that AC programs are parametric with respect to the interpretation domain, i.e., by replacing the interpretation domain we obtain a different AC-MAS. We assume that every program induces an AC-MAS whose transition relation is serial, i.e., states always have successors. This is a basic requirement that can be easily fulfilled, for instance, by assuming that each agent has a skip action with a trivially true precondition and that when all agents execute skip, the global state of the system remains unchanged. In the next Subsection we present an example of one such program. A significant feature of AC programs is that they induce uniform AC-MAS.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Lemma 4.4 Every AC-MAS P induced by an AC program ACP is uniform.

Proof. Since by definition adom(s0) Con ACP , by Prop. 3.7 it is sufficient to consider only the temporal transition relation . Consider s, s , s S and s L0 Ln such that s s s s for some witness ι. In particular, for every Aj Ag, l j lj and l j l j, namely, l j = ι(lj) and l j = ι(l j). Also, assume that there exists α( u) = α1( u1), . . . , αn( un) Act(U) such that s τ(s, α( u)). First of all, αj( uj) Prj(lj) implies that (lj, σj) |= παj( xj)( yj) for σj( xj) = uj. Since l j lj, by Prop. 3.3 we have that (l j , σ j) |= παj( xj)( yj) where σ j( xi) = ι ( ui) for any ι extending ι to ui. Thus, αj(ι ( uj)) Prj(l j ) for every j Ag. Further, assume that (DAg D Ag, σ) |= ψ α( x)( z), where DAg, D Ag are the DAg-instances obtained as above and σ( x) = u. Consider the DAg-instances D Ag, D Ag such that D Ag(P j i ) = l j (Pi) = ι(lj(Pi)), and D Ag(P j i ) = l j (Pi) = ι(l j(Pi)). Since s s s s , we obtain that DAg D Ag D Ag D Ag for the same witness ι. In particular, (D Ag D Ag, σ ) |= ψ α( x)( z), where σ ( x) = ι ( u) for any ι

extending ι to u. Finally, it can be easily checked that adom(s ) adom(s ) ι ( u) con(ψ α( x)). As a result, s τ(s , α(ι ( u))), i.e., P is uniform.

We can now define what it means for an AC program to satisfy a specification, by referring to its induced AC-MAS.

Definition 4.5 Given an AC program ACP, a FO-CTLK formula ϕ, and an assignment σ, we say that ACP satisfies ϕ under σ, written (ACP, σ) |= ϕ, iff (PACP , s0, σ) |= ϕ.

Thus, the model checking problem for an AC program against a specification φ is defined in terms of the model checking problem for the corresponding AC-MAS PACP against φ. The following result allows us to reduce the verification of any AC program with an infinite interpretation domain U1, that induces a b-bounded AC-MAS, to the verification of an AC program over a finite U2. To show how this is constructed, we let NACP = P i {1,...,n} maxα( x) Ωi{| x|} be the maximum number of different parameters that can occur in a joint action of ACP.

Lemma 4.6 Consider an AC program ACP1 = D, U1, Σ operating on an infinite interpretation domain U1 and assume that its induced AC-MAS PACP1 = Ag1, s10, τ1 is b-bounded. Consider a finite interpretation domain U2 such that Con ACP1 U2 and |U2| 2b + |Con ACP1| + NACP1 and the AC program ACP2 = D, U2, Σ . Then, the AC-MAS PACP2 = Ag2, s20, τ2 induced by ACP2 is a finite abstraction of PACP1.

Proof. Let Ag1 and Ag2 be the set of agents induced respectively by ACP1 and ACP2, according to Def. 4.2. Firstly, we prove that the set Ag1 and Ag2 of agents satisfy Def. 3.14, for Ag = Ag1 and Ag = Ag2. To this end, observe that because ACP1 and ACP2 differ only in U, by Def. 4.2, D = D , and Act = Act. Thus, only requirement 3 of Def. 3.14 needs to be checked. For this, fix i {1, . . . , n} and assume that α( u) Pri(li). By Def. 4.2, we have that (li, σ) |= παi( xi)( yi) for σ( xi) = ui. By the assumption on |U2|, since con(α) Con ACP1 U2, | u| NACP1, and |adom(li)| b, we can define an injective function ι : adom(li) u Con ACP1 7 U2 that is the identity on Con ACP1. Thus, for l i = ι(li), we can easily extract from ι a witness for li l i. Moreover, it can be seen that σ(y) = v and σ (y) = v = ι( v) are equivalent for π. Then, by applying Prop. 3.3 to li and l i, we conclude that (l i, σ ) |= παi( xi)( yi). Hence, by Def. 4.2, α( u ) Pr i(l i) for u = ι( u). So, we have shown the right-to-left part of requirement 3. The left-to-right part can be shown similarly and more simply since U1 is infinite.

BELARDINELLI, LOMUSCIO & PATRIZI

Thus, we have proven that Ag = Ag1 and Ag = Ag2 are obtained as in Def. 3.14. Hence, the assumption on Ag and Ag in Def. 3.15 is fulfilled. We show next that also the remaining requirements of Def. 3.15 are satisfied. Obviously, since Σ is the same for ACP1 and ACP2, by Def. 4.3, s10 = s20, so the initial states of PACP1 and PACP2 are the same. It remains to show that the requirements on τ1 and τ2 are satisfied. We prove the right-to-left part. To this end, take two states s1 = l10, . . . , l1n , s 1 = l 10, . . . , l 1n in S1 and a joint action α( u) = α0( u0), . . . , αn( un) Act(U1) such that s 1 τ1(s1, α( u)). Consider s1 s 1. By the assumptions on U2, there exists an injective function ι : adom(s1) adom(s 1) u Con ACP1 7 U2 that is the identity on Con ACP1 (recall that |adom(s1)|, |adom(s 1)| b). Then, for s2 = ι(l10), . . . , ι(l1n) , s 2 = ι(l 10), . . . , ι(l 1n) in S2, we can extract from ι a witness for s1 s 1 s2 s 2. Moreover, it can be seen that for every παi( xi) and ψ α( x), the assignments σ( x) = u and σ ( x) = u = ι( u) are equivalent with respect to s1 s 1 and s2 s 2. Now, consider Def. 4.3 and recall that both PACP1 and PACP2 are AC-MAS induced by ACP1 and ACP2, respectively. By applying Prop. 3.3, we have that, for i {0, . . . , n}, (i) (ι(l1i), σ ) |= παi( xi)( yi) iff (l1i, σ) |= παi( xi)( yi); (ii) (DAg2 D Ag2, σ ) |= ψ α( x)( zi) iff (DAg1 D Ag1, σ) |= ψ α( x)( zi), where each DAgi is obtained from si as detailed in Def. 4.3; (iii) adom(s 1) adom(s1) u con(ψ α( x)) iff adom(s 2) adom(s2) ι( u) con(ψ α( x)) by the definition of ι. But then, it is the case that s 2 τ2(s2, α(ι( u))). So we have proved the right-to-left part of the second requirement of Def. 3.15. The other direction follows similarly. Therefore, PACP2 is an abstraction of PACP1.

Intuitively, Lemma 4.6 shows that the following diagram commutes, where [U1/U2] stands for the replacement of U1 by U2 in the definition of ACP1. Observe that since U2 is finite, one can actually apply Def. 4.3 to obtain PACP2; in particular the transition function τ2 can be computed. Instead, PACP1, and in particular τ1, cannot be directly computed from ACP1 by applying Def. 4.3, as U1 is infinite.

ACP1 Def. 4.3

Def. 3.15 ACP2 Def. 4.3 / PACP2

The following result, a direct consequence of Lemma 3.17 and Lemma 4.6, is the key conclusion of this section.

Theorem 4.7 Consider an FO-CTLK formula ϕ, an AC program ACP1 operating on an infinite interpretation domain U1 and assume its induced AC-MAS PACP1 is b-bounded. Consider a finite interpretation domain U2 such that CACP1 U2 and |U2| 2b+|CACP1|+max{NACP1, |var(ϕ)|}, and the AC program ACP2 = D, U2, Σ . Then we have that:

ACP1 |= ϕ iff ACP2 |= ϕ.

Proof. By Lemma 4.6 PACP2 is a finite abstraction of PACP1. Moreover, |U2| 2b + |Con ACP1| + max{NACP1, |var(ϕ)|} implies |U2| 2b + |Con ACP1| + |var(ϕ)|. Hence, we can apply Lemma 3.17 and the result follows.

The results shows that if the generated AC-MAS model is bounded, then any AC program can be verified by model checking its finite abstraction, i.e., a bisimilar AC-MAS defined on a finite

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

interpretation domain. Note that the procedure is constructive: given an AC program ACP1 = D, U1, Σ on an infinite domain U1 and an FO-CTLK formula ϕ, to check whether ACP1 satisfies the specification ϕ, we first consider its finite abstraction ACP2 = D, U2, Σ defined on a finite domain U2 satisfying the cardinality requirement of Theorem 4.7. Since U2 is finite, the induced AC-MAS PACP2 is also finite; hence we can apply standard model checking techniques to verify whether PACP2 satisfies ϕ. Finally, by definition of satisfaction for AC programs and Theorem 4.7, we can transfer the result obtained to decide the model checking problem for the original infinite AC program ACP1 against the specification ϕ. Also observe that in the finite abstraction considered above the abstract interpretation domain U2 depends on the number of distinct variables that the specification ϕ contains. Thus, in principle, to check the same AS program against a different specification ϕ , one should construct a new abstraction PACP 2 using a different interpretation domain U 2, and then check ϕ against it. However, it can be seen that if the number of distinct variables of ϕ does not exceed that of ϕ, the abstraction PACP2, used to check ϕ, can be re-used for ϕ . Formally, let FO-CTLKk be the set of all FO-CTLK formulas containing at most k distinct variables. We have the following corollary to Theorem 4.7.

Corollary 4.8 If |U2| 2b + |Con ACP1| + max{NACP1, k}, then, for every FO-CTLKk formula ϕ, ACP1 |= ϕ iff ACP2 |= ϕ.

This result holds in particular for k = NACP ; thus for FO-CTLKNACP formulas, we have an abstraction procedure that is specification-independent. Theorem 4.7 requires the induced AC-MAS to be bounded, which may seem a difficult condition to check a priori. Note however that AC programs are declarative. It is therefore straightforward to give postconditions that enforce that no transition will generate states violating the boundedness requirement. The scenario in the next Subsection will exemplify this.

4.2 Verifying the Order-to-Cash Scenario

In Section 2.4 we introduced the order-to-cash scenario (Hull et al., 2011), a business process modelled as an artifact-centric system. Now we show how it can be formalised within the framework of AC programs. For the sake of simplicity we assumed only three agents in our scenario: one customer c, one manufacturer m and one supplier s. Further, the database schema Di for each agent i {c, m, s} was given as:

Customer c: Dc = {Products(pcode, budget), PO(id, pcode, offer, status)};

Manufacturer m: Dm = {PO(id, pcode, offer, status), MO(id, pcode, price, status)};

Supplier s: Ds = {Materials(mcode, cost), MO(id, pcode, price, status)}.

Also, we assumed that in the initial state the only non-empty relations are Products and Materials. Hence, the artifact-centric program ACPotc corresponding to the order-to-cash scenario can be given formally as follows:

Definition 4.9 (ACPotc) The artifact-centric program ACPotc is a tuple Dotc, Uotc, Σotc, Ψotc , where:

the program s database schema Dotc and interpretation domain Uotc are defined as in Sec. 2.4, i.e., Dotc = Dc Dm Ds = {PO/4, MO/4, Products/2, Materials/2} and Uotc is the set of all alphanumeric strings.

BELARDINELLI, LOMUSCIO & PATRIZI

πcreate PO(id,pcode) = b.Products(b, pcode) requires id to be a fresh identifier for p, o, s.PO(id, p, o, s) POs, and the newly created PO to refer to an existing product πdone MO(id) = pc, p.MO(id, pc, p, preparation) requires id to refer to an existing MO currently in preparation πaccept MO(id) = pc, p.MO(id, pc, p, submitted) which requires id to refer to an existing MO that has been submitted

Table 1: Preconditions for the actions create PO(id, pcode), done MO(id), and accept MO(id)

Σ = {Σc, Σm, Σs} is the set of agent specifications for the customer c, the manufacturer m and the supplier s. Specifically, for each i {c, m, s}, Σi = Di, li0, Acti, Πi is such that:

Di D is agent i s database schema as detailed above, i.e., Dc = {Products/2, PO/4}, Dm = {PO/4, MO/4}, and Ds = {MO/4, Materials/2}.

lc0, lm0, and ls0 are database instances in Dc(Uotc), Dm(Uotc), and Ds(Uotc) respectively s.t. lc0(Products) and ls0(Materials) are non-empty, i.e., they contain some background information, while lc0(PO), lm0(PO), lm0(MO) and ls0(MO) are all empty.

The sets of actions are given as

Actc = {create PO(id, pcode), submit PO(id), pay(id), delete PO(id), skip}. Actm = {create MO(id, price), done MO(id), ship PO(id), delete MO(id), skip}; Acts = {accept MO(id), reject MO(id), ship MO(id), skip}.

Each action α( x) is associated with a precondition πα( x). The preconditions for the actions create PO(id, pcode), done MO(id), accept MO(id) are reported in Table 1. The remaining preconditions are omitted for brevity.

Ψ = {ψ α( x) | α( x)) Actc Actm Acts}, where

DAg = {Productsc, POc, POm, MOm, Materialss, MOs}.

Table 2 illustrates only the postcondition of the joint action

α(id, pc, m1, m2) = create PO(id, pc), done MO(m1), accept MO(m2) .

The others are omitted.

In the postcondition in Table 2 variables (from V ) and constants (from U) are distinguished by fonts v and c, respectively. The first two lines impose that the interpretation of the relations Products and Materials, occurring only in the local database of agents c (customer) and s (supplier), respectively, remain unchanged. The third line states that the relation PO of agents c and m (manufacturer) contains a new procurement order, with identifier id and product code pc, both taken from the parameters of action create PO. Observe that, although executed by the customer, this action affects also the local state of the manufacturer. The next 3 lines express that the local PO relation of c and m, in addition to the newly added item, contains also all, and only, the items present before the action execution. The next conjunct (3 lines) states that new identifiers must be unique within each local PO relation. Notice that while this cannot be guaranteed by agent c when executing create PO

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

x.Productsc( x) Productsc ( x) y.Materialss( y) Materialss ( y) b.Productsc(pc, b) POc (id, pc, b, prepared) POm (id, pc, b, prepared) i, pc, b, s.i = id

(POc (i, pc, b, s) POc(i, pc, b, s))

(POm (i, pc, b, s) POc(i, pc, b, s)) i, pc, b, s, pc , b , s .

(POc (i, pc, b, s) POc (i, pc , b , s ) (pc = pc b = b s = s ))

(POm (i, pc, b, s) POm (i, pc , b , s ) (pc = pc b = b s = s )) m1 = m2 m3, pc, p, s.

(MOm(m3, pc, p, s) MOm (m3, pc, p, s))

(MOs(m3, pc, p, s) MOs (m3, pc, p, s)) m1 = m2 pc, p, s.MOm(m1, pc, p, s) (

MOm (m1, pc, p, s) MOm (m1, pc, p, submitted) MOs (m1, pc, p, s) MOs (m1, pc, p, submitted)) pc, p, s.MOs(m2, pc, p, s) ( MOs (m2, pc, p, s) MOs (m2, pc, p, accepted)

MOm (m2, pc, p, s) MOm (m2, pc, p, accepted)) m3, pc, p, s.m1 = m2 m1 = m3

(MOm (m3, pc, p, s) MOm(m3, pc, p, s))

(MOs (m3, pc, p, s) MOm(m3, pc, p, s))

Table 2: The postcondition ψ α(id,pc,m1,m2) for the joint action α(id, pc, m1, m2) = create PO(id, pc), done MO(m1), accept MO(m2)

BELARDINELLI, LOMUSCIO & PATRIZI

(as it cannot access relation PO of m), this value might actually be returned automatically by the system, and then used as input by the agent. The successive 3 lines state that if m1 and m2 coincide, i.e., two distinct operations are to be executed on the same material order m1, then the action has no effect on any local MO relation. On the contrary, as the successive 6 lines state, if m1 = m2 then in the local MO relations of both agent s and m the material order with id m1 changes its state to submitted and the one with id m2 to accepted. Finally, the last 3 lines state that all material orders not involved in the executed (joint) action are propagated unchanged to their respective local relations. Notice that although actions are typically conceived to manipulate artifacts of a specific class, their preconditions and postconditions may depend on artifact instances of different classes. For example, note that the action create MO manipulates MO artifacts, but its precondition depends on PO artifacts. Also, we stress that action executability depends not only on the status attribute of an artifact, but on the actual data content of the whole database, i.e., of all the other artifacts. Similarly, action executions affect not only status attributes. Most importantly, by using first-order formulas such as φb = x1, . . . , xb+1 W i =j(xi = xj) in the postcondition ψ, we can guarantee that the AC program in question is bounded and is therefore amenable to the abstraction methodology of Section 4. We now define the agents induced by the AC program ACPotc given above according to Definition 4.2.

Definition 4.10 Given the AC program ACPotc = Dotc, Uotc, Σotc , the agents Ac, Am and As induced by ACPotc are defined as follows:

Ac = Dc, Actc, Prc , where (i) Dc is as above; (ii) Actc = Ωc = {create PO, submit PO, pay, delete PO}; and (iii) α( u) Prc(lc) iff (lc, σ) |= πα( x)( y) for σ( x) = u.

Am = Dm, Actm, Prm , where (i) Dm is as above; (ii) Actm = Ωm = {create MO, done MO, ship PO, delete MO}; and (iii) α( u) Prm(lm) iff (lm, σ) |= πα( x)( y) for σ( x) = u.

As = Ds, Acts, Prs , where (i) Ds is as above; (ii) Acts = Ωs = {accept MO, reject MO, ship MO}; and (iii) α( u) Prs(ls) iff (ls, σ) |= πα( x)( y) for σ( x) = u.

Note that the agents Ac, Am and As strictly correspond to the agents defined in Def. 2.12. In particular, by the definition of Am above we can see that create MO(id, price) Prm(lm) if and only if the interpretation lm(PO) of the relation PO in the local state lm contains a tuple id, pc, o, prepared for some product pc and offer o; while done MO(mo id) Prm(lm) iff lm(MO) contains a tuple with id mo id and status preparation. As a result, the formal preconditions for create MO and done MO satisfy the intended meaning of these actions. We can now define the AC-MAS generated by the set of agents Ag = {Ac, Am, As} according to Definition 4.3.

Definition 4.11 Given the AC program ACPotc and the set Ag = {Ac, Am, As} of agents induced by ACPotc, the AC-MAS induced by ACPotc is the tuple Potc = Ag, s0 otc, τotc , where:

s0 otc = lc0, lm0, ls0 is the initial global state, where the only non-empty relations are Products and Materials;

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

τotc is the global transition function defined according to Def. 4.3.

The AC-MAS generated by the AC program ACPotc corresponds closely to the AC-MAS appearing in Def. 2.13. As an example we give a snippet of the transition function τotc by considering the global action α( u) = create PO(id, pcode), done MO(m1), accept MO(m2) enabled by the respective protocols in a global state s. By the definition of actions create PO(id, pcode), done MO(m1), and accept MO(m2) we have that li(s) Pri for i {c, m, s} implies that the Products relation contains information about the product pcode. Also, the interpretation of the relation MO contains the tuples m1, p, pr, preparation and m2, p , pr , submitted for some prod-

ucts p and p . By the definition of τotc it follows that for every s Sotc, s α( u) s implies that (DAg D Ag, σ) |= ψα( u)(id, pcode, m1, m2), where DAg and D Ag are obtained from s and s by renaming the relation symbols, α( u) = create PO(id, pcode), done MO(m1), accept MO(m2) , and σ is an interpretation of the formal parameters id, pcode, m1 and m2 in Uotc. In particular, the interpretation of the relation PO in D Ag extends both DAg(POc) and DAg(POm) with the tuple id, pc, b, prepared , where id is a fresh identifier. The tuples for the material orders m1 and m2 are updated in D Ag(MOm) (resp. D Ag(MOs)) and become m1, p, pr, submitted (resp. m2, p , pr , accepted ). In light of the specification of ψα( u) for action α( u), no other element is updated in the transition. Finally, notice that these extensions are indeed the interpretations of PO and MO in s . Thus, the semantics satisfies the intended meaning of the actions. It can also be checked that, in line with the discussion in Section 2.4, a full version of the function τotc given above can easily encode the artifacts lifecycles as given in Figure 2. We now proceed to exploit the methodology of Section 4 to verify the AC program ACPotp. We use the formula ϕmatch from Section 2.4 as an example specification; analogous results can be obtained for the other formulas. Observe that according to Definition 4.3 the AC-MAS induced by ACPotp has infinitely many states. We assume two interpretations for the relations Products and Materials, which determine an initial state D0. Consider the maximum number max of parameters and the constants CΩin the operations in Ωc, Ωm and Ωs. In the case under analysis we have that max = 2. We earlier remarked that formulas such as φb in the postcondition of actions force the AC-MAS Potc corresponding to ACPotc to be bounded. Here we have that Potc is b-bounded. According to Corollary 3.19, we can therefore consider any finite domain U such that

U D0 CΩ con(ϕmatch)

D0(Products) D0(Materials) CΩ

and such that

|U | 2b + |D0| + |CΩ| + |con(ϕmatch)| + max

= 2b + |D0| + |CΩ| + 2

For instance, we can consider any subset U of Uotc satisfying the conditions above. Given that U

satisfies the hypothesis of Theorem 4.7, it follows that the AC program ACPotc over Uotc satisfies ϕmatch if and only if ACPotc over U does. But the AC-MAS induced by the latter is a finite-state system, which can be constructively built by running the AC program ACPotc on the elements in U . Thus, ACPotc |= ϕmatch is a decidable instance of model checking that can be therefore solved by means of standard techniques.

BELARDINELLI, LOMUSCIO & PATRIZI

A manual check on the finite model indeed reveals that ϕmatch, ϕbudget and ϕcost are satisfied in the finite model, whereas ϕfulfil is not. By Corollary 3.19 the AC-MAS Potc induced by ACPotp satisfies the same specifications. Hence, in view of Definition 4.5, we conclude that the artifactcentric program ACPotp satisfies ϕmatch, ϕbudget and ϕcost but does not satisfy ϕfulfil. This is in line with our intuitions of the scenario.

5. Conclusions and Future Work

In this paper we put forward a methodology for verifying agent-based artifact-centric systems. We proposed AC-MAS, a novel semantics incorporating first-order features, that can be used to reason about multi-agent systems in an artifact-centric setting. We observed that the model checking problem for these structures against specifications given in a first-order temporal-epistemic logic is undecidable and proceeded to identify a suitable fragment for which decidability can be retained. Specifically, we showed that the class of bounded, uniform AC-MAS we identified admit finite abstractions that preserve the first-order specification language we introduced. Previous results in the literature, discussed in Subsection 1.2, limit the preservation to fragments of the quantified language and do not allow the interplay between first-order quantifiers and modalities. We explored the complexity of the model checking problem in this context and showed this to be EXPSPACE-complete. While this is obviously a hard problem, we need to consider that these are first-order structures which normally lead to problems with high complexity. We note that the abstract interpretation domain is actually linear in the size of the bound considered. Mindful of the practical needs for verification in artifact-centric systems, we then explored how finite abstractions can actually be built. To this end, rather than investigating one specific datacentric language, we defined a general class of declarative artifact-centric programs. We showed that these systems admit uniform AC-MAS as their semantics. Under the assumption of bounded systems we showed that model checking these multi-agent system programs is decidable and gave a constructive procedure operating on bisimilar, finite models. While the results are general, they can be instantiated for various artifact-centric languages. For instance, Belardinelli et al. (2012b) explore finite abstractions of GSM programs by using these results. We exemplified the methodology put forward on a use case consisting of several agents purchasing and delivering products. While the system has infinitely many states we showed it admits a finite abstraction that can be used to verify a variety of specifications on the system. A question left open in the present paper is whether the uniform condition we provided is tight. While we showed this to be a sufficient condition, we did not explore whether this is necessary for finite abstractions or whether more general properties can be given. In this context it is of interest that artifact-centric programs generate uniform structures. Also, it will be worthwhile to explore whether a notion related to uniformity can be applied to other domains in AI, for example to retain decidability of specific calculi. This would appear to be the case as preliminary studies in the Situation Calculus demonstrate (De Giacomo, Lesp erance, & Patrizi, 2012). On the application side, we are also interested in exploring ways to use the results of this paper to build a model checker for artifact-centric MAS. Previous efforts in this area (Gonzalez, Griesmayer, & Lomuscio, 2012) are limited to finite state systems. It would therefore be of great interest to construct finite abstractions on the fly to check practical e-commerce scenarios such as the one here discussed.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Abiteboul, S., Hull, R., & Vianu, V. (1995). Foundations of Databases. Addison-Wesley.

Alonso, G., Casati, F., Kuno, H. A., & Machiraju, V. (2004). Web Services - Concepts, Architectures and Applications. Data-Centric Systems and Applications. Springer.

Alves, A., Arkin, A., Askary, S., Barreto, C., Ben, Curbera, F., Ford, M., Goland, Y., Gu ızar, A., Kartha, N., Liu, C. K., Khalaf, R., K onig, D., Marin, M., Mehta, V., Thatte, S., van der Rijn, D., Yendluri, P., & Yiu, A. (2007). Web Services Business Process Execution Language Version 2.0. Tech. rep., OASIS Web Services Business Process Execution Language (WSBPEL) TC.

Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., & Montali, M. (2013). Verification of Relational Data-centric Dynamic Systems with External Services. In Hull, R., & Fan, W. (Eds.), Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 13), pp. 163 174. ACM.

Baresi, L., Bianculli, D., Ghezzi, C., Guinea, S., & Spoletini, P. (2007). Validation of Web Service Compositions. IET Software, 1(6), 219 232.

Baukus, K., & van der Meyden, R. (2004). A knowledge based analysis of cache coherence. In Davies, J., Schulte, W., & Barnett, M. (Eds.), Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM 04), Vol. 3308 of Lecture Notes in Computer Science, pp. 99 114. Springer.

Belardinelli, F., & Lomuscio, A. (2012). Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results. Journal of Artificial Intelligence Research, 45, 1 45.

Belardinelli, F., Lomuscio, A., & Patrizi, F. (2011a). A Computationally-Grounded Semantics for Artifact-Centric Systems and Abstraction Results. In Walsh, T. (Ed.), Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 12), pp. 738 743. AAAI.

Belardinelli, F., Lomuscio, A., & Patrizi, F. (2011b). Verification of Deployed Artifact Systems via Data Abstraction. In Kappel, G., Maamar, Z., & Nezhad, H. R. M. (Eds.), Proceedings of the 9th International Conference on Service-Oriented Computing (ICSOC 11), Vol. 7084 of Lecture Notes in Computer Science, pp. 142 156. Springer.

Belardinelli, F., Lomuscio, A., & Patrizi, F. (2012a). An Abstraction Technique for the Verification of Artifact-Centric Systems. In Brewka, G., Eiter, T., & Mc Ilraith, S. A. (Eds.), Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR 12). AAAI.

Belardinelli, F., Lomuscio, A., & Patrizi, F. (2012b). Verification of gsm-based artifact-centric systems through finite abstraction. In Liu, C., Ludwig, H., Toumani, F., & Yu, Q. (Eds.), Proceedings of the 10th International Conference on Service-Oriented Computing (ICSOC 12), Vol. 7636 of Lecture Notes in Computer Science, pp. 17 31. Springer.

Berardi, D., Calvanese, D., De Giacomo, G., Hull, R., & Mecella, M. (2005). Automatic Composition of Transition-based Semantic Web Services with Messaging. In B ohm, K., Jensen, C. S., Haas, L. M., Kersten, M. L., Larson, P.- A., & Ooi, B. C. (Eds.), Proceedings of the 31st International Conference on Very Large Data Bases (VLDB 05), pp. 613 624. ACM.

BELARDINELLI, LOMUSCIO & PATRIZI

Berardi, D., Cheikh, F., Giacomo, G. D., & Patrizi, F. (2008). Automatic Service Composition via Simulation. International Journal of Foundations of Computer Science, 19(2), 429 451.

Bertoli, P., Pistore, M., & Traverso, P. (2010). Automated Composition of Web Services via Planning in Asynchronous Domains. Artificial Intelligence, 174(3-4), 316 361.

Bhattacharya, K., Gerede, C. E., Hull, R., Liu, R., & Su, J. (2007). Towards Formal Analysis of Artifact-Centric Business Process Models. In Alonso, G., Dadam, P., & Rosemann, M. (Eds.), Proceedings of the 5th International Conference on Business Process Management (BPM 07), Vol. 4714 of Lecture Notes in Computer Science, pp. 288 304. Springer.

Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal Logic, Vol. 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.

Calvanese, D., De Giacomo, G., Lenzerini, M., Mecella, M., & Patrizi, F. (2008). Automatic Service Composition and Synthesis: the Roman Model. IEEE Data Engineering Bulletin, 31(3), 18 22.

Ciobaca, S., Delaune, S., & Kremer, S. (2012). Computing Knowledge in Security Protocols Under Convergent Equational Theories. Journal of Automated Reasoning, 48(2), 219 262.

Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. The MIT Press.

Cohn, D., & Hull, R. (2009). Business Artifacts: A Data-Centric Approach to Modeling Business Operations and Processes. IEEE Data Engineering Bulletin, 32(3), 3 9.

Damaggio, E., Deutsch, A., & Vianu, V. (2012). Artifact Systems with Data Dependencies and Arithmetic. ACM Transactions on Database Systems, 37(3), 22:1 22:36.

Damaggio, E., Hull, R., & Vacul ın, R. (2011). On the Equivalence of Incremental and Fixpoint Semantics for Business Artifacts with Guard-Stage-Milestone Lifecycles. In Rinderle-Ma, S., Toumani, F., & Wolf, K. (Eds.), Proceedings of the 9th International Conference on Business Process Management (BPM 11), Vol. 6896 of Lecture Notes in Computer Science, pp. 396 412. Springer.

De Giacomo, G., Lesp erance, Y., & Patrizi, F. (2012). Bounded Situation Calculus Action Theories and Decidable Verification. In Brewka, G., Eiter, T., & Mc Ilraith, S. A. (Eds.), Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR 12). AAAI.

Dechesne, F., & Wang, Y. (2010). To Know or not to Know: Epistemic Approaches to Security Protocol Verification. Synthese, 177(Supplement-1), 51 76.

Deutsch, A., Hull, R., Patrizi, F., & Vianu, V. (2009). Automatic Verification of Data-centric Business Processes. In Fagin, R. (Ed.), Proceedings of the 12th International Conference on Database Theory (ICDT 09), Vol. 361 of ACM International Conference Proceeding Series, pp. 252 267. ACM.

Deutsch, A., Sui, L., & Vianu, V. (2007). Specification and Verification of Data-Driven Web Applications. Journal of Computer and System Sciences, 73(3), 442 474.

Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995). Reasoning About Knowledge. The MIT Press.

VERIFICATION OF AGENT-BASED ARTIFACT SYSTEMS

Gammie, P., & van der Meyden, R. (2004). MCK: Model Checking the Logic of Knowledge. In Alur, R., & Peled, D. (Eds.), Proceedings of 16th International Conference on Computer Aided Verification (CAV 04), Vol. 3114 of Lecture Notes in Computer Science, pp. 479 483. Springer.

Gerede, C. E., & Su, J. (2007). Specification and Verification of Artifact Behaviors in Business Process Models. In Kr amer, B. J., Lin, K.-J., & Narasimhan, P. (Eds.), Proceedings of the 5th International Conference on Service-Oriented Computing (ICSOC 07), Vol. 4749 of Lecture Notes in Computer Science, pp. 181 192. Springer.

Gonzalez, P., Griesmayer, A., & Lomuscio, A. (2012). Verifying GSM-Based Business Artifacts. In Goble, C. A., Chen, P. P., & Zhang, J. (Eds.), Proceedings of the 19th IEEE International Conference on Web Services (ICWS 12), pp. 25 32. IEEE.

Grohe, M. (2001). Generalized Model-Checking Problems for First-Order Logic. In Ferreira, A., & Reichel, H. (Eds.), Proceedings of the 18th Annual Symposium on Theoretical Aspects of Computer Science (STACS 01), Vol. 2010 of Lecture Notes in Computer Science, pp. 12 26. Springer.

Heath, F. T., Boaz, D., Gupta, M., Vacul ın, R., Sun, Y., Hull, R., & Limonad, L. (2013). Barcelona: A Design and Runtime Environment for Declarative Artifact-Centric BPM. In Basu, S., Pautasso, C., Zhang, L., & Fu, X. (Eds.), Proceedings of the 11th International Conference on Service-Oriented Computing (ICSOC 13), Vol. 8274 of Lecture Notes in Computer Science, pp. 705 709. Springer.

Hull, R. (2008). Artifact-Centric Business Process Models: Brief Survey of Research Results and Challenges. In Meersman, R., & Tari, Z. (Eds.), Proceedings (part II) of Confederated International Conferences, Coop IS, DOA, GADA, IS, and ODBASE 2008 (On the Move to Meaningful Internet Systems: OTM 08), Vol. 5332 of Lecture Notes in Computer Science, pp. 1152 1163. Springer.

Hull, R., Damaggio, E., De Masellis, R., Fournier, F., Gupta, M., Heath, III, F. T., Hobson, S., Linehan, M., Maradugu, S., Nigam, A., Sukaviriya, P. N., & Vaculin, R. (2011). Business Artifacts with Guard-Stage-Milestone Lifecycles: Managing Artifact Interactions with Conditions and Events. In Eyers, D. M., Etzion, O., Gal, A., Zdonik, S. B., & Vincent, P. (Eds.), Proceedings of the 5th ACM International Conference on Distributed Event-Based Systems (DEBS 11), pp. 51 62. ACM.

Hull, R., Narendra, N. C., & Nigam, A. (2009). Facilitating Workflow Interoperation Using Artifact Centric Hubs. In Baresi, L., Chi, C.-H., & Suzuki, J. (Eds.), Proceedings of the 7th International Conference on Service-Oriented Computing (ICSOC-Service Wave 09), Vol. 5900 of Lecture Notes in Computer Science, pp. 1 18. Springer.

Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., P olrola, A., Szreter, M., Wozna, B., & Zbrzezny, A. (2008). Ver ICS 2007 - a Model Checker for Knowledge and Real-Time. Fundamenta Informaticae, 85(1-4), 313 328.

Kupferman, O., Vardi, M. Y., & Wolper, P. (2000). An Automata-Theoretic Approach to Branching Time Model Checking. Journal of the ACM, 47(2), 312 360.

Lomuscio, A., Penczek, W., Solanki, M., & Szreter, M. (2011). Runtime Monitoring of Contract Regulated Web Services. Fundamenta Informaticae, 111(3), 339 355.

BELARDINELLI, LOMUSCIO & PATRIZI

Lomuscio, A., Qu, H., & Raimondi, F. (2009). MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In Bouajjani, A., & Maler, O. (Eds.), Proceedings of the 21st International Conference on Computer Aided Verification (CAV 09), Vol. 5643 of Lecture Notes in Computer Science, pp. 682 688. Springer.

Lomuscio, A., Qu, H., & Solanki, M. (2012). Towards Verifying Contract Regulated Service Composition. Autonomous Agents and Multi-Agent Systems, 24(3), 345 373.

Lomuscio, A., & Raimondi, F. (2006). The Complexity of Model Checking Concurrent Programs Against CTLK Specifications. In Baldoni, M., & Endriss, U. (Eds.), Proceedings of the 4th International Workshop on Declarative Agent Languages and Technologies (DALT 06), Selected, Revised and Invited Papers, Vol. 4327 of Lecture Notes in Computer Science, pp. 29 42. Springer.

Marin, M., Hull, R., & Vacul ın, R. (2013). Data Centric BPM and the Emerging Case Management Standard: A Short Survey. In La Rosa, M., & Soffer, P. (Eds.), Proceedings of Business Process Management Workshops - BPM 2012 International Workshops. Revised Papers, Vol. 132 of Lecture Notes in Business Information Processing, pp. 24 30. Springer.

Meyer, J.-J. C., & van der Hoek, W. (1995). Epistemic Logic for AI and Computer Science, Vol. 41 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.

Nigam, A., & Caswell, N. S. (2003). Business Artifacts: An Approach to Operational Specification. IBM Systems Journal, 42(3), 428 445.

Nooijen, E., Fahland, D., & Dongen, B. V. (2013). Automatic Discovery of Data-Centric and Artifact-Centric Processes. In La Rosa, M., & Soffer, P. (Eds.), Proceedings of Business Process Management Workshops - BPM 2012 International Workshops. Revised Papers, Vol. 132 of Lecture Notes in Business Information Processing, pp. 316 327. Springer.

Papadimitriou, C. H. (1994). Computational complexity. Addison-Wesley.

Parikh, R., & Ramanujam, R. (1985). Distributed Processes and the Logic of Knowledge. In Parikh, R. (Ed.), Logic of Programs, Vol. 193 of Lecture Notes in Computer Science, pp. 256 268. Springer.

Singh, M. P., & Huhns, M. N. (2005). Service-Oriented Computing: Semantics, Processes, Agents. John Wiley & Sons.

Wooldridge, M. (2000). Computationally Grounded Theories of Agency. In Proceedings of the 4th International Conference on Multi-Agent Systems (ICMAS 00), pp. 13 22. IEEE.

Wooldridge, M. (2001). Introduction to Multiagent Systems. John Wiley & Sons.