# parameterised_verification_of_dataaware_multiagent_systems__182cfe11.pdf

Parameterised Verification of Data-aware Multi-agent Systems

Francesco Belardinelli Laboratoire IBISC, UEVE IRIT Toulouse, France belardinelli@ibisc.fr

Panagiotis Kouvaros Department of Computing Imperial College London, UK Univ. of Naples Federico II , Italy p.kouvaros@imperial.ac.uk

Alessio Lomuscio Department of Computing Imperial College London, UK a.lomuscio@imperial.ac.uk

We introduce parameterised data-aware multiagent systems, a formalism to reason about the temporal properties of arbitrarily large collections of homogeneous agents, each operating on an infinite data domain. We show that their parameterised verification problem is semi-decidable for classes of interest. This is demonstrated by separately addressing the unboundedness of the number of agents and the data domain. In doing so we reduce the parameterised model checking problem for these systems to that of parameterised verification for interleaved interpreted systems. We illustrate the expressivity of the formal model by modelling English auctions with an unbounded number of bidders on unbounded data.

1 Introduction There has been recent interest in the study of data-aware multi-agent systems (DAMAS) [Montali et al., 2014; Belardinelli et al., 2014; Calvanese et al., 2016]. While standard multi-agent systems (MAS) are modelled by studying the properties of the underlying processes or agents, in DAMAS the emphasis is given equally to the agents and the data driving the executions. This paradigm shift answers a growing demand from applications to support fully the ever increasing amount of data generated by and available to current networked applications [Singh and Huhns, 2005]. A successful paradigm in data-aware systems is that of artifact-centric systems, which have been used to model and execute, among others, data-aware services [De Masellis et al., 2015], hierarchical systems [Deutsch et al., 2016], and case-centric applications [Montali and Calvanese, 2016]. Verifying DAMAS is challenging because of the infinite state models generated by their infinite-domain variables. Approaches based on abstraction have been put forward to solve this problem [Lomuscio and Michaliszyn, 2014; Belardinelli et al., 2014; Montali and Calvanese, 2016], and related techniques have been suggested for similar systems [Bagheri et al., 2013; Gonzalez et al., 2012]. While these investigations have resulted in sound methodologies and open-source toolkits [Gonzalez et al., 2015], a key limitation of DAMAS is that the number of agents in the system is fixed and given at

design-time. This is in marked contrast with the range of applications DAMAS are meant to be employed for (services, case-management, auction-based mechanisms, etc.), which precisely rely on the fact that data-centric structures interact with an unbounded number of actors.

In this contribution we address this issue by introducing parameterised data-aware MAS (or P-DAMAS) as systems with an unbounded number of homogenous agents, each assumed to be data-aware, i.e., endowed with possibly infinite domains and interacting with an environment composed of partially shared data. Specifically, we here tackle the question of verifying P-DAMAS against MAS-oriented specifications. Since the latter involve quantification over data, we combine temporal logic together with first-order features. To deal with the infinity arising from infinite-state variables, we use abstraction techniques based on simulations. To overcome the problems arising from an unbounded number of agents, we develop a parameterised verification technique. The key contribution shows that the verification of particular classes of P-DAMAS that we introduce is partially decidable.

The rest of the paper is organised as follows. In Section 2 we introduce the syntax and semantics of P-DAMAS. In Section 3 we identify a class of P-DAMAS for which we give the semi-decidability result. We illustrate the method in Section 4, where we discuss the verification of auction-based mechanisms. All proofs are omitted for reasons of space.

Related Work. As mentioned above, several proposals have been put forward to verify DAMAS and artifactcentric systems, including [Belardinelli et al., 2012; Lomuscio and Michaliszyn, 2014; Belardinelli et al., 2014; Montali and Calvanese, 2016; Bagheri et al., 2013; Belardinelli and Lomuscio, 2016]. None of these approaches deals with an unbounded number of agents as we do here. Methods for the verification of unbounded MAS have also been developed [Kouvaros and Lomuscio, 2013a; 2016; 2015a; 2015b]; however, these technique do not deal with infinitestate agents. More recently a method for the verification of parameterised MAS, each encoded via infinite-state models, was suggested [Kouvaros and Lomuscio, 2017]. However, the approach targets a non-quantified specification language and does not deal with (semi-)structured data as we do here. As a result, their method differs from the one we present and it is applicable to an uncomparable class of systems.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

