Verifying Emergent Properties of Swarms

1 Introduction

Robot swarms have been put forward as an alternative to single-robot systems for a wide variety of applications including search and rescue, de-mining, and surveillance. Robots in a swarm are behaviourally identical agents interacting with each other and the environment by following relatively simple protocols [Bonabeau et al., 1999]. Due to their nature, individual agents in a swarm can interact in subtle ways, thereby displaying global properties for the swarm system that are difficult to predict. Yet, for robot swarms to be deployed in key applications, guarantees about their behaviours need to be provided.

Recent research has begun to address the problem of verifying that robot swarms behave according to their specifications. This is a challenging problem because, in contrast to traditional systems, swarms are typically deployed in varying number of units. It is tolerated, expected even, that some units may develop a fault while the swarm is operating, or that a swarm may be deployed in varying number of components depending on the domain. So for validation purposes it is not sufficient to verify that a swarm satisfies a given property of interest for a determined number of components; instead, we are required to ascertain that the property is satisfied for any number of agents in the swarm. This entails verifying an unbounded number of systems and leads to a problem that is undecidable in general [Apt and Kozen, 1986].

In this paper we address a related yet different problem, namely when it is the case that a swarm displays an emergent behaviour. While no commonly accepted formal definition exists, by global or emergent behaviour it is often meant a configuration, or a characteristic property of the swarm as a whole, that may be difficult to predict with certainty when

[Bonabeau

et al., 1999]. A notable characteristic of flocking, shoaling and herd behaviour is that the emergent behaviour may be exhibited only when some conditions on the number of agents present is met.

In this paper we aim to develop the foundations for establishing that, given the individual description of the agents, a certain emergent behaviour will be displayed by the system. We are interested in establishing a lower bound on the number of agents to be present for a given emergent property to be displayed. The methodology that we put forward is sound and complete; so if the swarm admits the emergent behaviour, then this fact will be established. In this case the method also guarantees that any swarm composed of any number of agents greater than the bound will exhibit the behaviour.

Related Work. We are not aware of previous work addressing the question above. Traditional research in verification of swarm systems involves the application of model checking techniques to particular instances of known swarm algorithms [Dixon et al., 2012; Brambilla et al., 2014; Kloetzer and Belta, 2007]. Systems over a certain size become quickly intractable; hence, while a property can be shown to be satisfied, no consideration on emergent behaviour can be drawn. Much closer to our work are the techniques described in [Kouvaros and Lomuscio, 2013b; 2015] where methods for the parameterised verification of interleaved interpreted systems are put forward. These, however, cannot be used to verify emergence as we do here, as they are tailored to establishing that a system meets its specifications irrespective of the number of components considered. In contrast, here we identify whether population thresholds exist for the swarm to display an emergent behaviour. While the abstract models we introduce below resemble the ones used in [Kouvaros and Lomuscio, 2015], the semantics and the notion of simulation we develop here are radically different, including all the procedures which, crucially, depend on the property under examination.

2 Swarm Systems

Swarm systems are typically composed of an arbitrary number of simple and identical robotic agents interacting with the environment. In line with common theoretical assumptions made in the literature [Sahin, 2005; Brambilla et al., 2013] we here assume that each agent operates on a two-dimensional arena and communicates with its peers and the environment by means of a wireless sensor of limited range. The framework we present can be extended for agents operating in three dimensions, such as flying machines, but the assumed arena will make our presentation more concise. We consider the arena to be finite and we allow it to wrap around, similarly to a sphere, i.e., for an α×α arena, the cell (1, 1) is one position to the right of the cell (1, α). We also assume that the robots update their state with high frequency; so we can model them by assuming synchronicity even if at any instance some robots may be idle [Dixon et al., 2012]. To model dynamic swarms we introduce a variant of interpreted systems [Fagin et al., 2003], the standard semantics for multi-agent systems, and extend it to agent templates [Kouvaros and Lomuscio, 2015].

