Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems

1 Introduction

Modal temporal-epistemic logic has long been adopted as a formalism for reasoning about multi-agent systems (MAS). In its basic setting it consists of either the linear or the branching version of discrete-time temporal logic, augmented with knowledge modalities for the agents in the system. Several properties of MAS (e.g., perfect recall, no learning, synchronicity) have been axiomatised on the widely adopted semantics of Interpreted Systems [Fagin et al., 1995]. In the past decade several model checking methodologies and toolkits that use temporal-epistemic specification languages have been developed [Penczek and Lomuscio, 2003; Gammie and van der Meyden, 2004; Lomuscio et al., 2009].

Two key assumptions are made in the basic setting of the formalism above. Firstly, facts are expressed in propositional terms. Secondly, the number of agents is finite and given at design time. As a consequence, the indexes of individual knowledge operators are constants in a finite set Ag of agents, while the indexes for group knowledge operators are finite subsets of Ag. Proposals have been made to overcome the first limitation by introducing first-order versions of temporal-epistemic logic both on quantified versions of interpreted systems [Belardinelli and Lomuscio, 2012] and on artifact-centric multi-agent systems [Belardinelli et al., 2014]. These approaches surmount the shortcomings of a purely propositional language by extending the syntax to first-order formulas. In some cases completeness can be retained [Belardinelli and Lomuscio, 2012] and verification can

Alessio Lomuscio

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

in principle be performed on finite abstractions [Belardinelli and Lomuscio, 2013; Belardinelli et al., 2014].

Regarding the second limitation, proposals have been put forward to consider a set of objects that vary at design time; the set of agents is normally considered to be finite in each system run. This is a sensible assumption in many scenarios, but there are applications of MAS (e.g., e-commerce, smart grids) where an unbounded number of agents may freely enter and leave the system at run time. There is, therefore, a need to account for the unbounded and possibly infinite agents joining in or leaving an open MAS. In this setting it is still of interest to reason about their evolution and what they know individually and collectively. For example, in an auction setting, such as fishmarkets [Rodr´ıguez-Aguilar et al., 1998], different agents attend different auctions at run time. Nonetheless, all of them, however many they may be, will eventually know what the reserve price for a particular good is. Formally, such a temporal-epistemic specification can be expressed in the proposed formalism as:

(1) intuitively expresses that any good x has always a price y that will eventually be learnt by all agents z currently attending the auction. A key feature of this specification is that agents appear as quantifiable terms in the logical language and appear as such in the indexes of the epistemic operators. In particular, compare the subformula ∀zKzPrice(y, x) of (1), where the quantification domain of ∀z changes depending on the state, with the standard temporal-epistemic formula ∧a∈Ag KaPrice(y, x), which assumes Ag fixed. In this paper we propose a formalism accounting for (1); we show that, while the verification problem is undecidable in general, bounded MAS admit finite abstractions.

Related Work. A quantified doxastic logic, with modalities indexed by variables, was introduced in [Lomuscio and Colombetti, 1996]. However, this focused on a 3-valued semantics in view of providing sound axiomatisations. In contrast, here we consider a 2-valued semantics and the model checking problem. Various classes of models and types of quantifications have been developed recently to account for Artifact-centric Systems [Belardinelli et al., 2012; 2014; Hariri et al., 2013]. While our work is influenced by the techniques introduced therein, none of these contributions deals with open MAS with a possibly infinite number of agents.

In [Montali et al., 2014] agents appear in the relational structure, but there is no explicit quantification on them. This feature, however, may be useful in a number of scenarios, as we argue in this paper. There are also similarities with recent work on parametrised verification of MAS [Kouvaros and Lomuscio, 2013a; 2013b]. However, parametrised verification aims at establishing whether properties hold irrespective of the finite but unbounded number of agents in the system; here we deal with an infinite set of agents which we only bound at a state and not in the whole model. Closer to our approach is [Belardinelli and Grossi, 2015] which introduces a semantics for dynamic agent networks; however, epistemic operators are not discussed there.

Scheme of the paper. In Section 2 we formalise open multi-agent systems in our setting and introduce a novel firstorder temporal-epistemic logic CTLKx. We state the model checking problem for this setting (Section 2.2) and illustrate the formal machinery with a use case (Section 2.3). Section 3 contains the main theoretical results on the existence of finite, bisimilar abstractions. We conclude and point to future work in Section 4.

