Parameterised Verification of Data-aware Multi-Agent Systems

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

Alessio Lomuscio

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

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.

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 � θtYθ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

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 varYpar, 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):

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 � xL, 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 � ℘pActqztHu 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γαe q, θ1 pviq � σαpxiq and θ1e pwiq � σαe pyiq; 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 transition 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 idpXq � 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 idpAEeq � idpAEt q and idpGSt q � idpGSeq.

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 � xLj,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 � xL, init, Act, P, τy, the j-th concrete agent instantiated from t is a tuple tj � xLj , 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 � -agPAgpnqYteu 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, l1ag � τagplag, α.ag, α.eq, l1e � τ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 � xS, init, τy, where: init � -agPAgpnqYteu 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 ECTLzX (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-ECTLzX). Indexed first-order formulas over agent parameters apar are defined according to the following BNF, where z � pv, aq

(resp. z1 � pv1 , a1 q), for v, v1 P ctr, a, a1 P apar, and x P par: φ ::� z � z1 | z / z1 | φ | φ�φ | @xφ

Formulas in first-order ECTLzX are defined as follows, where φ is an indexed FO-formula:

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-ECTLzX 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-ECTLzX we can have arbitrary alternations of quantifiers and ECTLzX operators. A consequence of this is that quantification in FO-ECTLzX 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α1 s2α2 s3 . . . with τpsi , αi q � 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-ECTLzX formula ψ, and an interpretation σ is defined as follows (clauses for propositional connectives are immediate and thus omitted).

• pMpnq, s, σq |ø φ

iff ps, σq |ø φ, where φ is an FO-formula

pMpnq, s, σq |ø @xψ

pMpnq, s, σq |ø EpψUψ1 q iff

pMpnq, s, σq |ø EpψRψ1 q iff

• iff for all u P spvarpnqq, pM, s, σxu q |ø ψ
• for some π P Pathpsq, for some i ¥ 0, pMpnq, πpiq, σq |ø ψ1 and for all j � i, pMpnq, πpjq, σq |ø ψ
• for some π P Pathpsq, either for some i ¥ 0, pMpnq, πpiq, σq |ø ψ and for all j / i pMpnq, πpjq, σq |ø ψ1 , or for all i ¥ 0 pMpnq, πpiq, σq |ø ψ1
• iff ag P t1, . . . , nu implies pMpnq, s1 , σq |ø ψry �� ags, for ag P apar

We remark that the semantics of ECTLzX operators in Def. 10 is standard, while quantification over regular parameters ranges on the active domain spvarpnqq. However, differently fromDef. 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 s1 pvarpnqq. As a result, quantification in FO-ECTLzX gives us a language that is strictly more expressive than propositional ECTLzX.

An FO-ECTLzX formula ψ is true in state s, or pMpnq, sq |ø ψ, iff for all interpretations σ, pMpnq, s, σq |ø ψ; ψ is true in Mpnq, or Mpnq |ø ψ, iff pMpnq, initq |ø ψ. In light of decidability limitations (see [Bloem et al., 2015] for a detailed discussion), hereafter we consider prenex mindexed FO-ECTLzX 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-ECTLzX 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-ECTLzX. 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-ECTLzX are preserved fromM Apnq toMpnq.

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 iA is obtained by restricting the range of variables in cnti to DA.

Further, given P-DAMAS MA � xt, ey, the abstract PDAMAS M � xtA, eAy is the collection of abstractions tA and eA built on DA.

Given n P N, the DAMAS M Apnq for n agents per abstract template tA is defined as the composition of n copies of tA with the abstract environment eA, in analogy with Def. 6 and 7. In particular, observe that if s is a state in DAMASM 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 inM Apnq, then s α�� s1 inMpnq.

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.

Theorem3. LetMpnq be aDAMASwith abstractionM Apnq defined on DA � D. For every states s in M Apnq and formula φ in FO-ECTLzX, if M Apnq |ø φ, thenMpnq |ø φ.

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 M PA whose concrete systems satisfy the same FO-ECTLzX 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 M PA . 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 � g1 px11 , . . . , x1k1q ❀ v11 :� x11 ; . . . ; v1k1 :� x1k1 is defined as the guarded command id � gpx1, . . . , xkq ^ g1 px11 , . . . , x1k1q ❀ v1 :� x1; . . . ; vk :� xk; v11 :� x11 ; . . . ; v1k1 :� x1k1 .

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 , σ1 q, we write a � a1 � pγ � γ 1 , σ Y σ1 q 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 M PA associated with MA.

Definition 15 (Associated PIIS). The PIIS M PA � @tPA, ePAD associated with P-DAMAS MA � @tA, eAD over domain DA Y tae syncu is obtained from tA, eA by defining the following sets of actions for tPA and ePA :

ActtPA: A is the set of asynchronous actions; tar?s | a P AEtu is the set of agent-environment actions; and AEe Y tar!s � aer!s | a P AEt , ae P AEe, ida � idae u Y ta � ae | a P GSt , ae P GSe, ida � idae u is the set of global-synchronous actions.

ActePA: tar?s | a P AEeu is the set of agentenvironment actions and GSe Ytar!s | a P GSeu is the set of global-synchronous actions.

Above we assume that ae sync is initially set to K. Also, every action of tPA 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 systemM 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-ECTLzX formulas. Since the initial states of corresponding concrete systems are related, the systems satisfy the same FO-ECTLzX 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.

Theorem5. LetMbe a P-DAMASwith abstractionMA. Let M PApnq be the PIIS associated with MA. Then, for every formula φ in FO-ECTLzX, 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 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.

1 Note 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].

Theorem 6. Let M be a P-DAMAS with abstraction MA such that MA P NB. Then, for every m-indexed formulae φ in FO-ECTLzX, 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 FOECTLzX. This takes as input a P-DAMAS M and an mindexed FO-ECTLzX 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 � xLa, 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 � xLb, initb, Actb, Pb, τby is such that

• ctrb � ttvalue, bidu, with both tvalue and bid ranging over Q Y tuuu.

2 This 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 id12 � 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, id12 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 � @ag a: 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 � @ag a: 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 M1A 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 SVeDaS (ANR-16-CE40-0021).