2 Parametric Data-aware MAS We introduce parametric data-aware multi-agent systems (PDAMAS) an extension of infinite-state reactive modules [Belardinelli and Lomuscio, 2016], where the number of agents is unbounded. P-DAMAS consist of an agent template, from which an unbounded number of homogeneous (concrete) agents may be constructed, as well as an environment in which the agents operate. The agent template and the environment admit variables with an infinite domain of interpretation, possibly totally ordered (e.g., natural numbers). The specifications for these systems will be given in a parametric first-order extension of the branching-time temporal logic CTL [Clarke et al., 1999]. Agent templates. In the following we assume an ordered interpretation domain D, a set var tv0, v1, . . .u of variables and a set par tx0, x1, . . .u of parameters interpreted on D. Variables are used to describe the data model, while parameters appear in formulas. Further, we introduce an agent template t (or simply template) as well as the environment e. In line with reactive systems [Alur and Henzinger, 1999], we assume that each i P tt, eu controls a finite set cnti Ď var of variables. Specifically, tcnte, cnttu forms a partition of var. Hence, the set var can be assumed to be finite. The set obst of variables that are observable by agent template t includes all of her controlled variables as well as the variables controlled by the environment: obst cntt Y cnte. In line with the formal account of agents in the literature on interpreted systems [Fagin et al., 1995], we suppose each i P tt, eu has a set L of local states, a set Act of actions, and a protocol function P. In particular, to introduce a formal account of local state, we consider local interpretations as functions θi : cnti Ñ D, i.e., (finite) assignments from the variables in cnti to values in D. For simplicity, we often identify an interpretation θi with its range θipcntiq Ď D, whenever domain cnti is clear by the context. Then, a local state l P L of agent template t includes all values of its observed variables in obst, i.e., l θt Yθe. Since the domain D is infinite in general, the set L of local states is also infinite. To define the individual actions in Act and the protocol P, we introduce a first-order language built on variables, parameters and relation symbols and ď. Definition 1 (FO-formulas). First-order formulas are defined according to the following BNF, where z, z1 P var Y par and x P par: φ :: z z1 | z ď z1 | φ | φ Ñ φ | @xφ The symbols , ă, ě, J, K, connectives , _, quantifier D, and free and bound variables and parameters are defined as standard [Hamilton, 1978]. Notice that quantification applies to parameters only, this is in accordance with the intuition above on the use of variables and parameters. Definition 2 (Guarded Command). A guarded command γ over var and par is an expression id gpx1, . . . , xkq ; v1 : x1; . . . ; vk : xk where (i) id is the command s identity; (ii) guard g is an FOformula with free parameters among x1, . . . , xk. The intuitive meaning of a guarded command is that if guard g is true for some interpretation σ : par Ñ D of parameters, then the command γ is enabled for execution. By

executing γ we set each variable vi to value σpxiq P D. In particular, the skip command can be represented as J ; ϵ, where ϵ is the empty sequence. We say that v1, . . . , vk are the variables controlled by γ, and denote this set by ctrpγq, while the variables in g are the observable variables obspγq [Hoek et al., 2006]. Following the typical setting in parameterised formalisms for MAS [Kouvaros and Lomuscio, 2013b; 2016], we assume that each command can either be an asynchronous command, an agent-environment command, or a global-synchronous command. Each type of command enables a different communication pattern between the concrete agents instantiated from the templates. Specifically, asynchronous commands enable the asynchronous evolution of an agent; agentenvironment commands enable pairwise synchronisation between one agent and the environment; global-synchronous commands enable full synchronisation among all the agents and the environment. To introduce the semantics of guarded commands formally, we define the satisfaction |ù of FO-formulas. An FO-formula φ is given meaning by a finite interpretation σ : frpφq Ñ D that assigns values in D to the free parameters in φ. A reinterpretation σx u coincides with σ, but assigns value u P D to parameter x P frpφq. Given z P var Ypar, pθ, σqpzq θpzq for z P var, and pθ, σqpzq σpzq for z P par.

Definition 3 (Satisfaction). The satisfaction of an FOformula φ for a finite interpretation σ and local interpretation θ, denoted pθ, σq |ù φ, is defined as follows (clauses for propositional connectives are immediate and thus omitted):

pθ, σq |ù z z1 iff pθ, σqpzq pθ, σqpz1q pθ, σq |ù z ď z1 iff pθ, σqpzq ď pθ, σqpz1q pθ, σq |ù @xφ iff for all u P θpvarq, σx u |ù φ

The interpretation of FO-formulas is completely standard, but for quantification that takes values from the finite image θpvarq tu P D | u θpvq for some v P varu of var. This is consistent with the interpretation of quantification on active domains in database theory [Abiteboul et al., 1995]. Indeed, at this stage quantification can be considered syntactic sugar, as θpvarq is finite.

Definition 4 (Agent template). The agent template is a tuple t x L, init, Act, P, τy where L tθt Y θe | θi : ctri Ñ D for i P tt, euu, where ctrt and ctre are the (finite) set of variables owned by t, e; init ιt Y ιe, where ιt : ctrt Ñ D and ιe : ctre Ñ D provide the initial interpretations of ctrt and ctre; Act is a (infinite) set of pairs α pγ, σq of guarded commands γ, together with finite interpretations σ, s.t. for every γ, ctrpγq Ď ctrt and obspγq Ď obst; P : L Ñ p Actqzt Hu is such that, for every l P L, Pplq tα P Act | pl, σαq |ù γαu; τ : L ˆ Act ˆ Acte Ñ L is such that (i) τpl, α, αeq is defined only if α P Pplq; and (ii) τpl, α, αeq l1 iff for every variable vi P cntpγαq and wi P cntpγαeq, θ1pviq σαpxiq and θ1 epwiq σαepyiq; while all other variables do not change value.