2 OpenMulti-agent Systems

In this section we present a formalism to reason about open multi-agent systems (OMAS). A key feature of OMAS is that agents may join and leave the system at run time. We then put forward a first-order version of the temporal-epistemic logic CTLK to reason about OMAS, that allows us to index knowledge operators with variables. We conclude by formulating the model checking problem for OMAS. Since we wish to account for possibly infinite domains of objects and agents we import some basic terminology from related literature [Abiteboul et al., 1995; Belardinelli et al., 2014].

Definition 1 (Database schema and instance) A database schema is a finite set D = {P1/q1, . . . , Pn/qn} of predicate symbols P with arity q ∈ N.

Given a (possibly infinite) interpretation domain X, a Dinstance over X is a mapping D associating each predicate symbol P to a finite q-ary relation on X, i.e., D(P) ⊆ Xq .

For a database schema D, D(X) is the set of all Dinstances on X; while the active domain adom(D) is the finite set ⋃P∈D {u1, . . . , uq ∈ X | 〈u1, . . . , uq〉 ∈ D(P)} of all individuals occurring in some predicate interpretation D(P). Further, the primed version of a database schema D as above is the schema D′ = {P ′1/q1, . . . , P ′n/qn}. Then, the disjoint union D ⊕ D′ of D-instances D and D′ is the (D ∪ D′ )-instance s.t. (i) D ⊕ D′ (P) = D(P), and (ii) D ⊕D′ (P ′ ) = D′ (P). Hereafter, primed versions and disjoint unions are used to account for the temporal evolution of a database from the previous state D to the next state D′ .

2.1 Agents in OMAS

To introduce OMAS, we import some preliminary notions from [Belardinelli and Grossi, 2015]. Hereafter we assume a finite number of agent types T0, . . . , Tk. Each agent type T comprises (i) a local database schema DT , and (ii) a finite set ActT of parametric actions α(⃗x). Hence, agents of the same type share the database schema and available actions. For every agent type T , AgT , Ag′T , . . . are (possibly infinite) sets of agent names. In the rest of the paper, the interpretation domain X contains a set AgT of agent names for each type T , i.e., X = Ag ∪ U for Ag = ⋃type T AgT and some other (possibly empty) set U of elements. We will also consider a set Con ⊆ X of constants, including names for agents. To describe the temporal evolution of OMAS, we define protocols for agent types. To do so, we first introduce isomorphisms on database instances.

Definition 2 (Instance Isomorphism) Instances D ∈ D(X) and D′ ∈ D(X′ ) are isomorphic, or D ≃ D′ , iff for some bijection ι : adom(D) ∪ Con ↦→ adom(D′ ) ∪ Con, (i) ι is the identity on Con; (ii) ι is type-preserving, i.e., for every type T , ι is a bijection from (adom(D) ∪ Con) ∩ AgT into (adom(D′ ) ∪ Con) ∩ Ag′T ; and (iii) for every P ∈ D, ⃗u ∈ Xq , ⃗u ∈ D(P) iff ι(⃗u) ∈ D′ (P).

Whenever the above holds, we say that ι is a witness for D ≃ D′ and write D ι≃ D′ to state this explicitly. While isomorphisms depend on the set Con of constants, in what follows we consider Con fixed and omit it.

We now introduce the local protocol PrT for a type T .

Definition 3 (Protocols) Given domain X, PrT is a function from DT (X) to 2ActT (X) , where ActT (X) is the set of ground actions α(⃗u), for α(⃗x) ∈ ActT and ⃗u ∈ X|⃗x| .

By Def. 3 the protocol PrT returns a ground action in ActT (X) for every DT -instance. In the rest of the paper we assume the following requirement on protocols:

So, by requirement (∗) isomorphic states allow "isomorphic" ground actions. Most OMAS of interest satisfy (∗). For example, in an English auction an agent may make a valid bid as long as the bid is above the current best price.

We now introduce the notion of agent.

Definition 4 (Agents) Given an agent name a ∈ AgT of type T , an agent is a tuple a = 〈DT , ActT , PrT 〉 where DT , ActT , and PrT are defined as above.

We assume a finite number of agent types, but we do not assume a bound on the number of agents of each type in any concrete instantiation of the system. This is common place in OMAS, such as in services, auctions, etc., whereby engineers have prior knowledge of the behaviour of the agent types without knowing how many instances of each type will be executed at runtime. We provide an example of this in Section 2.3. Agents as in Def. 4 are related to the notion of agent templates introduced in [Kouvaros and Lomuscio, 2013a; 2013b]. However, while the latter assumes that any concrete run admits a finite number of agents built on these types, we do not make this assumption here.