Models for swarms. We represent robots in a swarm by means of agents modelled by a generic template agent R(α, β) = (L, I, Act, P, t) operating in an α × α ∈ N × N arena with localised communication capabilities of a limited range β ∈ N. A template agent R(α, β) comprises a set of local states L = Loc × S representing the Cartesian product between the set Loc = {1, . . . , α} × {1, . . . , α} of the arena square cells and the set S of private local states. The private states represent internal configurations of the agent, whereas Loc represents the position of the agent in the arena. Given a local state l = (x, y, s), a local state l′ = (x′ , y′ , s′ ) with min(|x-x′ |, α-|x-x′ |) ≤ β, min(|y-y′ |, α-|y-y′ |) ≤ β is said to be in the communication range for the agent when in l, or, equivalently, in its neighbourhood. We denote this by l ⋉ l′ . For an agent i in state l, an agent j in state l′ is said to be in agent i's neighbourhood, denoted by i⋉j, if l⋉l′ . Furthermore, R(α, β) is defined by considering a set I ⊆ L of initial local states and a nonempty set Act of (local) actions. When α, β are assumed to be given, we simply write R for R(α, β). The framework can accommodate a finite number of template agents; for simplicity we do not pursue this here.

The template agent's actions are performed in compliance with a protocol P : L → P(Act) that defines which actions may be performed at a given local state. The evolution of the agent is characterised by a (local) transition function t : L × LE ×Act × P(Act) ×ActE → L. The transition function returns the next agent's local state given the current agent's local state, the environment's state (see below), the agent's action, the set of actions performed by the agents in its neighbourhood, and the environment's action.

The template environment E = (LE, IE, ActE, PE, tE) is defined by a nonempty set of states LE, a nonempty set of initial states IE ⊆ LE, and a nonempty set of actions ActE. E also includes a protocol PE : LE → P(ActE), and a transition function tE : LE × ActE × P(Act) → LE returning the environment's next local state given its current state, its action, and the set of actions performed by all the agents in the swarm.

We define a swarm system (SS) as a tuple S = 〈R, E, V〉, where R is a template agent, E is a template environment and V : L × LE → P(AP) is a labelling function on the Cartesian product of the template agent's states and the environment's states for a set AP of atomic propositions. S gives an abstract description of an unbounded collection of concrete swarm systems, each one obtained by instantiating the SS with the number of actual agents in the system. So, differently from the generic SS S = 〈R, E, V〉, given an n ≥ 1 the concrete swarm S(n) will encode precisely n agents interacting with the environment.

Let {1, . . . , n} denote the set of the concrete agents in S(n). For any i ∈ {1, . . . , n}, the i-th concrete agent Ri = (Li, Ii,Acti, Pi, ti) is defined as follows: Li = L × {i}; Ii = I × {i}; Acti = Act; Pi is given by a ∈ Pi((l, i)) iff a ∈ P(l); and ti is given by ti((l, i), lE, a,A, aE) = (l′ , i) iff t(l, aE, a,A, aE) = l′ . So, each local state of a concrete agent is made of the template local states indexed by the name of the agent in question and inherits from its template the actions, the protocols and the transition function.

A global state g = (l1, . . . , ln, lE) is a tuple of local states for all the agents in the system and the environment; it represents a snapshot of the system at a particular instant of time. Given a global state g we write g.i to denote the local state of agent i in g. Given an agent i ∈ {1, . . . , n}, we let N(g, i) = {j ∈ {1, . . . , n} | i ⋉ j} to denote the set of agents in the neighbourhood of i when at a global state g.

Consider ACT (n) = Act1 ×. . . Actn ×ActE to be the set of all possible joint actions that may be performed in S(n). Given ¯a ∈ ACT(n), let ¯a.i denote the action of agent i in ¯a. The agents' local protocols and local evolution functions determine the temporal evolution of the system's global states via a sequence of joint actions as defined below.

Definition 1 (Global transition relation). The global transition relation T (n) ⊆ G(n)×ACT (n)×G(n) on a set G(n) of concrete global states of a concrete system S(n) is defined as (g, ¯a, g′ ) ∈ T (n) iff the following hold.

1. ¯a.E ∈ PE(g.E) and tE(g.E, ¯a.E,A) = g′ .E, where A = {¯a.i | i ∈ {1, . . . , n}};
2. For all i ∈ {1, . . . , n}, we have ¯a.i ∈ Pi(g.i) and ti(g.i, g.E, ¯a.i,A, a.E) = g′ .i, where A = {¯a.j | j ∈ N(g, i)}.

So, for S(n) to transition from a global state g to a global state g′ via a joint action ¯a, the following is required: the origin and target states and actions for the environment are in compliance with the environment's protocol and transition function; the origin and target local states and actions of each participant are in compliance with their respective concrete protocols and transition functions; finally, for every agent i, the set of actions performed by the agents in i's neighbourhood is in compliance with i's transition function. Thus, the global transition relation reflects the localised, interactive nature of swarms.