The environment is similarly defined. Observe, however, that its set of local states is defined only on θe and its tran-

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

sition function is defined only on its current state le and action αe. The actions of the agent template are partitioned as Act A Y AE Y GS, where A is a set of asynchronous actions, AE is a set of agent-environment actions, and GS is a set of global-synchronous actions. Concretely, the agents synchronise on actions with the same identity. Given a set X of actions, let idp Xq tidγ | pγ, σq P Xu be the set of the commands identities in X. Following the agent-environment and global-synchronous synchronisation patterns we assume that idp AE eq idp AE tq and idp GS tq idp GS eq. Finally, a parametric data-aware multi-agent system is a pair of an agent template and an environment.

Definition 5 (P-DAMAS). A parametric data-aware multiagent system (P-DAMAS) is a pair M xt, ey, where t is the agent template and e is the environment.

P-DAMAS provide a description of an unbounded collection of (concrete) data-aware multi-agent systems (DAMAS). Concrete Agents. Concrete DAMAS are obtained by setting the parameters to the actual number of agents in the system. That is, given a P-DAMAS M and n P N, the DAMAS Mpnq of n agents per template t is the composition of n copies of t with the environment. We write Agpnq ttj | 1 ď j ď nu for the set of all concrete agents tj x Lj, Actj, initj, Pj, τjy. The concrete agent inherits from the template her actions, her protocol, and her transition function. However, these are defined on variables that are indexed by the agent s identity. Specifically, we consider the set varpnq tv ˆ t1, . . . , nu | v P ctrtu Y ctre of variables, where agent tj controls the variables in ctrj tvj P varpnq | v P ctrtu and observes the variables in obsj ctrj Y ctre. This is consistent with the requirement that tctr1, . . . , ctrn, ctreu form a partition of varpnq.

Definition 6 (Concrete agent). Given the agent template t x L, init, Act, P, τy, the j-th concrete agent instantiated from t is a tuple tj x Lj, initj, Actj, Pj, τjy, where Lj tθj Y θe | θi : ctri Ñ D for i P tj, euu; initj ιj Y ιe, where ιj : ctrj Ñ D is such that ιjpvjq x iff ιtpvq x; Actj tpγ1, σq | pγ, σq P Acttu, where γ1 is obtained from γ by replacing every variable v P ctrpγq by vj; The protocol Pj and the transition function τj are defined as in Def. 4.

Def. 6 above provides the concrete counterpart to the notion of agent template introduced in Def. 4. Further, a global state in DAMAS Mpnq is a tuple s xθ1, . . . , θn, θey, where each θj : cntj Ñ D is an interpretation for the j-th instantiation of template t. Equivalently, global states can be represented as functions s : varpnq Ñ D, i.e., finite interpretations of the variables in varpnq with values in D such that for every vj P varpnq, spvq θjpvq. As anticipated above, any state s is well-defined as varpnq is partitioned among the agents in Agpnq. Further, given a global state s, we denote as l1, . . . , ln, le the corresponding local states for all agents in Agpnq Y teu. Observe that xθ1, . . . , θn, θey and xl1, . . . , ln, ley are equivalent representations of global state s, in terms of controlled, respectively observable, variables. So, we will use the two notations interchangeably. We

stress that concrete agents have only partial observability of the global state of the system. Let ACT ś ag PAgpnq Yteu Actag be the set of joint actions. For a P ACT, consider a.ag to represent the action of agent ag. The concrete system evolves over time in compliance with the agents protocols and evolution functions. This is described by the global transition function.

Definition 7 (Global transition function). The global transition function τ : G ˆ ACT Ñ G is defined as follows: τps, αq s1 iff for every ag P Agpnq, l1 ag τagplag, α.ag, α.eq, l1 e τeple, α.eq, and one of the following holds: (Asynchronous): for some ag P Agpnq, (i) α.ag is asynchronous; and (ii) for every ag1 ag, α.ag1 skip. (Agent-environment): for some ag P Agpnq, (i) α.ag is an agent-environment action; (ii) idα.e idα.ag; and (iii) for every ag1 ag, ag1 e, α.ag1 skip. (Global-synchronous): for every ag, ag1 P Agpnq Y teu, (i) α.ag is a global-synchronous action; and (ii) idα.ag idα.ag1.

Above τ defines only one action to be performed at each time step. If this is an asynchronous action, then exactly one concrete agent participates in the global transition; if it is an agent-environment action, then exactly one concrete agent and the environment participate in the transition; if it is a global-synchronous action, then all concrete agents and the environment participate in the transition. The agents not participating in the transition are assumed to perform the skip action. Moreover, by the definition of each τag, we have that for every ag P Agpnq Y teu, a.ag P Pagpsagq. We can now define the concrete systems generated from a P-DAMAS M.