In the following an agent is often identified with her name; therefore we write a = 〈Da, Acta, Pra〉 and omit the type. By Def. 4 a local state l ∈ Da(U ∪Ag) encodes the knowledge of agent a about the elements in U as well as fellow agents in Ag. Thus, a fundamental difference with the standard approach to multi-agent systems [Parikh and Ramanujam, 1985;

Fagin et al., 1995; Wooldridge, 2001] is that the agent's information is structured as a relational database.

We can now introduce OMAS to represent the interactions amongst agents, beginning with the notion of global state.

Definition 5 (Global States) Given a finite subset A ⊆ Ag of agents ai = 〈Di, Acti, Pri〉 defined on domain X = U ∪ Ag, for i ≤ n, a global state is a tuple s = 〈l0, . . . , ln〉 of instances li ∈ Di(X) s.t. ⋃i≤n adom(li) ∩ Ag ⊆ A.

Note that, while we admit an infinite number of agents in existence, only a finite number of them can be active at any given time, and different agents can be active at different times, thus accounting for the openness of the system. Also by Def. 5, a global state s comprises at least all agents appearing in its active domain adom(s) = ⋃i≤n adom(li). For instance, if agent a appears in the local state lb ∈ Db(X) of agent b ∈ A, and thus a ∈ adom(s), then a also belongs to A. By assuming a fixed enumeration of agents, we will identify global states containing the same local states for the same agents, possibly in a different order. Further, let ag be the function that for any global state s = 〈l0, . . . , ln〉 returns the set ag(s) = {a0, . . . , an} of agents s.t. li ∈ Dai (X) for i ≤ n. By the requirement above on global states, for every state s, adom(s) ∩ Ag ⊆ ag(s). We let G be the set ⋃n∈N(∏i≤n Dai (X)) of all global states. As a consequence, G is infinite whenever X is.

To account for the knowledge of agents, we say that states s = 〈l0, . . . , ln〉 and s′ = 〈l′0 , . . . , l′m〉, of possibly different lengths, are epistemically indistinguishable for agent ai, or s ∼i s′ , iff ai ∈ ag(s), ai ∈ ag(s′ ), and li = l′i . Since s and s′ can be tuples of different length, an agent does not generally know the exact number of active agents at each moment, nor their identity. Observe that if a /∈ ag(s), then the set {s′ ∈ G | s′ ∼a s} is empty. That is, if agent a is not active in state s, then no state is indistinguishable for her. We elaborate more on this point in Section 2.2.

Finally, we introduce open multi-agent systems.

Definition 6 (OMAS) Given a (possibly infinite) domain X = Ag ∪ U containing a (possibly infinite) set Ag = {a0, a1, . . .} of agents ai = 〈Di, Acti, Pri〉, an open multiagent system is a tuple P = 〈Ag, U, I, τ 〉 where

• I is the set of initial states s0 for some finite ag(s0) ⊆ Ag;
• τ : G ×Act(X) ↦→ 2G is the global transition function, where Act is the set of joint (parametric) actions, and τ(〈l0, . . . , ln〉, 〈α0(⃗u0), . . . , αn(⃗un)〉) is defined iff αi(⃗ui) ∈ Pri(li) for every i ≤ n.

An OMAS describes all system's executions from an initial state s0 ∈ I, according to the global transition function τ, which returns the successor states τ(s, α(⃗u)) ⊆ G given the current state s and joint ground action α(⃗u) by all agents in s. Since the domain X is typically infinite, OMAS are infinitestate systems in general. Specifically, OMAS are open and dynamic as global states may be tuples of different length, comprising different agents. Differently from most literature on MAS [Parikh and Ramanujam, 1985; Fagin et al., 1995; Wooldridge, 2001], which assumes that the set of agents is finite and fully specified at design time, here the successor states returned by the transition function may contain fewer or more agents w.r.t. the current state.

We now state a requirement on joint actions in OMAS. To introduce it, we first extend isomorphisms to global states. Definition 7 (State Isomorphism) The global states s ∈ G and s′ ∈ G′ are isomorphic, or s ≃ s′ , iff for some bijection ι : adom(s) ∪Con ∪ ag(s) ↦→ adom(s′ ) ∪Con ∪ ag(s′ ), for every aj ∈ ag(s), ι is a witness for laj ≃ l′ι(aj) .