A path is a finite or infinite sequence π = g1 ¯a1 g2 ¯a2 g3 . . . with (gi , ¯ai , gi+1 ) ∈ T (n), for every i ≥ 1 whenever applicable. Given a path π, we write π(i) for the i-th state in π. The set of all paths originating from a state g is denoted by Π(g). A global state g is said to be reachable from a global state g1 if there is a path π ∈ Π(g1 ) such that π(i) = g, for some i ≥ 1.

We now have all the ingredients to define our concrete semantics, i.e., the notion of concrete swarm system.

Definition 2 (Concrete swarm system). Given a swarm system S = 〈R, E, V〉 and n ≥ 1, the concrete swarm system

(CSS) S(n) is a tuple S(n) = 〈G(n), I(n), T (n), V(n)〉, where G(n) ⊆ L1 × . . . ×Ln ×LE is the set of global states reachable via T (n) from the initial global states I(n) = I1×. . .×In×IE, and V(n) : G(n) → P(AP×{1, . . . , n}) is a labelling function for a set AP ×{1, . . . , n} of local atomic propositions such that (p, i) ∈ V(n)(g) iff p ∈ V(g.i, g.E).

Hence a swarm system S is a concise description of an unbounded collection {S(n) | n ≥ 1} of concrete swarm systems, each made of a different number of identical agents.

Swarm properties. We adopt the temporal-epistemic logic CTLK [Penczek and Lomuscio, 2003] as a specification language for robot swarms. By means of CTLK we can express properties of the agents as well as their states of knowledge over time. Given a set of agents {1, . . . , n} and a set of local atomic propositions AP × {1, . . . , n}, the CTLK formulae are defined by the following BNF grammar:

where p ∈ AP × {1, . . . , n} and i ∈ {1, . . . , n}. The epistemic modality Kiφ represents "agent i knows that φ" [Fagin et al., 2003]. The temporal formula EXφ stands for "there is a path such that φ holds at the next step"; E[φUψ] denotes "there is a path such that at some point ψ holds and before then φ is true along the path"; and EGφ means "there is a path such that φ is globally true". Dual temporal modalities prefixed by the path quantifier A ("for all paths") can be defined as standard [Huth and Ryan, 2004]. The interpretation of CTLK formulae on a CSS S(n) = 〈G(n), I(n), T (n), V(n)〉 is given as usual [Clarke et al., 1999; Fagin et al., 2003]: the temporal modalities are interpreted by means of the global transition relation, and the epistemic modalities are interpreted by the epistemic possibility relations ∼i∈{1,...,n}= {(g, g′ ) ∈ G(n) × G(n) | g.i = g′ .i}. We write (S(n), g) |= φ to denote that the formula φ is true at state g in S(n). We refer to [Penczek and Lomuscio, 2003] for the usual definition of the satisfaction relation |=. A formula φ is said to be true in S(n), denoted S(n) |= φ, if (S(n), ι) |= φ for every ι ∈ I(n).

As it is typical in the analysis of unbounded systems [Clarke et al., 1989], we consider specifications that reflect the parametric nature of swarms. To do this, we use propositional variables to index the atomic propositions and epistemic modalities appearing in a specification. We write φ({v1, . . . , vm}) to indicate that each of the variables v1, . . . , vm appears in an atomic proposition or epistemic modality in φ. We verify SS against properties of the form

(∧i,j∈{1,...,m}¬(vi = vj) → φ({v1, . . . , vm}))

∀v1 . . . ∀vm where ∀ is a universal quantifier over the variables. We denote such a formula as ∀V φ(V ), where V = {v1, . . . , vm}, and we say that ∀V φ(V ) is an m-indexed formula if |V | = m. In other words, when evaluated on a concrete system S(n), the formula ∀V φ(V ) denotes a CTLK formula expressing the conjunction of all its ground instantiations under any assignment for V from the domain {1, . . . , n}. For example, assume a foraging scenario [Liu et al., 2007], and suppose that we want to express the following property: "whenever a robot starts searching for food, it knows that it will eventually deposit food in the nest".

We can express this property with the 1-indexed formula ∀{i}AG(si → Ki(AFdi)), where s (search) and d (deposit) are atomic propositions that hold in the appropriate states, and AFφ ≜ A[⊤Uφ]. When evaluated on S(2), the formula denotes AG(s1 → K1(AF d1)) ∧ AG(s2 → K2(AF d2)).