Definition 8 (DAMAS). The data-aware MAS (DAMAS) Mpnq of n agents is a tuple Mpnq x S, init, τy, where: init ś ag PAgpnq Yteu initag; τ is the global transition function (Definition 7); S is the closure of init according to τ.

Clearly, a P-DAMAS generates different DAMAS depending on the number n of agents in the system. Overall, a concrete DAMAS Mpnq describes the evolution of a multi-agent system from the initial state init, according to the transition function τ. Again, since the domain D is infinite in general, every generated DAMAS is an infinite-state system. The Specification Language. To reason about an unbounded number of agents, we here define an indexed, firstorder extension of the temporal logic ECTLz X (the existential fragment of CTL without next X), where the atomic propositions are indexed by agent parameters. These are agent-specific parameters whose domain depends on the concrete system on which the specification is evaluated: if it is evaluated on Mpnq, then the potential set of values is t1, . . . , nu. For agent template t consider a set apar of agent parameters. Intuitively, indexed formulas quantify universally over the concrete agents.

Definition 9 (Indexed FO-formulas and FO-ECTLz X). Indexed first-order formulas over agent parameters apar are defined according to the following BNF, where z pv, aq

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

(resp. z1 pv1, a1q), for v, v1 P ctr, a, a1 P apar, and x P par: φ :: z z1 | z ď z1 | φ | φ Ñ φ | @xφ Formulas in first-order ECTLz X are defined as follows, where φ is an indexed FO-formula:

ψ :: φ | φ | ψ ψ | ψ _ ψ | @xψ | EpψUψq | EpψRψq | @agaψ

Note that we use @ag to indicate that the operator quantifies over agent parameters. The temporal modality EpφUψq stands for for some path, φ holds until ψ holds ; and EpφRψq denotes for some path, φ releases ψ . We say that an FO-ECTLz X sentence is m-indexed, for m P N, if there are precisely m agent parameters from apar appearing in the formula. Notice that in FO-ECTLz X we can have arbitrary alternations of quantifiers and ECTLz X operators. A consequence of this is that quantification in FO-ECTLz X is not syntactic sugar. We now define the satisfaction relation. In the definition we assume that the sets of parameters appearing in the commands and the formula are disjoint. This can be done without loss of generality, as both sets are finite and defined at design-time. Hereafter a path is an infinite sequence π s1α1s2α2s3 . . . with τpsi, αiq si 1, for every i ě 1. Given a path π, we write πpiq for the i-th state in π. The set of all paths originating from a state s is denoted by Pathpsq. Definition 10 (Satisfaction). The satisfaction relation |ù for a DAMAS Mpnq, a global state s, an FO-ECTLz X formula ψ, and an interpretation σ is defined as follows (clauses for propositional connectives are immediate and thus omitted).

p Mpnq, s, σq |ù φ iff ps, σq |ù φ, where φ is an FO-formula p Mpnq, s, σq |ù @xψ iff for all u P spvarpnqq, p M, s, σx uq |ù ψ p Mpnq, s, σq |ù EpψUψ1q iff for some π P Pathpsq, for some i ě 0, p Mpnq, πpiq, σq |ù ψ1 and for all j ă i, p Mpnq, πpjq, σq |ù ψ p Mpnq, s, σq |ù EpψRψ1q iff for some π P Pathpsq, either for some i ě 0, p Mpnq, πpiq, σq |ù ψ and for all j ď i p Mpnq, πpjq, σq |ù ψ1, or for all i ě 0 p Mpnq, πpiq, σq |ù ψ1

p Mpnq, s, σq |ù @agyψ iff ag P t1, . . . , nu implies p Mpnq, s1, σq |ù ψry ÞÑ ags, for ag P apar We remark that the semantics of ECTLz X operators in Def. 10 is standard, while quantification over regular parameters ranges on the active domain spvarpnqq. However, differently from Def. 3, quantification is not syntactic sugar: transitions might take us to a successor state s1, in which an individual u P spvarpnqq is no longer active, i.e., u R s1pvarpnqq. As a result, quantification in FO-ECTLz X gives us a language that is strictly more expressive than propositional ECTLz X. An FO-ECTLz X formula ψ is true in state s, or p Mpnq, sq |ù ψ, iff for all interpretations σ, p Mpnq, s, σq |ù ψ; ψ is true in Mpnq, or Mpnq |ù ψ, iff p Mpnq, initq |ù ψ. In light of decidability limitations (see [Bloem et al., 2015] for a detailed discussion), hereafter we consider prenex mindexed FO-ECTLz X formulas in which the universal quantifiers on apar appear only at the front of the formula. We can now state the parameterised model checking problem for the present setting. Definition 11 (PMCP for P-DAMAS). Given a P-DAMAS M and an m-indexed FO-ECTLz X formula ψ, the parameterised model checking problem consists in determining whether for all n ě m, Mpnq |ù ψ.