Any function ι as above is a witness for s ≃ s′ , also indicated as s ι≃ s′ . As for instance isomorphisms, ≃ is an equivalence relation, and by Def. 7 isomorphic states are tuples of the same length. In the rest of the paper we impose the following requirement on the transition functions in OMAS:

Similarly to protocols, requirement (+) guarantees that actions performed with "isomorphic" values in isomorphic states, also return isomorphic states. In Section 2.3 we will discuss an OMAS satisfying (+); but similar assumptions are common place in database theory and the theory of programming languages [Hariri et al., 2013; Deutsch et al., 2007].

We now introduce some useful notation. We define the transition relation s → s′ on global states iff s α(⃗u) ---→ s′ for some joint ground action α(⃗u), i.e., s′ ∈ τ(s, α(⃗u)). An srun r is an infinite sequence s0 → s1 → · · · , with s0 = s. For n ∈ N, we set r(n) = sn . A state s′ is reachable from s iff s′ = r(i) for some s-run r and i ≥ 0. Hereafter we enforce seriality on the transition relation → by assuming skip actions. Further, we introduce S as the set of states reachable from some initial state s0 ∈ I. Since the domain X may be infinite, the set S of reachable states is also infinite in principle. Indeed, OMAS are infinite-state systems in general. Finally, we will refer to the global database schema Ds = D0 ∪ · · · ∪ Dn of a state s = 〈l0, . . . , ln〉, and the corresponding Ds-instance Ds s.t. Ds(P) = ⋃i≤n li(P), for P ∈ Ds. Therefore, we suppose that each agent has a truthful, yet limited, view of the global database Ds. Also, the disjoint union s ⊕ s′ is defined as state s′′ = 〈l′′ 0 , . . . , l′′m〉 on ag(s) ∪ ag(s′ ) s.t. (i) if ai ∈ ag(s) ∩ ag(s′ ) then l′′ i = li ⊕ l′i ; (ii) if ai ∈ ag(s) \ ag(s′ ) then l′′ i = li; and (iii) if ai ∈ ag(s′ ) \ ag(s) then l′′ i = l′i .

2.2 The Specification Language FO-CTLKx

We now introduce FO-CTLKx, a first-order extension of the temporal epistemic logic CTLK, as a specification language for OMAS. Differently from other quantified temporalepistemic logics [Belardinelli et al., 2014], FO-CTLKx features an expressive formulation of the epistemic operators that can be indexed by individual terms. Below we consider a set Var of individual variables containing a set VarAg of variables for agents, as well as the database schema D = ⋃type T DT . Terms t, t′ , . . . are either variables or constants in Con.

Definition 8 (FO-CTLKx) The FO-CTLKx formulas are defined in BNF as follows:

where t, t′ are terms, P ∈ D, a ∈ Con∩Ag, z ∈ VarAg, and ⃗t is a q-tuple of terms.

The temporal formulas AXϕ and AϕUϕ′ (resp. EϕUϕ′ ) are read as "for all runs, next ϕ" and "for every (resp. some) run, ϕ until ϕ′ ". The epistemic formula Ktϕ means that "the agent denoted by t knows ϕ". The fact that epistemic modalities are indexed to terms represents a significant difference w.r.t. standard approaches. Free and bound variables are defined as standard, as well as sets var(φ) (resp. fr(φ), con(φ)) of all variables (resp. free variables, constants) in φ. Notice that z ∈ fr(Kzφ) and a ∈ con(Kaφ). The same symbols are sometimes used to refer to individual variables and action parameters, the context will disambiguate.

To define the satisfaction of an FO-CTLKx formula on an OMAS, we introduce the notion of an assignment σ : Var ↦→ X s.t. for every z ∈ VarAg, σ(z) ∈ Ag. We denote by σx u the assignment s.t. (i) σx u (x) = u; and (ii) σx u (x′ ) = σ(x′ ) for every x′ different from x. Also, σ(c) = c for all c ∈ Con.

Definition 9 (Semantics of FO-CTLKx) We define whether an OMAS P satisfies a formula ϕ in a state s according to assignment σ, or (P, s, σ) |= ϕ, as follows (clauses for propositional connectives are omitted as straightforward):