Following the symmetric nature of ∀V (φV ), the formula can be evaluated by considering only the ground instantiation obtained by assigning pairwise distinct values to the variables in V from the domain {1, . . . ,m} [Kouvaros and Lomuscio, 2013a]. For example, the above formula can be evaluated simply by considering its ground instantiation AG(s1 → K1(AFd1)). For the rest of the paper, an m-indexed formula equivalently refers to its aforementioned ground instantiation.

Identification of emergent behaviour. Swarm robots are typically designed to achieve a global behaviour [Bonabeau et al., 1999]. Often, properties of interest displayed during the agents' interactions are referred to as emergent behaviour. The formal analysis of emergent behaviour has been mainly studied on predefined number of participants [Brambilla et al., 2014; Dixon et al., 2012]. However, no technique based on fixed numbers of participants can ensure the robustness of a swarm with respect to a global behaviour. When the number of participants varies the overall behaviour may change. For instance a simple local protocol might ensure that 10 flying robots remain in a flocking formation, only for this pattern to break down by adding a further robot to the swarm. This is an issue that does not arise in single robot systems and presents a severe difficulty for the swarm approach [Brambilla et al., 2013]. One approach recently put forward aims to establish that a specification holds on a swarm for any number of agents in the system [Kouvaros and Lomuscio, 2015]. However, the method addresses a related, but different issue; moreover it suffers from constraints in terms of which swarms can be modelled, essentially forcing every pair of concrete systems to be behaviourally identical. In contrast here we aim to obtain the threshold over which an emergent property holds, irrespective of the behaviours displayed by the swarm instances under the boundary condition.

To do this we begin by defining emergent behaviour formally. Intuitively the emergent behaviour is displayed by the swarm only when the swarm is sufficiently populated.

Definition 3 (Emergent behaviour). Given an SS S, an mindexed formula φ is said to be an emergent behaviour exhibited by S if there is an emergence threshold t ∈ N such that for all t′ ≥ t we have S(t′ ) |= φ.

Thus, differently from the standard treatment of unbounded systems concerning the satisfaction of a formula by all concrete systems [Emerson and Kahlon, 2000], we are here interested in whether or not an emergence threshold exists. The definition above immediately gives raise to the following decision problem.

Definition 4 (Emergence identification problem). The emergence identification problem (EIP) takes as input an mindexed formula φ and an SS S and returns as output the threshold t ∈ {0,m,m+ 1, . . . } for φ and S. If t = 0, then S admits no threshold for φ.

We do not present the problem above as outputting true and false, but this can be done without loss of generality.

The definition of threshold above is related to the previously adopted, but stronger definition of cutoffs in [Kouvaros and Lomuscio, 2015], which refer to the number of agents that is sufficient to consider when evaluating any formula on the system. We stress the two notions are different and require a separate technical treatment. While procedures for solving the parameterised verification problem are typically incomplete, as we show in the next section, by giving a specification-dependent procedure we can obtain a sound and complete procedure to solve the EIP.

3 Emergence Identification Procedure

We now put a formal technique to solve the EIP defined above. Clearly we cannot solve the EIP by generating all the swarm concrete instances, as the number of systems to consider is unbounded. Instead, we identify an emergence threshold for either the property in question or its negation. Note that if the system does not admit any emergent behaviour, we can still use the notion of threshold above to establish the negation of the property under consideration. Also observe that we do not assume the threshold to be minimal; so if an SS admits an emergence threshold for a given emergent property φ, then it admits infinitely many.

Cycle-Stuttering Simulation. We begin by defining the degree of temporal depth for a CTLK formula by counting the temporal operators nested in a formula. We then define a simulation relation that preserves CTLK formulas up to a level of depth. In the following, we fix an m-indexed formula φ and two CSS S(n) = 〈G(n), I(n), T (n), V(n)〉 and S(n′ ) = 〈G(n′ ), I(n′ ), T (n′ ), V(n′ )〉, where n, n′ ≥ m.

Definition 5. The temporal depth td(φ) of φ is inductively defined as follows.

where φ, ψ are CTLK formulae and i ∈ {1, . . . , m}.

The notion of temporal depth finds a correspondence in the cycle-stuttering simulation equivalence that we now introduce. Intuitively, S(n) and S(n′ ) are cycle-stuttering simulation equivalent if they are behaviourally identical modulo stuttering of cyclic behaviours. To formally define this equivalence, we first introduce some preliminary definitions.