Parameterised model checking involves checking an unbounded number of systems. Since P-DAMAS extend broadcast protocols whose PMCP is undecidable [Esparza et al., 1999], the PMCP the P-DAMAS is also undecidable. general [Apt and Kozen, 1986]. Moreover, notice that each concrete system is an infinite-state system, and again the model checking problem for infinite-state systems is normally undecidable [Deutsch et al., 2009]. However, in what follows we define a cutoff technique to bound the number of agents to check, thereby obtaining partial decidability.

3 Partial Decidability via Abstractions

In this section we develop a partial model checking procedure for FO-ECTLz X. Specifically, the partial decidability of the parameterised verification problem is given in two steps. In the first step, the domain D of the P-DAMAS to be verified is abstracted into a finite domain DA. It is shown that every concrete system generated from the abstract P-DAMAS defined on DA is simulated by the equally populated concrete system obtained from the original P-DAMAS built on D. As a result, the PMCP is reduced to checking an unbounded number of finite-state systems. In the second step, a mapping is defined from (abstract) finite state P-DAMAS to parameterised interleaved interpreted systems (PIIS) [Kouvaros and Lomuscio, 2016]. Consequently, we can apply the results in [Kouvaros and Lomuscio, 2016] to solve the PMCP. Finite Simulations. First of all, notice that Def. 4 of agent template depends on the interpretation domain D as well. That is, by varying D we can obtain P-DAMAS defined on the same partition of variables, but with different interpretations. In particular, if DA Ď D is finite, then the corresponding P-DAMAS is finite as well, and while we can still have an unbounded number of agents in the concrete DAMAS, each DAMAS itself is a finite-state system. Hereafter we prove that, whenever DA Ď D, for every n P N, the concrete, possibly finite DAMAS M Apnq built on DA is a submodel of the concrete, infinite-state DAMAS Mpnq defined on D. In particular, the former is simulated by the latter. As a consequence, existential formulas in FO-ECTLz X are preserved from M Apnq to Mpnq.

Definition 12 (Abstract Template and Abstract P-DAMAS). Let i P tt, eu be an agent template (resp. the environment) whose controlled variables in cnti take values in domain D, and let DA Ď D. Then the abstraction i A is obtained by restricting the range of variables in cnti to DA. Further, given P-DAMAS MA xt, ey, the abstract PDAMAS M xt A, e Ay is the collection of abstractions t A and e A built on DA.

Given n P N, the DAMAS M Apnq for n agents per abstract template t A is defined as the composition of n copies of t A with the abstract environment e A, in analogy with Def. 6 and 7. In particular, observe that if s is a state in DAMAS M Apnq, then s also belongs to the concrete Mpnq. Hence, M Apnq is a submodel of Mpnq. In particular, Mpnq simulates M Apnq. To prove this fact we state some partial results.

Lemma 1. For every states s, s1 in M Apnq and joint action α P ACT, if s αÝÑ s1 in M Apnq, then s αÝÑ s1 in Mpnq.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

By Lemma 1 all transitions in M Apnq are simulated in Mpnq. This result can be extended to whole paths.

Lemma 2. Every path π from s in M Apnq is also a path (from s) in Mpnq.

By Lemma 2 we can prove the main preservation result of this section.

Theorem 3. Let Mpnq be a DAMAS with abstraction M Apnq defined on DA Ď D. For every states s in M Apnq and formula φ in FO-ECTLz X, if M Apnq |ù φ, then Mpnq |ù φ.

In particular, by Theorem 3 existential formulas are preserved by taking DAMAS defined on a finite domain DA Ď D. However, in principle we have an infinite number of such finite DAMAS Mpnq, one for every choice of agent parameter n. We tackle this issue in the following section. PIIS simulations. We reduce the PMCP for finite-state P-DAMAS to the PMCP for PIIS. That is, we show that for every abstract P-DAMAS MA we can associate a PIIS MPA whose concrete systems satisfy the same FO-ECTLz X formulas as the equally populated concrete systems from MA. Recall that PIIS are defined as finite-state P-DAMAS, but with the following differences: (i) the variables controlled by the environment are private to the environment, i.e., obst cntt; (ii) the agent template s transition function does not depend on the action of the environment, i.e., τ : LˆAct Ñ L. Accounting for these differences we now define MPA. We begin with the definition of the notions of guarded command products and AE-synchronisation commands. Intuitively, the commands enable the PIIS agents to simulate the updates of the observable components of the DAMAS agents states.

Definition 13 (Guarded command products). The product of two guarded commands id gpx1, . . . , xkq ; v1 : x1; . . . ; vk : xk and id g1px1 1, . . . , x1 k1q ; v1 1 : x1 1; . . . ; v1 k1 : x1 k1 is defined as the guarded command id gpx1, . . . , xkq g1px1 1, . . . , x1 k1q ; v1 : x1; . . . ; vk : xk; v1 1 : x1 1; . . . ; v1 k1 : x1 k1.