A formula ϕ is true at s, or (P, s) |= ϕ, if (P, s, σ) |= ϕ for all assignments σ; ϕ is true in P, or P |= ϕ, if (P, s0) |= ϕ for all s0 ∈ I. We remark that Def. 9 adopts an active domain semantics, where quantifiers range over the set adom(s) ∪ ag(s) of active individuals and agents. This is an extension to agents of the standard assumption in database theory, also used in data-aware systems [Belardinelli et al., 2014; Hariri et al., 2013]. Also, notice that the active domain may vary at each state. Furthermore, by definition of epistemic indistinguishability, if a /∈ ag(s) then (P, s, σ) |= Kaϕ, for all formulas ϕ, as for no s′ ∈ S, s′ ∼a s. In other words, epistemic formulas are vacuously true for agents not in the active domain of the state considered. So, for an epistemic formula not to be satisfied, it is required that an agent in the active domain does not know the fact in question.

Finally, we state the model checking problem for OMAS with respect to the specification language FO-CTLKx.

Definition 10 (Model Checking Problem) Given an OMAS P and an FO-CTLKx formula ϕ, determine whether for every initial state s0 ∈ I, (P, s0, σ0) |= ϕ for some assignment σ0.

Def. 10 assumes that the transition function τ is given as a computable function, and that we have finitary descriptions for the set I of initial states and the domain X. These requirements are normally fulfilled in cases of interest (see Section 2.3). Moreover, the specification ϕ is typically an FOCTLKx sentence, with no free variables. Hence, the model checking problem reduces to determine whether P |= ϕ. Model checking general data-aware systems is known to be undecidable [Deutsch et al., 2007]. In [Belardinelli et al., 2012; 2014] this problem is proved decidable for bounded and uniform systems. However, all these contributions assume that the set of agents is fixed at design time. In [Belardinelli and Grossi, 2015] preliminary results on the verification of a particular class of OMAS are presented, but without considering the epistemic dimension.

2.3 Use Case: Knowledge in openMAS networks

We now illustrate the formalism introduced by means of an example on agent networks. In [Belardinelli and Grossi, 2015] it is shown how a non-probabilistic variant of the SIR network diffusion model (see [Jackson, 2008, Ch. 7]) can be formally verified against first-order, purely temporal specifications. In the SIR model a group of agents connected in a network structure goes through three different stages during an 'epidemic' involving the spread of diseases, ideas, information, or similar social phenomena. First, each agent is susceptible to be infected; she may actually get infected at a certain point depending on whether any of her neighbors in the network are also infected; then an agent will eventually recover. OMAS can be used to encode open and dynamic SIR models, also incorporating the epistemic aspects of diffusion. The specification language FO-CTLKx allows us to express properties of SIR models concerning: (i) how knowledge influences diffusion through the network; and (ii) how knowledge itself spreads within the system.

Let a binary predicate N denote the network structure, so N(x, y) means that agents x and y are connected; while the unary predicates Sus, Inf and Rec denote the properties of being susceptible, infected, and recovered respectively. As examples of the first group of properties consider the following formulas:

Formula (2) states that it is always the case that if an agent x knows that she is connected to an infected agent y, then she will part at some point in the future. Formula (3) states that it is always the case that if an agent x knows she is susceptible, then eventually she will always be connected only to recovered agents.

We stress the fundamental difference between a quantified formula ∀xKxφ, which express dynamically the joint knowledge of φ for all active agents in a given state s, and the standard, static epistemic formula Eφ = ∧a∈Ag Kaφ. Actually, for Eφ to be a formula, the set Ag of agents has to be finite and specified at design time. Moreover, a formula such as AG ∀xKxφ refers to the knowledge of a possibly different group of active agents at each time.

As examples of the second group of properties above consider the following formulas:

Formula (4) states that it is always the case that if an agent is recovered, then this fact won't be ignored, i.e., someone will know it. Formula (5) states that it is always the case that if some agent y is infected, then all agents that are connected to y will eventually know this fact. We stress once more that to express epistemic properties, such as (2)-(5) above, in open MAS we do need epistemic modalities indexed by terms and quantification, as the set Ag of agents is infinite in general.

In the next section we develop techniques to model check OMAS against such first-order temporal-epistemic specifications.

3 Bisimulation