A substring δ = π(i), . . . , π(j) of a concrete path π in S(n) is said to be a cycle if V(n)(π(i)) = V(n)(π(j)). A cycle δ′ in π corresponds to the x-th repetition of δ if δ′ = δx , e.g., δ′ = abababa = (aba)3 . A cyclicdecomposition of π is an inductive partition of π into alternating non-cyclic and cyclic blocks. Each non-cyclic block is a finite sequence of states in π without repetitions, whereas each cyclic block corresponds to a (possibly infinite) repetition of a cycle in π and it can be further partitioned into cyclic and non-cyclic blocks. For example, consider the path π = abcbcbdabcbcbda. The partition [[a][bcb]2 [da]]2 is a cyclic decomposition of π, where [[a][bcb]2 [da]]2 is a cyclic block, [a], [da] are non-cyclic blocks, and [bcb]2 is a cyclic block; the partition [a][bcb]2 [da][bcb]2 [da] is also a cyclic decomposition of π. Given a non-cyclic block C, we write C(i) for the i-th state in C, and |C| for the sequence's length. For a cyclic block Cx , we write Cx [i] for the sequence of states corresponding to the i-th repetition of the cycle associated with Cx . If Cx cannot be decomposed further, then we treat each Cx [i] as a non-cyclic block, otherwise we treat it as a cyclic decomposition.

Definition 6. The relations ≈d⊆ G(n) × G(n′ ) and ∼=d⊆ S(n) × S(n′ ) are defined as follows.

We start by defining two states g and g′ to be ≈0-related if V(n)(g) = V(n′ )(g′ ). Then, for all d ≥ 0, we define ∼=d as follows. Two paths π and π′ (either both finite or both infinite) are ∼=d-related if there is a cyclic decomposition C1Cx1 1 C2Cx2 2 . . . of π and a cyclic decomposition C ′1C′x′1 1 C ′2C′x′2 2 . . . of π′ such that for all i ≥ 1, Ci ∝d C ′ i and Cxi i ∝d C′x′i i , where

• Ci ∝d C ′ i if: (i) |Ci| = |C′ i |; (ii) for each 1 ≤ j ≤ |Ci|, we have Ci(j) ≈d C ′ i (j).
• Cxi i ∝d C′x′i i if: (i) either xi = x′i or xi > d + 1, x′i > d + 1; (ii) for every pair Cxi i [z], C′x′i i [z′ ] of repetitions of Cxi i and C′x′i i , we have Cxi i [z] ∝d′ C′x′i i [z′ ], where d′ = min(d + 1, xi - z, x′i - z′ ) - 1.

So, Ci ∝d C ′ i if: (i) the blocks have the same length; and (ii) each pair (Ci(j),C′ i (j)) of states is ≈d-related. Two blocks Cxi i and C′x′i i are ∝d-related if: (i) the blocks agree up to d + 1 on the number of repetitions of their associated cycles; and (ii) each pair of repetitions (Cxi i [z], C′x′i i [z′ ]) is ∝d′ -related, where d′ + 1 is the greatest number of repetitions in {1, . . . , d + 1} such that Cxi i [z] and C′x′i i [z′ ] can both "see" d′ + 1 repetitions ahead in their blocks.

Finally, we define ≈d+1 as follows. Two states g and g′ are ≈d+1-related if: i) for every path π ∈ Π(g) there is a path π′ ∈ Π(g′ ) such that π ∼=d π′ ; and ii) for every path π′ ∈ Π(g′ ) there is a path π ∈ Π(g) such that π′ ∼=d π.

Definition 7. We say that S(n) and S(n′ ) are cycle-stuttering simulation equivalent, denoted by S(n) ≡d S(n′ ), if ι ≈d ι′ for every pair (ι, ι′ ) of initial states in I(n) × I(n′ ).

The following proposition can easily be established.

Proposition 1. Let π ∼=d π′ . Then for each state π(i), there is a state π′ (i′ ) such that π(i) ≈d π′ (i′ ). Further, for each state π(j) in π(1), . . . , π(i), there is a state π′ (j ′ ) in π′ (1), . . . , π′ (i′ ) such that π(j) ≈d π′ (j ′ ).

Formulas with temporal nesting up to d are preserved by cycle-stuttering simulation of degree d.

Proof sketch. The proof is by induction on d in which each case is shown by structural induction on φ. The φ = EXψ case follows by observing that the successor states of two ≈drelated states are ≈d-1-related. The cases of EG[ψ1Uψ2]

and EGψ are shown using Proposition 1. The case for Kiψ (i ∈ {1, . . . ,m}) is shown as follows. Let g ≈d g′ . If g |= Kiψ, then g1 |= ψ for all g1 with g ∼i g1 . Assume g′1 such that g′ ∼i g′1 . By Proposition 1, there is a state g2 in G(n) with g′1 ≈d g2 ; therefore g ∼i g2 , hence g2 |= ψ. So, the inductive hypothesis gives g′1 |= ψ, hence g′ |=Kiψ.