The product of an agent s command and the environment s command enables a PIIS agent to explicitly update the environment s variables encoded in the agent s state. Given actions a pγ, σq, a1 pγ1, σ1q, we write a ˆ a1 pγ ˆ γ1, σ Y σ1q for their product.

Definition 14 (AE synchronisation commands). Let γ be an agent-environment command id gpx1, . . . , xkq ; v1 : x1; . . . ; vk : xk. The AE initiator command of γ, γr?s, is the agent-environment command idr?s gpx1, . . . , xkq ae sync K ; ae sync J. The AE broadcast command γr!s of γ is the global-synchronous command idr!s gpx1, . . . , xkq ae sync J ; v1 : x1; . . . ; vk : xk; ae sync K.

AE-synchronisation commands enable the PIIS agents to simulate the agent-environment transitions of the DAMAS agents. In particular the AE initiator command γr?s is performed by the agent participating in the agent-environment transition. The command marks said agent and signals the execution of the global-synchronous command γr!s by setting the (fresh) boolean variable ae sync to J. With the global

synchronisation the agent updates both controlled and observable variables, whereas all other agents update only the observable variables (see item (ii) of Lemma 4). We now define the PIIS MPA associated with MA. Definition 15 (Associated PIIS). The PIIS MPA @ t PA, e PAD associated with P-DAMAS MA @ t A, e AD over domain DA Y tae syncu is obtained from t A, e A by defining the following sets of actions for t PA and e PA: Actt PA: A is the set of asynchronous actions; tar?s | a P AEtu is the set of agent-environment actions; and AE e Y tar!s ˆ aer!s | a P AE t, ae P AE e, ida idaeu Y ta ˆ ae | a P GS t, ae P GS e, ida idaeu is the set of global-synchronous actions. Acte PA: tar?s | a P AE eu is the set of agentenvironment actions and GS e Y tar!s | a P GS eu is the set of global-synchronous actions. Above we assume that ae sync is initially set to K. Also, every action of t PA that is not a broadcast action is guarded by the additional requirement that ae sync is set to K. The following definition relates the states of each concrete system M Apnq to the states of the concrete system M PApnq. Definition 16 (Related states). A global state s of M Apnq and a global state q of M PApnq are related, or s q, iff (i) for all v P avarpnq, spvq qpvq; and (ii) for all ag P t1, . . . , n, eu, sppae syncq, agq qppae syncq, agq K. Following the above definition we show that related states satisfy the same FO-ECTLz X formulas. Since the initial states of corresponding concrete systems are related, the systems satisfy the same FO-ECTLz X formulas. To show this we first state some intermediate results. Lemma 4. Let s be a state of M Apnq and q a state of M PApnq. If s q, then the following hold: (i) If s α s1, then q α q1 and s1 q1. (ii) If s α s1 is an agent-environment transition fired by agent i, then q α1 q1 α2 q2 and s1 q2, where α1 is defined by α1.j skip for j i e, α1.i α.ir?s, and α1.e α.er?s; α2 is defined by α2.j α.e for all j i e, α2.i α.ir!s ˆ α.er!s, α2.e α.er!s. (iii) If s α s1 is a global synchronous transition, then q α1 q1 and s1 q1, where α1 is defined by α1.i α.i ˆ α.e for i e, and α1.e α.e. By Lemma 4 the transitions in M Apnq are simulated in M PApnq 1. Additionally, it is easy to see that transitions in M PApnq are simulated in M Apnq. We thus obtain the following preservation result. Theorem 5. Let M be a P-DAMAS with abstraction MA. Let MPApnq be the PIIS associated with MA. Then, for every formula φ in FO-ECTLz X, M Apnq |ù φ iff M PApnq |ù φ. As a consequence, the PMCP for P-DAMAS can be solved by solving the PMCP for PIIS. Given an m-indexed formula, the latter problem can be solved by checking the concrete system with maxp2, mq agents [Kouvaros and Lomuscio, 2013b]. The result is derived under the assumption that

1Note that since our specification logic does not include the nexttime operator, a transition in M Apnq can be simulated by more than one transition in M PApnq [Kouvaros and Lomuscio, 2016].

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

the environment is non-blocking. That is, whenever an agentenvironment action, or a global synchronous action is enabled for a concrete agent, then the action is also enabled for the environment. We write NB for the class of PIIS with nonblocking environments. We then obtain the following. Theorem 6. Let M be a P-DAMAS with abstraction MA such that MA P NB. Then, for every m-indexed formulae φ in FO-ECTLz X, M Apmq |ù φ implies @n ě maxp2, mq, Mpnq |ù φ. The above is the main result of the paper; it outlines a partial procedure to solve the PMCP for P-DAMAS and FOECTLz X. This takes as input a P-DAMAS M and an mindexed FO-ECTLz X formula φ and constructs the abstract P-DAMAS MA as per Definition 12. If the PIIS associated with MA is non-blocking 2, then the abstract DAMAS with up to maxp2, mq agents are checked against the formula. If these satisfy φ, then we can conclude that the PMCP is true for M and φ; otherwise no conclusions can be drawn.