In Section 2 we stated that model checking OMAS against FO-CTLKx specifications is undecidable in general. To single out semantical fragments with a decidable model checking problem, we first introduce a notion of bisimulation and show that bisimilar OMAS satisfy the same FO-CTLKx formulas. The results presented in this section build upon previous work in the literature [Belardinelli et al., 2012; 2014; Belardinelli and Grossi, 2015]. However, the present setting differs, as we consider open MAS, where agents can join and leave at run time, and our specification language contains term-indexed epistemic modalities.

In the rest of the paper we let P = 〈Ag,U, I, τ〉 and P ′ = 〈Ag′ ,U ′ , I ′ , τ ′ 〉 be OMAS and assume that s = 〈l0, . . . , ln〉 ∈ S and s′ = 〈l′0 , . . . , l′n 〉 ∈ S ′ . According to Def. 7 isomorphic states have the same relational structure, but to account also for values assigned to free variables we introduce the following notion.

Definition 11 (Equivalent assignments) Given states s ∈ S and s′ ∈ S ′ , and a formula φ, assignments σ : Var ↦→X and σ′ : Var ↦→ X′ are equivalent for φ (w.r.t. s and s′ ) iff for some bijection γ : adom(s) ∪ ag(s) ∪ Con ∪ σ(fr(ϕ)) ↦→ adom(s′ ) ∪ ag(s′ ) ∪ Con ∪ σ′ (fr(ϕ)), (i) the restriction γ|adom(s)∪ag(s)∪Con is a witness for s ≃ s′ ; and (ii) σ′ |fr(ϕ) = γ ◦ σ|fr(ϕ).

Equivalent assignments preserve agent types, the (in)equalities in ϕ, as well as the active elements in s and s′ , modulo renaming.

Bisimulations are known to preserve the satisfaction of modal formulas in a propositional setting [Blackburn et al., 2001, Ch. 2]. We now investigate under which conditions this is true of OMAS as well.

Definition 12 (Simulation) A relation R ⊆ S ×S ′ is a simulation iff R(s, s′ ) implies (i) s ≃ s′ ; (ii) for every t ∈ S, if s → t then for some t′ ∈ S ′ , s′ → t′ , s ⊕ t ≃ s′ ⊕ t′ , and R(t, t′ ); and (iii) for every t ∈ S, a ∈ ag(s), if s ∼a t then for some t′ ∈ S ′ , s′ ∼a t′ , s ⊕ t ≃ s′ ⊕ t′ , and R(t, t′ ).

A state s′ simulates s iff R(s, s′ ) holds for some simulation R. In particular, similar states are isomorphic by condition 12.(i) above. Simulations can then be extended to bisimulations.

Definition 13 (Bisimulation) A relation B ⊆ S × S ′ is a bisimulation iff both B and B-1 = {〈s′ , s〉 | 〈s, s′ 〉 ∈ B} are simulations.

Two states s and s′ are bisimilar, or s ≈ s′ , iff B(s, s′ ) holds for some bisimulation B. Notice that ≈ is the largest bisimulation and an equivalence relation on S ∪ S ′ . Finally, the OMAS P and P ′ are bisimilar, or P ≈ P ′ , iff (i) for every s0 ∈ I, s0 ≈ s′0 for some s′0 ∈ I ′ , and (ii) for every s′0 ∈ I ′ , s0 ≈ s′0 for some s0 ∈ I.

In [Belardinelli et al., 2014] it is shown that, differently from the propositional modal case, in data-aware systems bisimilarity does not preserve first-order temporal-epistemic formulas. Nonetheless, we prove that uniform OMAS admit FO-CTLKx-preserving bisimulations.

Definition 14 (Uniformity) An OMAS P is uniform iff for every s, t, s′ ∈ S, t′ ∈ G, (i) if s → t and s ⊕ t ≃ s′ ⊕ t′ then s′ → t′ ; and (ii) for every a ∈ ag(s), if s ∼a t and s ⊕ t ι≃ s′ ⊕ t′ then s′ ∼ι(a) t′ .

Intuitively, uniformity expresses a fullness condition on OMAS: a uniform OMAS allows all "isomorphic" transitions. We discuss uniformity in more depth in Section 3.

We finally prove that FO-CTLKx formulas cannot distinguish between bisimilar and uniform OMAS, as longs as specific cardinality constraints on the interpretation domains are satisfied.

Theorem 1 Consider bisimilar and uniform OMAS P and P ′ , bisimilar states s ∈ S and s′ ∈ S ′ , an FO-CTLKx formula ϕ, and assignments σ and σ′ equivalent for ϕ w.r.t. s and s′ . If