Emergence Threshold Identification Procedure. We can now give an emergence threshold identification procedure (ETIP) for solving the emergence identification problem. ETIP takes as input an SS S and an m-indexed formula φ, and returns an integer t ≥ m representing an emergence threshold for S and φ. If ETIP returns t = 0, then φ is not an emergent property for S.

ETIP first calls an auxilliary potential threshold identification procedure (PTIP). PTIP takes as input S and φ and returns an integer t′ corresponding to either an emergence threshold for φ on S, or an emergence threshold for ¬φ on S. Then, following the potential threshold computation, ETIP employs standard model checking algorithms for CTLK, e.g., those implemented by MCMAS [Lomuscio et al., 2009], to check whether S(t′ ) |= φ. If the latter is the case, then t′ is an emergence threshold and thus φ is an emergent behaviour exhibited by S. In this case ETIP returns t = t′ ; if S(t′ ) ̸|= φ, ETIP returns returns t = 0.

We now describe the PTIP, which returns an integer t′ > m such that S(n) ≡td(φ) S(n′ ), for every n, n′ ≥ t′ . By Theorem1, the latter implies that t′ is an emergence threshold for either φ or ¬φ. PTIP operates by means of three steps.

Step 1: Construction of the Abstract Model. In the first step, an abstract model ˆ S(m) is built. ˆ S(m) is an abstraction of any concrete system from S of arbitrary size. Its definition is inspired by models used in [Emerson and Namjoshi, 1996], but modified to represent the current semantics. ˆ S(m) is defined as the tuple ˆ S(m) = 〈 ˆ G(m), ˆ I(m), ˆ T (m)〉, where ˆ G(m) ⊆ L1×. . .×Lm×(P(L)\{∅})×LE is the set of abstract states; ˆ I(m) = I1×. . .×Im×(P(I)\{∅})×IE is the set of initial abstract states; and ˆ T (m) ⊆ ˆ G(m) ×Λ× ˆ G(m) is the abstract transition relation for a set of labels Λ = P(L × Act × P(Act) × L) \ {∅}.

An abstract state γ = (l1, . . . , lm, X, lE) consists of a concrete component γ.c = (l1, . . . , lm, lE) and an abstract component γ.ˆa = X. γ represents any concrete state g in S(n), n > m, in which: (i) the environment is at local state lE; (ii) the agents 1, . . . ,m are at local states l1, . . . , lm, respectively; (iii) X = {g.i | i ∈ {m+1, . . . , n}} is the set of local states of the agents m+ 1, . . . , n. Thus γ.c encodes the atomic propositions on which φ is built, and γ.ˆa encodes how an arbitrary number of agents may interfere with the state of γ.c. To see this, consider a transition (γ, Ξ, γ ′ ) ∈ ˆ T (m), representing a set of transitions between the concrete states represented by γ and γ ′ . The label Ξ indicates the template transitions enabling the agents to participate in a global transition. In other words, a tuple (l, a,A, l′ ) ∈ Ξ indicates that in a global transition at least one agent is in state l; this agent performs action a, its neighbours perform the set of actions A, and the agent moves to state l′ .

For a set Ξ ⊆ Λ, let Act(Ξ) = {a | ∃l, l′ , A. (l, a, A, l′ ) ∈

Ξ} to be the set of actions performed by Ξ. Given a template state l ∈ L, consider ˆN(Ξ, l) = {a | ∃l′ , l′′ , A. (l′ , a, A, l′′ ) ∈ Ξ and l ⋉ l′} to be the set of actions performed by Ξ in the neighbourhood of l. The construction of ˆ S(m) is completed by defining ˆ T (m) as follows: (γ, Ξ, γ ′ ) iff there is a joint action ¯a ∈ Act1 × . . . × Actm × ActE such that:

1. The transition is valid for the environment: ¯a.E ∈ PE(γ.c.E) and tE(γ.c.E, ¯a.E,A) = γ ′ .c.E, where A = Act(Ξ) ∪ {¯a.i | i ∈ {1, . . . ,m}};
2. The transition is valid for a concrete agent: for all i ∈ {1, . . . ,m}, we have ¯a.i ∈ Pi(γ.c.i) and ti(γ.c.i, γ.c.E, ¯a.i,A, ¯a.E) = γ ′ .c.i, where A = ˆN(Ξ, γ.c.i) ∪ {¯a.j | j ∈ N(γ.c, i)};
3. The transition is valid for the agents represented by γ.ˆa: For all (l, a,A, l′ ) ∈ Ξ, we have l ∈ γ.ˆa, l′ ∈ γ ′ .ˆa, a ∈ P (l), t(l, γ.c.E, a, A, ¯a.E) = l′ , and A = ˆN(Ξ, l)∪ {¯a.i | i ∈ {1, . . . ,m} and l ⋉γ.c.i};
4. For every l ∈ γ.ˆa, there is a transition label in Ξ to a state l′ ∈ γ ′ .ˆa, and for every l′ ∈ γ ′ .ˆa, there is a transition label in Ξ from a state l ∈ γ.ˆa.

A path in ˆ S(m) is either a finite or infinite sequence γ 1Ξ1γ 2 , . . . with (γ i , Ξi , γ i+1 ) ∈ ˆ T (m), for every i ≥ 1 whenever applicable. We now establish a correspondence between any CSS S(n), n > m, and ˆ S(m) as follows. Define δn to map concrete states from S(n) to abstract states in ˆ S(m) as δn(g) = (g.1, . . . , g.m, {g.j | j ∈ {m+1, . . . , n}}, g.E). Assume ζn to map tuples in T (n) to tuples in Λ by ζn(g, ¯a, g′ ) = {(l, a,A, l′ ) | ∃i ∈ {m+1, . . . , n} s.t. g.i = l, ¯a.i = a,A = {¯a.j | j ∈ N(g, i)}, and g′ .i = l′}. Finally, define θn to map paths in S(n) to paths in ˆ S(m) by θn(g1 ¯a1 g2 . . .) = δn(g1 )ζn(g1 , ¯a1 , g2 )δn(g2 ) . . ..

Lemma 1. For a path π in S(n), θn(π) is a path in ˆ S(m).

The above gives the correspondence between ˆ S(m) and a CSS S(n). Following this, the covering lemma from [Emerson and Namjoshi, 1996] can be adapted here to show that for every path π in S(n) and for every n′ > n, there is a path π′ in S(n′ ) such that θn(π) = θn′ (π′ ). Thus S can only exhibit additional behaviour as the number of agents grows. This gives rise to the completeness of our procedure as it implies an emergence threshold for either φ or its negation. The threshold corresponds to a t′ ≥ m with S(n) ≡td(φ) S(n′ ), for every n, n′ ≥ t′ . We now proceed to compute it by counting the sufficient number of agents to enable every behaviour (modulo cyclic-stuttering) in ˆ S(m). To do this, we do not consider infinite paths as they may require an infinite number of concrete agents. In other words, we first prune the computation tree of ˆ S(m).

Step 2: Pruning. We now build the computation tree of ˆ S(m) by including all and only the paths in ˆ S(m) that do not contain any cyclic repetition for td(φ) + 1 times. More precisely, for a state γ ∈ ˆ G(m), we associate a labelled computation tree T(γ) rooted at γ that is inductively defined as follows.

• T0 (γ) consists of exactly one node with label γ.
• Tn+1 (γ) consists of root node r with label γ, and for every transition (γ, Ξ, γ ′ ) ∈ ˆ T (m), r has a subtree Tn (γ ′ ) with edge label Ξ iff there is no path in Tn+1 (γ) containing a cycle with td(φ) + 1 repetitions.

It is easy to see that there is a k ∈ N such that Tk (γ) is isomorphic to every Tk′ (γ) with k′ ≥ k. We write T(γ) to denote this tree. Note that T(γ) is finite. A path B in T(γ) is a sequence r1Ξ1 . . . Ξx-1 rx such that r1 is the root, rx is a leaf, and for every 1 ≤ i ≤ x - 1, Ξi is the label for the edge between ri and ri+1 . We write B(i) for the i-th node in B, B(i, Λ) for the i-th label in B, and |B| for the number of nodes in B.