4 Auctions as AES P-DAMAS To illustrate the formal machinery and the result in Section 2 and 3, we introduce agent templates for simple English (ascending bid) auctions. We refer to [Easley and Kleinberg, 2010] for a detailed presentation of this type of auctions. First of all, we model the auctioneer and bidders taking part in the auction as the environment and the agent template. Definition 17 (Auctioneer). The auctioneer a x La, inita, Acta, Pa, τay is such that La is the set of local states defined on set ctra tbase, t out, highu of variables, where t out is boolean, while base and high range over the rational numbers Q extended with the undefined value uu. inita ιa : ctra Ñ D, where ιapbaseq uu, ιapt outq J, and ιaphighq uu. Acta contains guarded commands skip and

id1 t out K ; t out : J id2 t out J ; base : x2; t out : K id3 J ; high : x4 with id1 P GSa, id2 P Aa, and id3 P AEa. Pa and τa are given as in Def. 4. Intuitively, the auctioneer keeps track of the base price base as well as the highest bid high for the auctioned item, and owns a boolean variable t out to terminate nondeterministically the bidding round. At the start of the bidding process the auctioneer initialises base to a random rational x2 and t out to false (K). Then, she updates the highest bid high and possibly terminate the bidding round. A new round can then be started. Further, the template for bidders is given as follows. Definition 18 (Bidder). The bidder template tb x Lb, initb, Actb, Pb, τby is such that ctrb ttvalue, bidu, with both tvalue and bid ranging over Q Y tuuu.

2This test can be performed in polynomial time in the size of the agent template and the environment [Kouvaros and Lomuscio, 2013b].

initb ιb : ctrb Ñ D, where ιbpbidq uu and ιbptvalueq uu. Actb contains guarded commands skip and id1 J ; tvalue : uu; bid uu id1 2 pt out Kq ptvalue uuq ; tvalue : x6 id3 pt out Kq ptvalue uuq px4 ď tvalueq phigh uu Ñ high ă x4q pbid uu Ñ bid ă highq ; bid : x4x with id1 P GSb, id1 2 P Ab, and id3 P AEb Pb and τb are given as in Def. 4. By Def. 18 every bidder template b has a true value tvalue, up to which she is happy to bid, as well as current bid. At the beginning she initialises tvalue, while bid is set to undefined . Thereafter, she might choose to bid and then update bid according to the other bidders offers. At the end of the bidding round, she reinitialises her true value for a new round. Given the auctioneer and the bidder template as defined above, a P-DAMAS for an English auction is the pair M xa, tby for the auctioneer a and bidders b. Since base prices, true values, and bids all take rationals as values, M is actually an infinite-state system. On the P-DAMAS M we might want to verify properties such as every agent will eventually win in some execution: φA1 fi@aga: EFpwin, aq, where winpaiq :: ppbid, aiq highq. Moreover, we can express that in at least one execution, every agent bids up to her true value: φA2 fi@aga: EFppbid, aq pt value, aqq. To verify φA1 and φA2 on M, we first model check abstraction MA and, if the answer is positive, by Theorems 3 and 6 the result transfers to M. Notice that this defines a partial verification procedure. If the answer is negative, a possible different abstraction M 1A needs to be considered.

5 Conclusions As argued in the introduction, while data-aware systems have rapidly become common in applications, there is still a lack of techniques capable of providing formal guarantees for systems of agents interacting with these. The difficulty of doing this results both from the possibly infinite amount of data and the unbounded number of agents interacting with it. In this contribution we addressed these problems and put forward P-DAMAS, a formal model for such systems, then presented a technique for their verification. The key result here is that for the relevant class of P-DAMAS verification is semi-decidable. It should be noted that partial decidability is a common feature in abstraction methodologies, which can normally decide on the truth of a specification in some cases only. Indeed, partial decidability can be useful in several applications of importance, as we showed here in analysing the auction scenario. In future work we plan to extend the present results to yet more expressive languages, including epistemic and strategy logics.

Acknowledgments The research described in this paper was partly supported by the EPSRC project Trusted Autonomous Systems (EP/I00529X) and the French ANR JCJC Project SVe Da S (ANR-16-CE40-0021).

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