1. for every s-run r, for every k ≥ 0, (i) |X′ | ≥ |adom(r(k)) ∪ ag(r(k)) ∪ adom(r(k + 1)) ∪ ag(r(k + 1)) ∪ Con ∪ σ(fr(ϕ))| + |var(ϕ) \ fr(ϕ)|, and (ii) |Ag′T | ≥ |agT (r(k))∪agT (r(k+1))∪Con∪σ(fr(ϕ))|+ |var(ϕ) \ fr(ϕ)| for every type T;
2. for every s′ -run r′ , for every k ≥ 0, (i) |X| ≥ |adom(r′ (k))∪ag(r′ (k))∪adom(r′ (k+1))∪ag(r′ (k+ 1)) ∪ Con ∪ σ′ (fr(ϕ))| + |var(ϕ) \ fr(ϕ)|, and (ii) |AgT | ≥ |agT (r′ (k)) ∪ agT (r′ (k + 1)) ∪ Con ∪ σ′ (fr(ϕ))| + |var(ϕ) \ fr(ϕ)| for every type T ;

As a consequence of Theorem 1, bisimilar states satisfy the same FO-CTLKx formulas for equivalent assignments, whenever cardinality constraints (1) and (2) are satisfied.

We now apply Theorem 1 to the model checking problem for OMAS. First of all, we introduce bounded OMAS.

Definition 15 (Bounded OMAS) An OMAS P is bbounded, for b ∈ N, iff for all s ∈ S, |adom(s) ∪ ag(s)| ≤ b.

An OMAS P is bounded iff it is b-bounded for some b ∈ N. We remark that bounded OMAS are still infinite-state systems in general. Hereafter let sups∈S{|adom(s)∪ag(s)|} be equal to ∞ whenever the OMAS P is unbounded. Similarly for sups∈S {|agT (s)|}.

Corollary 2 Consider bisimilar and uniform OMAS P and P ′ , and an FO-CTLKx formula ϕ. If

1. |X′ | ≥ 2 sups∈S{|adom(s) ∪ ag(s)|} + |con(φ)| + |var(ϕ)| and |Ag′T | ≥ 2 sups∈S{|agT (s)|}+|con(φ)|+ |var(ϕ)| for every type T;
2. |X| ≥ 2 sups′∈S ′{|adom(s′ ) ∪ ag(s′ )|} + |con(φ)| + |var(ϕ)| and |AgT | ≥ 2 sups′∈S ′{|agT (s′ )|} + |con(φ)| + |var(ϕ)| for every type T ;

Corollary 2 shows that an infinite-state OMAS P can in principle be verified by model checking a bisimilar system P ′ , as long as X′ is sufficiently large for P ′ to bisimulate P.

In the next section we show that finite abstractions can indeed be defined for bounded OMAS, thus allowing for the verification of properties, such as (2)-(5) in Section 2.3, but first we briefly discuss uniform OMAS.

Discussion: Uniformity The notion of uniformity was put forward in [Belardinelli et al., 2012] to prove the decidability of model checking data-aware systems. In [Belardinelli et al., 2014] uniformity is related to genericity in databases [Abiteboul et al., 1995]. Intuitively, in uniform systems trasitions depend on the logical form of data, rather than on the actual data content. It has been argued that the class of uniform systems covers most cases of interest [Hariri et al., 2013; Deutsch et al., 2007].

We now analyse uniformity in the context of OMAS through the following result.

Lemma 3 Suppose that an OMAS P satisfies the following:

Then, P is uniform.

The proof of Lemma 3 makes essential use of conditions (∗) and (+) on protocols and transition functions respectively. Thus, requirements (i) and (ii) in Def. 14 can be substituted by closure (⋆) of initial states under isomorphism. The latter condition is quite natural, as we are mainly interested in the relational structure of data, not the actual data content. In the final section we assume that all OMAS satisfy (⋆) and are therefore uniform.

3.1 Finite Abstraction

We now show that an infinite OMAS can in principle be verified by checking a finite abstraction. The main result is Theorem 5, which ensures that boundedness and closure under uniform initial states (⋆) are sufficient to obtain finite bisimilar abstractions, thus preserving FO-CTLKx formulas.

We first define the notion of abstract agents.