Step 3: Counting. Consider a path B in T(γ). Define B(0,Λ) = ∅, and B(i,Λ) = ∅ whenever B(i) is a leaf node. Then, given a template state l, define in(B(i), l) = |{l′ | (l′ , a,A, l) ∈ B(i -1,Λ)}|, and out(B(i), l) = |{l′ | (l, a,A, l′ ) ∈ B(i,Λ)}|. So, in any concrete transition (γ, ¯a, γ ′ ) that corresponds to (B(i - 1), Ξ,B(i)), out(B(i - 1), l) is the least number of agents that need to transition from l in γ, and in(B(i), l) is the least number of agents that need to transition to l in γ ′ . Thus, let et(B(i), l) = max(0, out(B(i)) - in(B(i))). Then, define et(B(i)) = ∑l∈L et(B(i), l) and et(B) = ∑i∈|B| et(B(i)). Finally, let et(T(γ)) = max(et(B) | B is a path in T(γ)) and et( ˆ S(m)) = max(et(T(ι)) | ι ∈ ˆ I(m)) +m. We obtain the following.

Theorem 2. et( ˆ S(m)) corresponds to exactly one of the following: (i) an emergence threshold for S and φ; or (ii) an emergence threshold for S and ¬φ.

Proof sketch. The thesis follows by showing that S(n) ≡td(φ) S(n′ ), for any n, n′ ≥ et( ˆ S(m)).

The above concludes the analysis of the ETIP. The procedure first constructs the abstract model ˆ S(m) for the SS S in question. Then, for a formula φ under analysis, it prunes the computation tree of ˆ S(m) to include only td(φ) cyclic repetitions. Finally, the procedure counts the number t′ = et( ˆ S(m)) of agents required for a CSS to include every behaviour of said tree. By Theorem 2, t′ corresponds to an emergence threshold either for φ or for ¬φ. Since t′ is computable, the procedure is complete. This is because an emergence threshold for ¬φ implies that there is no emergence threshold for φ. In other words, if S(t′ ) |= φ, then t′ is an emergence threshold for φ, and therefore φ is an emergent behaviour. Otherwise, t′ is an emergence threshold for ¬φ, and thus φ is not an emergent behaviour.

4 Verifying the Beta Aggregation Algorithm

We exemplify the methodology described so far on the Beta aggregation algorithm [Nembrini, 2005] (here described in a simplified manner), a protocol used to aggregate robots somewhere on a grid. To begin, given a robot i, define a lost robot j to be a robot satisfying i ⋉ j in the previous time step but not in the current step. Each robot i obeys two simple rules.

The first rule concerns the number of i's neighbours that can observe a lost robot in their neighbourhoods. If this number is less than a predefined threshold β for at least one lost robot, then robot i performs a 180◦ turn. The second rule concerns the number of i's neighbours. If the first rule does not apply and the number of i's neighbours increases during a time step, then the robot performs a random 90◦ turn. If neither rule can be applied, the robot moves forward one cell.

Fix a 5×5 arena, assume a communication range of 1, and let β = 0. We can easily encode the Beta algorithm as an SS S consisting of a template agent R(5, 1) that reflects the rules above for the action selection and state evolution. The state encodes (among other concepts) the set Z of occupied cells of the agent's neighbours' neighbourhoods (See [Beta, 2015] for the full encoding).

We say that a robot i is connected to a robot j if j is in the transitive closure of i's neighbours. Note that, given the size of the arena and the communication range, i and j are connected in a global state iff they agree on the sets Z of cells encoded in their local state. Thus, associate a fresh atomic proposition q for each set Q of cells and assign q to each template state with Z = Q. Consider the formula φ = ∀{v,u}KvAFAG ∨Q(qv ∧ qu) expressing "every robot knows that eventually it will be forever connected to every other robot". This means that not only the whole swarm will be connected in a single cluster, but everyone will know to be connected. We are interested to check whether φ emerges in S as the number of robots increases in the system. Following the procedure of the previous section, we can compute an emergence threshold of 16 (the full calculation is reported in [Beta, 2015]). Thus, we conclude that φ is an emergent behaviour iff S(16) |= φ. The latter query can be solved by any epistemic model checker, which would return false, thereby establishing that ¬φ is satisfied by every S(n), for n ≥ 16. So the robots will not eventually congregate into a stable cluster.

We conclude that the property above is not an emergent property of the Beta protocol. We emphasise that the above result cannot be obtained with traditional model checking nor simulation techniques since an unbounded number of systems would have to be considered.

5 Conclusions and FurtherWork

We have introduced a technique for determining automatically whether a swarm will display an emergent behaviour irrespective of the number of agents present. The technique is provably sound and complete. While we have put forward a fully automatic methodology, our methodology can also be used to complement simulations for fast prototyping. Specifically, if early simulations on small populations show a particular behaviour to emerge, we can then use the technique here described to check whether this behaviour will still be displayed by larger systems. In future work we intend to implement the technique here presented into a toolkit that can be paired to well-established simulation toolkits to achieve this.

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