References [Abiteboul et al., 1995] S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. [Alur and Henzinger, 1999] R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7 48, 1999. [Apt and Kozen, 1986] K.R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307 309, 1986. [Bagheri et al., 2013] B. Bagheri, D. Calvanese, M. Montali, G. Giacomo, and A. Deutsch. Verification of relational data-centric dynamic systems with external services. In Proceedings of PODS13, pages 163 174. ACM, 2013. [Belardinelli and Lomuscio, 2016] F. Belardinelli and A. Lomuscio. Abstraction-based verification of infinitestate reactive modules. In Proceedings of ECAI16, pages 725 733, 2016. [Belardinelli et al., 2012] F. Belardinelli, A. Lomuscio, and F. Patrizi. An abstraction technique for the verification of artifact-centric systems. In Proceedings of KR12, pages 319 328, 2012. [Belardinelli et al., 2014] F. Belardinelli, A. Lomuscio, and F. Patrizi. Verification of agent-based artifact systems. Journal of Artificial Intelligence Research, 51:333 376, 2014. [Bloem et al., 2015] R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. Decidability of Parameterized Verification. Morgan and Claypool Publishers, 2015. [Calvanese et al., 2016] D. Calvanese, M. Montali, F. Patrizi, and M. Stawowy. Plan synthesis for knowledge and action bases. In Proceedings of IJCAI16, pages 1022 1029, 2016. [Clarke et al., 1999] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. [De Masellis et al., 2015] R. De Masellis, D. Lembo, M. Montali, and D. Solomakhin. Semantic enrichment of gsm-based artifact-centric models. J. Data Semantics, 4(1):3 27, 2015. [Deutsch et al., 2009] A. Deutsch, R. Hull, F. Patrizi, and V. Vianu. Automatic verification of data-centric business processes. In Proceedings of ICDT09, pages 252 267. ACM, 2009. [Deutsch et al., 2016] A. Deutsch, Y. Li, and V. Vianu. Verification of hierarchical artifact systems. In Proceedings of PODS16, pages 179 194, 2016. [Easley and Kleinberg, 2010] D. Easley and J. Kleinberg. Networks, Crowds, and Markets: Reasoning About a Highly Connected World. Cambridge University Press, New York, NY, USA, 2010. [Esparza et al., 1999] J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proceedings of LICS99, pages 352 359. IEEE, 1999.

[Fagin et al., 1995] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995. [Gonzalez et al., 2012] P. Gonzalez, A. Griesmayer, and A. Lomuscio. Verifying GSM-based business artifacts. In Proceedings of ICWS12, pages 25 32. IEEE Press, 2012. [Gonzalez et al., 2015] P. Gonzalez, A. Griesmayer, and A. Lomuscio. Verification of GSM-based artifact-centric systems by predicate abstraction. In Proceedings of ICSOC15, volume 9435 of LNCS, pages 253 268. Springer, 2015. [Hamilton, 1978] A. G. Hamilton. Logic for Mathematicians. Cambridge University Press, 1978. [Hoek et al., 2006] W. van der Hoek, A. Lomuscio, and M. Wooldridge. On the complexity of practical ATL model checking. In Proceedings of AAMAS06, pages 201 208, 2006. [Kouvaros and Lomuscio, 2013a] P. Kouvaros and A. Lomuscio. Automatic verification of parametrised interleaved multi-agent systems. In Proceedings of AAMAS13, pages 861 868. IFAAMAS, 2013. [Kouvaros and Lomuscio, 2013b] P. Kouvaros and A. Lomuscio. A cutoff technique for the verification of parameterised interpreted systems with parameterised environments. In Proceedings of IJCAI13, pages 2013 2019. AAAI Press, 2013. [Kouvaros and Lomuscio, 2015a] P. Kouvaros and A. Lomuscio. A counter abstraction technique for the verification of robot swarms. In Proceedings of AAAI15, pages 2081 2088. AAAI Press, 2015. [Kouvaros and Lomuscio, 2015b] P. Kouvaros and A. Lomuscio. Verifying emergent properties of swarms. In Proceedings of IJCAI15, pages 1083 1089. AAAI Press, 2015. [Kouvaros and Lomuscio, 2016] P. Kouvaros and A. Lomuscio. Parameterised verification for multi-agent systems. Artificial Intelligence, 234:152 189, 2016. [Kouvaros and Lomuscio, 2017] P. Kouvaros and A. Lomuscio. Parameterised verification of infinite state multiagent systems via predicate abstraction. In Proceedings of AAAI17, pages 3013 3020. AAAI Press, 2017. [Lomuscio and Michaliszyn, 2014] A. Lomuscio and J. Michaliszyn. Model checking unbounded artifactcentric systems. In Proceedings of KR14, pages 488 497. AAAI Press, 2014. [Montali and Calvanese, 2016] M. Montali and D. Calvanese. Soundness of data-aware, case-centric processes. STTT, 18(5):535 558, 2016. [Montali et al., 2014] M. Montali, D. Calvanese, and G. De Giacomo. Verification of data-aware commitment-based multiagent system. In Proceedings of AAMAS14, pages 157 164. IFAAMAS, 2014. [Singh and Huhns, 2005] M. Singh and M. Huhns. Service Oriented Computing: Semantics, Processes, Agents. Wiley, 2005.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)