Definition 16 (Abstract agents) Let a = 〈D, Act, Pr〉 ∈ AgT be an agent of type T defined on a domain X = U ∪Ag. Given a set X′ = U ′ ∪ Ag′ of elements, the abstract agent a′ ∈ Ag′T is the tuple 〈D, Act, Pr′ 〉 on X′ s.t. Pr′ is the smallest function defined as

• if α(⃗u) ∈ Pr(l), l′ ∈ D′ (X′ ) and l′ ι≃ l, then α(ι(⃗u)) ∈ Pr′ (l′ ).

Given a set AgT of agents, let Ag′T be the set of the corresponding abstract agents. Notice that Ag and Ag′ are used to denote both the set of agent names and of agents; the context will disambiguate. The abstract agent a′ in Def. 16 is indeed an agent of type T, as defined in Def. 4, since a and a′ share the same database schema and actions. Moreover, protocol Pr′ is well-defined whenever Pr is, and it satisfies condition (∗) on protocols by definition. We now present abstractions.

Definition 17 (Abstractions) Let P = 〈Ag,U, I, τ〉 be an OMAS, and Ag′ the set of abstract agents defined on X′ as in Def. 16. The OMAS P ′ = 〈Ag′ ,U ′ , I ′ , τ ′ 〉 is an abstraction of P iff (i) I ′ = {s′0 ∈ G′ | s′0 ≃ s0 for some s0 ∈ I}, and (ii) τ ′ is the smallest function defined as follows

• if s α(⃗u) ---→ t in P, s′ , t′ ∈ G ′ , and s ⊕ t ≃ s′ ⊕ t′ for some witness ι, then s′ α(ι(⃗u)) ----→ t′ .

The abstraction P ′ in Def. 17 is an OMAS as it complies with Def. 6. Moreover, condition (+) on transition functions is satisfied. Notice that, by varying X′ we can obtain abstractions of different cardinalities, in particular finite abstractions.

Next, we explore the relationship between an OMAS and its abstractions. By the next result every abstraction is uniform, independently from the concrete OMAS.

Lemma 4 Every abstraction P ′ of an OMAS P is uniform. Moreover, if P is uniform and X′ = X, then P ′ = P.

By the next result there exists a bisimilar abstraction for every bounded OMAS, provided that the former is built over a sufficiently large domain. Hereafter we suppose that, for a bound b ∈ N, Nb is the maximum numbers of parameters contained in any parametric joint actions, i.e., Nb = b · max{α(⃗x)∈ActT ,type T}{|⃗x|}.

Theorem 5 Consider a bounded OMAS P over an infinite domain X, an FO-CTLx formula ϕ, and a domain X′ ⊇ con(ϕ). If (i) |X′ | ≥ 2b + |con(ϕ)| +max{|var(ϕ)|,Nb}, and (ii) for every type T, |Ag′T | ≥ 2b + |con(ϕ)| + max{|var(ϕ)|,Nb}, then there exists a bisimilar abstraction P ′ of P over X′ . In particular, P |= ϕ iff P ′ |= ϕ.

Notice that each Ag′T and X′ in Theorem 5 might as well be finite. So, by using a sufficient number of abstract agents and values, we can in principle reduce the model checking problem for infinite-state OMAS to the verification of a finite abstraction. Specifically, we obtain the following corollary to Theorem 5.

Corollary 6 Given a bounded OMAS P over an infinite domain X, and an FO-CTLx formula ϕ, there exists an abstract OMAS P ′ over a finite domain X′ s.t. ϕ holds in P iff it holds in P ′ .

As a consequence of Corollary 6, we can in principle verify an infinite-state, bounded OMAS, by model checking its finite, bisimilar abstraction.

4 Conclusions

In this paper we addressed the formal verification of MAS where an infinite number of agents may in principle be present and may be entering and leaving the system at run time. A notable feature of our proposal concerns the specification language FO-CTLKx, which includes epistemic operators indexed by individual terms. As we discussed, the latter are key to express relevant properties of OMAS. We analysed the model checking problem in this setting and showed that it can be addressed through finite bisimilar abstractions, under some natural conditions.

An open problem not tackled in the present contribution and left for future work is the development of methodologies for generating finite abstractions, so that effective model checking procedures can be provided. This is a major challenge for the verification of open MAS.

Acknowledgements The research described in this paper was partly funded by the EPSRC Research Project "Trusted Autonomous Systems" (grant No. EP/I00520X/1).