Verifying Fault-Tolerance in Probabilistic Swarm Systems

1 Introduction

Swarm robotics is commonly seen as the key technology for many forthcoming robotic applications from logistics, search and rescue, manufacturing and maintenance and beyond [S¸ahin, 2005]. While the technology has shown much promise, a key difficulty in adopting swarm robotics in either safety-critical or humans in the loop applications is to give guarantees on behaviour of the swarm before deployment. A key difficulty lies in the fact that swarms are often realised by arbitrarily large collections of robots. While methods such as model checking [Baier and Katoen, 2008] can be used to study particular ground instantiations [Dixon et al., 2012], they cannot be adopted to reason about a system of which the number of components is unknown. Indeed, this problem is known to be undecidable [Apt and Kozen, 1986] in general.

The method of parameterised model checking [Bloem et al., 2015] has been adapted for swarm systems specified by a variety of AI-inspired specifications [Kouvaros and Lomuscio, 2016] and recently extended to capture open systems in which agents may join and leave at run-time [Kouvaros et al., 2019] and systems incorporating probabilities [Lomuscio and Pirovano, 2019].

A key issue to establish before deployment is not just the correctness of the system, but the extent to which faults occurring at runtime can compromise the system safety. The method of safety analysis via fault injection and model checking is well established in dependable systems [Bozzano and Villafiorita, 2007; Bozzano et al., 2017]. Via safety-analysis the engineer can establish the consequences of particular faults in the system and identify particular weaknesses or critical faults which may compromise the system's safety. The method also allows engineers to establish the resilience of the system in adverse circumstances, contributing to the construction of safety arguments in certification.

Safety analysis via fault injection [Ezekiel and Lomuscio, 2017] has been used in AI to establish the resilience of autonomous systems [Ezekiel et al., 2011] and extensions have been explored in a swarm setting [Kouvaros and Lomuscio, 2017]. However, no method to date has addressed fault injection for probabilistic swarms. Since most swarm protocols are probabilistic in nature, this makes it impossible to perform safety analysis on unbounded swarm systems. This paper intends to rectify this shortcoming.

Related Work. Previous work has addressed the verification of fault-tolerance in multi-agent systems [Ezekiel and Lomuscio, 2017; Ezekiel et al., 2011]. In turn this builds on earlier work on safety analysis [Bozzano and Villafiorita, 2007] that has been successfully adopted in avionics [Bozzano et al., 2017]. While this work is relevant, the present contribution deals with unbounded swarms, where the number of agents is not known at design time, and, differently, from these, exhibit probabilistic behaviour.

A considerable body of research has been devoted to parametrised verification of non-probabilistic systems without any fault injection [Aminof et al., 2018; Aminof et al., 2016; Bloem et al., 2015]. The work presented here is distinct in that the systems we consider are probabilistic and we perform safety analysis by injecting faults into the templates.

Fault-tolerance in systems with an unbounded number of agents has been considered in a number of different semantics, including some geared to network protocols [John et al., 2013] and others catering for swarm systems [Kouvaros and Lomuscio, 2017; Kouvaros et al., 2018]. Note, however, that none of these semantics can express stochastic behaviour nor probabilistic specifications as we do here.

Closest to the work here pursued is a line of work in which probabilistic systems with a possibly unbounded number of agents are considered [Lomuscio and Pirovano, 2019; Lomuscio and Pirovano, 2020]. Note, however, that this work does not consider the mechanism of fault injection typical in safety analysis as we do here. Other work in the parameterised verification of probabilistic network protocols [Graham, 2008; Fournier, 2015] also fails to address faults.

In summary, the work presented here is distinct from the existing literature in that, to the best our knowledge, it addresses the safety analysis via fault injection for unbounded swarm systems that are governed by stochastic behaviour.

2 Background

In this section we introduce some background on probabilistic model checking of swarm systems, along with the notation that we will use throughout the paper. We follow [Lomuscio and Pirovano, 2019] in notation.

Discrete TimeMarkov Chains. We briefly summarise discrete time Markov chains [Kwiatkowska et al., 2007; Baier and Katoen, 2008; Kemeny et al., 1976].

Definition 1 (DTMC). A discrete-time Markov chain (DTMC) is a tuple D = 〈S, ι, t, L〉 where S is a finite set of states, ι ∈ S is a distinguished initial state, t : S×S → [0, 1] is a transition probability function (with ∑s′∈S t(s, s′ ) = 1 for any s ∈ S) and L : S → P(AP) is a labelling function on a set AP of atomic propositions.

A path in a DTMC is a sequence of states s0s1s2 . . . such that for every i ∈ N it is the case that t(si, si+1) > 0. We use FPathD and IPathD respectively, to denote the set of all finite and infinite paths starting from the initial state ι. For a finite path we define its probability by PD(s0 . . . sn) ≜ ∏n-1 i=0 t(si, si+1). Following [Kemeny et al., 1976], this can be extended to define a probability on infinite paths. Note that the probability of an infinite path occurring is uniquely defined by the probabilities of its finite prefixes occurring. For a measurable set of paths X ⊆ FPathD or X ⊆ IPathD we define PD(X) ≜ ∑ρ∈X PD(ρ).

Markov Decision Processes. We mostly follow the notation used in [Forejt et al., 2011] and refer to [Baier and Katoen, 2008; Puterman, 1994] for more details.

Definition 2 (MDP). A Markov decision process (MDP) is a tuple M = 〈S, ι, A, P, t, L〉 where S is a finite set of states, ι ∈ S is a distinguished initial state, A is a finite set of actions, P : S → P(A) is a protocol function (such that P(s) ̸= ∅ for all s ∈ S), t : S ×A×S → [0, 1] is a transition function (with ∑s′∈S t(s, a, s′ ) = 1 for any s ∈ S and a ∈ P(s)) and L : S → P(AP) is a labelling function on a set AP of atomic propositions.

Intuitively, a transition from a state s of an MDP occurs by first non-deterministically selecting some action a ∈ P (s) and then transitioning to state s′ with probability t(s, a, s′ ). MDPs thus give a way of describing systems that include both probabilistic and non-deterministic choice, unlike DTMCs which do not capture the latter.

A path in an MDP is a sequence of states and actions s0a0s1a2 . . . such that for all i ∈ N it is the case that ai ∈ P(si) and t(si, ai, si+1) > 0. We use FPathM (IPathM, respectively) to denote the set of all finite (infinite, respectively) paths starting from the initial state ι. For a finite path ρ = s0a0 . . . sn, last(ρ) ≜ sn denotes its last state.

In order to reason about the probability of a path occurring in an MDP, we need a way to resolve the inherent nondeterminism. This is captured by the notion of an adversary.

Definition 3 (Adversary). Given an MDP M = 〈S, ι,A, P, t,L〉 an adversary for M is a function σ : FPathM × A → [0, 1] such that for any finite path ρ ∈ FPathM, we have σ(ρ, a) > 0 only if a ∈ P(last(ρ)) and ∑a∈A σ(ρ, a) = 1.

We denote by AdvM the set of all adversaries for M. Note that when a choice of adversary σ is fixed, the nondeterminism in the MDP M is resolved, and we can describe the behaviour of the resulting system by a DTMC. We denote this DTMC byMσ (see, e.g., [Forejt et al., 2011] for details).

Probabilistic Swarm Systems. We now summarise the semantics of probabilistic parameterised interleaved interpreted systems (PPIISs). Here we will also follow the notation used in [Lomuscio and Pirovano, 2019].

A PPIIS is composed of an agent template, which defines the behaviour of one of the agents and an environment which gives the behaviour of the rest of the system.

Definition 4 (Probabilistic agent template). A probabilistic agent template is a tuple T = 〈S, ι, Act, P, t〉 where:

• The set S is a set of agent local states.
• ι ∈ S is a distinguished initial state.
• Act = A ∪ AE ∪ GS is the non-empty set of actions that can be performed by the agent. These may either be asynchronous actions, agent-environment actions or global-synchronous actions. Note the sets are disjoint, so each action only has one type. Each type of action gives a different communication pattern between the agents according Definition 6.
• The agent's protocol function P : S → P(Act) defines which actions are enabled at a given state.
• The agent's transition function t : S ×Act ×S → [0, 1] describes the evolution of the agent's state: given a local state s, an action a, and a local state s′ , t returns the probability that upon performing action a in state s the agent will transition to state s′ . Notice we require that for every l ∈ S, a ∈ P(l) we have ∑l′∈S t(l, a, l′ ) = 1.

The agent template can be seen as an MDP with additional labels on the actions for synchronisation purposes with other agents and the environment. The environment E = 〈SE, ιE,ActE, PE, tE〉 is similarly defined (see [Lomuscio and Pirovano, 2019] for details).

Definition 5 (PPIIS). A probabilistic parameterised interleaved interpreted system (PPIIS) is a tuple S = 〈T,E,L〉, where T is a probabilistic agent template, E is an environment and L : S × SE → P(AP) is a labelling function for a set of atomic propositions AP .

A PPIIS is an abstract description capturing an unbounded collection of concrete MDPs that are obtained by fixing a number of agents n ∈ Z+. We denote the agents by Agtn ≜ {1, . . . , n}. The instantiated, or concrete, MDPs have states, which we call global states, of the form g = 〈s1, . . . , sn, se〉 where s1, . . . , sn ∈ S and se ∈ SE. We denote by Sn the set of all such states, and use g.i to denote the state of agent i, and g.E to denote the state of the environment. The set of global actions is given by Actn ≜ GS ∪ AE ∪ ((A ∪ AE) × Agtn).

Definition 6 (Global protocol). The global protocol Pn : Sn → P(Actn) is defined by a ∈ Pn(g) if and only if one of the following holds:

• (Global-synchronous). (i) a ∈ GS; (ii) for all i ∈ Agtn, a ∈ P(g.i); (iii) a ∈ PE(g.E).
• (Asynchronous environment). (i) a ∈ AE; (ii) a ∈ PE(g.E).
• (Asynchronous agent). (i) a = (a′ , i) ∈ A×Agtn; (ii) a′ ∈ P(g.i).
• (Agent-environment). (i) a = (a′ , i) ∈ AE ×Agtn; (ii) a′ ∈ P(g.i); (iii) a′ ∈ PE(g.E).

Thus, global-synchronous actions must be enabled for all agents and the environment, asynchronous ones just for the agent or environment performing them, and agentenvironment ones for the environment and agent performing them. The restrictions above are intended to limit the undecidability of the resulting verification problem; they were originally introduced in [Kouvaros and Lomuscio, 2016] to study non-probabilistic systems.

We now define the global transition function, which describes the outcome of performing a global action.

Definition 7 (Global transition function). The global transition function tn : Sn × Actn × Sn → [0, 1] is defined by tn(g, a, g′ )

We can now define the MDP S(n) encoding the global behaviour of n agents and an environment.

Definition 8 (Concrete system). Given a PPIIS S and an n ∈ Z+, the concrete system of n agents is defined by S(n) = 〈Sn, ιn, Actn, Pn, tn, Ln〉, where ιn = 〈ι, . . . , ι, ιE〉, the labelling function Ln : Sn → P(AP × Agtn) is defined by Ln(g) ≜ {(p, i) ∈ AP ×Agtn : p ∈ L(g.i, g.E)}, and the other components are defined as in Definitions 6 and 7.

In [Lomuscio and Pirovano, 2019], it is observed that the concrete system is always a valid MDP. The properties we wish to check on this family of MDPs are expressed in a variant of PLTL [Forejt et al., 2011], which we define below.

Definition 9 (PLTL). For p ∈ AP and i ∈ Z+, the probabilistic LTL logic is defined by the following BNF:

We say a formula is m-indexed if it refers to agents with index at most m (i.e., any atomic proposition is of the form (p, i), where i ≤ m).

Definition 10 (Satisfaction). Given a concrete swarm system S(n) and φ an m-indexed formula, where n ≥ m, the satisfaction of φ on S(n) is inductively defined as follows:

Satisfaction for path formulae is defined as usual in LTL.

The parameterised model checking problem is concerned with checking whether a specification holds in concrete systems built on arbitrarily large number of agents.

Definition 11 (Parameterised Model Checking). Given a PPIIS S and an m-indexed PLTL formula φ, the parameterised model checking problem involves establishing whether it is the case that S(n) |= φ for all n ≥ m. We write S |= φ if this is the case.

Notice that this problem is a probabilistic extension of a problem that is known to be undecidable [Apt and Kozen, 1986]. Thus, it is also undecidable in general. However, a partial decision procedure was put forward for it in [Lomuscio and Pirovano, 2019].

3 Swarm Safety Analysis via Fault Injection

Parameterised model checking can be used to establish the correctness of, or establish bugs in a swarm protocol [Lomuscio and Pirovano, 2018]. However, certifying the absence of bugs is often not sufficient to guarantee safety of a swarm protocol nor to entirely understand the resulting run-time behaviour. For this, it is also important to establish the extent to which runtime malfunctions, or faults, affect the overall performance of the swarm. Some faults may break some overall swarm specifications; in other cases, the swarmmay actually be resilient to particular malfunctions. Understanding these weaknesses or strengths can inform designers and deployers.

To conduct a formal analysis of these aspects we construct a faulty PPIIS, S χ = 〈T χ ,E,Lχ 〉, from a non-faulty one S = 〈T,E,L〉 as follows. To model faults, we assume that the local states L of an agent are defined by a set of integer, Boolean, and enumerate (over a domain E) variables VAR = BV ar ∪ IV ar ∪ EV ar, i.e. L = (b : BV ar → {⊥,⊤}) × (i : IV ar → Z) × (e : EV ar → E). We denote by F the set of all possible faults. Various studies have been conducted in safety analysis to identify the faults normally of interest [Bozzano and Villafiorita, 2007]. We here consider the most widely used faults by assuming that F contains:

• For every x ∈ BV ar, a fault invert(x) that inverts the value of x and a fault setB(x, k) (where k ∈ {⊥,⊤}) that sets the value of x to k.
• For every y ∈ IV ar, a fault up(y) that increments the value of y, a fault down(y) that decrements the value of y, and a fault setI(y, k) (where k ∈ Z) that sets the value of y to k.

• For every z ∈ EV ar, a fault setE(z, v) (where v ∈ E) that sets the value of z to v.

More formally, F is given by:

Given a fault f ∈ F and a state s ∈ L, we will denote by (s)f the result of applying f to s. Formally:

where gx↦→y denotes the function obtained by replacing the value of g at x with y.

Having formalised the types of possible faults, we now define when they can occur and how likely they are. We encode this in the notion of a fault profile, which defines the probability of each fault occurring when performing a certain action from a certain state.

Definition 12 (Fault profile). A fault profile is a function χ : S×Act×(F ∪{✓}) → [0, 1]. The expression χ(s, a, f ) = p represents that when action a is performed from state s, there is a probability of p that fault f occurs. χ(s, a,✓) gives the probability of a fault not occurring when performing action a from state s. We assume that for all s ∈ S and a ∈ Act we have ∑f∈(F∪{✓}) χ(s, a, f ) = 1.

Note that the above restricts our swarms to having at most one fault at each time-step. We now define the behaviour of a faulty agent. This will augment the state of the agent with extra variables that allow us to write specifications involving whether the agent has exhibited faults.

Definition 13 (Faulty agent). Given an agent template T = 〈S, ι, Act, P, t〉 and a fault profile χ : S×Act×(F∪{✓}) → [0, 1], we define a faulty agent template T χ = 〈Sχ , ιχ ,Act, P χ , tχ 〉 as follows:

• Sχ = S × {⊥,⊤} × {⊥,⊤}, where the first Boolean variable encodes whether the agent has ever exhibited a fault and the second whether the agent exhibited a fault in the previous transition.
• ιχ = (ι,⊥,⊥) is a new initial state,
• P χ : Sχ → P(Act) is given by P χ ((s, f, i)) ≜ P(s).
• tχ : Sχ ×Act ×Sχ → [0, 1] is defined by:

The definition above includes both non-faulty transitions (corresponding to i′ = ⊥) in which the value of f is not affected, and faulty transitions (i′ = ⊤) in which f is set to ⊤. Note that transitions where f = ⊤ and f ′ = ⊥ are not allowed; so once an agent has exhibited faulty behaviour, it is labelled as faulty for the rest of the run of the system. However, faulty agents may still carry out correct transitions.

Observe that faulty agents are well-defined agents.

Observation 1. Let χ : S × Act × (F ∪ {✓}) → [0, 1] be a fault profile and T = 〈S, ι,Act, P, t〉 a non-faulty agent. Then, it is the case that for any l = (s, f, i) ∈ Sχ and a ∈ Act we have ∑l′∈Sχ tχ (l, a, l′ ) = 1.

We can now define faulty swarm systems.

Definition 14 (Fully Faulty Swarm System). Given a fault profile χ : S × Act × (F ∪ {✓}) → [0, 1] and a nonfaulty PPIIS S = 〈T,E,L〉, the (fully) faulty PPIIS S χ = 〈T χ , E, Lχ 〉 is constructed by taking T χ as in Definition 13, and Lχ : Sχ ×SE → P(AP ∪{faulty, injected}) defined:

Notice that the environment does not exhibit any faults. We add two additional atomic propositions to the language: faulty and injected, tracking whether an agent has ever exhibited faulty behaviour and whether it exhibited faulty behaviour at the previous time step, respectively. These atomic propositions allow us to express a number of specifications such as:

which expresses that the probability of an agent ever exhibiting a fault does not exceed 0.5.

We can also express probabilistic variants of properties often considered in fault-tolerance literature. For instance:

expresses that with high probability even if an agent exhibits a fault the swarm can still satisfy φ at some point in the future. This expresses a notion of resilience of the agents in the swarm w.r.t. the faults and the specification φ. Note that φ may depend on the state of other agents or the environment, and thus can express a property of the whole swarm system rather than just of agent 0.

Finally, the new atomic propositions allow us to limit specifications to agents which have not exhibited faulty behaviour. For instance:

expresses that with high probability whenever an agent is not faulty, the agent can satisfy the formula φ.

4 Model Checking Faulty PPIIS

In this section we define and solve the parameterised faulttolerance problem which concerns assessing whether a probabilistic swarm is resilient w.r.t. possible faults given as above. Before doing so, we extend the notion of swarm systems of the previous section by introducing a probability that an agent may be faulty.

Definition 15 (Probabilistically Faulty Swarm System). Given a PIIS S = 〈T,E,L〉, a fault profile χ : S × Act × (F ∪ {✓}) → [0, 1] and a faultiness probability p ∈ [0, 1], we define the probabilistically faulty swarm system S χ p = 〈T χ p ,Eχ p , Lχp 〉 as follows.

The faulty agent template T χ p = 〈Sχ p , ιχp , Actχp , P χ p , tχp 〉 is given by:

• Sχ p = S∪Sχ∪{ιχp , ιf , ι′f , ιn, ι′n }, defined by considering all the faulty and non-faulty states, as well as five fresh states used for initialisation below.
• ιχp , the new initial state.
• Actχp = Act ∪ {init, g, g′ } where init ∈ A and g, g′ ∈ GS, defined by introducing a fresh asynchronous action init and fresh global-synchronous actions g and g′ , used for initialisation.
• P χ p : Sχ p → P(Actχp ) is given by:

• tχp : Sχ p ×Actχp ×Sχ p → [0, 1] is given by:

The environment Eχ p = 〈Sχ p,E , ιχp,E , Actχp,E , P χ p,E , tχp,E 〉 is defined by:

• Sχ p,E = SE ∪ {ιχp,E , ι′ }, defined by adding two states to SE used for initialisation.
• ιχp,E , the new initial state.
• Actχp,E = ActE ∪ {g, g′ } where g, g′ ∈ GS, defined by adding two fresh global-synchronous actions.
• P χ p,E : Sχ p,E → P(Actχp,E ) is given by:

• tχp,E : Sχ p,E × Actχp,E × Sχ p,E → [0, 1] is given by:

The valuation function Lχp : Sχ p × Sχ p,E → P(AP ∪ {starting, faulty, injected}) is defined by:

Intuitively, the original swarm is extended with an initialisation phase where each agent asynchronously uses the init action to determine whether it will be faulty with probability p. Following this, the global-synchronous action g takes the system to a state where our new atomic proposition starting holds. Finally, the global-synchronous action g′ starts the system. This initialisation process is depicted in Figure 1. Note that the definition above results in a valid PPIIS.

Observation 2. Consider a PIIS S = 〈T,E,L〉, a fault profile χ : S × Act × (F ∪ {✓}) → [0, 1] and a faultiness probability p ∈ [0, 1]. Then, we have that ∑l′∈Sχ p tχp (l, a, l′ ) = 1 for all l ∈ Sχ p and a ∈ Actχp . We also have ∑l′E ∈Sχ p,E tχp,E (lE, aE, l′E ) = 1 for all lE ∈ Sχ p,E and aE ∈ Actχp,E .

We are interested in assessing whether an unbounded probabilistic swarm is resilient w.r.t. a specification when subjected to probabilistically faulty agents. To do so, we formulate the following decision problem.

Definition 16 (PFTP). Given a PIIS S, a PLTL formula φ = P max/min ▷◁x [ψ], a fault profile χ, and a p ∈ [0, 1], the parameterised fault-tolerance problem (PFTP) concerns answering the parameterised model checking problem (Definition 11) for S χ p |= P max/min ▷◁x [G((starting, 0) → Xψ)]. If this holds, we write S |=χp φ.

Definition 16 allows us to recast the PFTP via a simpler parameterised model checking query for the amended swarm system under a revised specification.

Given the above, we can introduce a simple procedure for checking the PFTP. This is presented in Algorithm 1. Note that the decision problem of line 2 can be resolved with tools for verification of probabilistic swarms [Lomuscio and Pirovano, 2019]. Note also that the procedure is incomplete, as the query on line 2 may not terminate. As we will see in the next section a number of concrete swarm protocols can effectively be checked irrespective of the theoretical undecidability of the underlying problem.

5 Implementation and Evaluation

We implemented the method described in the previous sections in a Java toolkit called PSV-F (Probabilistic Swarm Verifier for Faulty systems), built on top of PSV-CA [Lomuscio and Pirovano, 2019], which in turn uses PRISM 4.0 [Kwiatkowska et al., 2011] as its underlying probabilistic model checker. The source code for this and the model we consider below are released as open-source [PSV-F, 2020].

Like PSV-CA, our toolkit takes in a swarm file describing the behaviour of agents and the environment, and a file describing the specifications to check. In addition, PSV-F takes as input a file containing the list of faults that may occur in the system along with their relative conditions (actions being performed, states of the agent, and fault probabilities).

Upon invocation, PSV-F incorporates the faults into the model and invokes PSV-CA to verify the desired specification. Note that since the underlying decision procedure is partial, this call in principle may not receive an answer.

To evaluate the usefulness of our tool we consider the swarm foraging protocol [Campo and Dorigo, 2007; Liu and Winfield, 2010] that has previously been verified in a probabilistic setting without any faults in [Lomuscio and Pirovano, 2019]. We extend this analysis to introduce a fault.

The protocol has agents in four possible states: resting in a nest, searching for food, reaching some food, and returning to the nest with food. Resting robots may decide with probability 0.5 to begin searching for food. Robots searching for food may find some with probability 0.3. After two time-steps of failed searching, the robot goes back to resting. If a robot locates food, it moves towards it, picks it up, brings it back to the nest, then goes back to resting.

We inject one fault into the system encoding the fact that whenever a robot tries to move and is carrying food, it may drop the food with some probability pf . If it does this, it will return to the nest with no food. As in the original analysis we check the specification pattern P max ≤p [F <k deposited2 ], where deposited2 is an atomic proposition that holds if at least two units of food have been deposited in the nest and k is a parameter indicating the number of steps. The specification bounds the maximum probability p with which the agents can deposit at least two units of food within k time-steps.

Intuitively the probability p depends on the fault probability pf . By using PSV-F we can ascertain this relation precisely; importantly this analysis holds for any number of agents in the system as the analysis is based on parameterised model checking. We conducted this analysis and recorded in Figure 2 the maximum p for which the property holds for different values of k and pf . The abstraction that PSV-CA generated had 2×106 states and 46×106 transitions. Injecting the faults was instantaneous, constructing the model took approximately 400 seconds and the specification was checked in approximately 5 seconds.

By analysing the results obtained, we deduce that the higher the probability of the fault, the lower the probability of success of the protocol. However, even systems with faulty agents can achieve the objective with high probability as long as sufficient time-steps are considered. Note also that, as expected, if pf = 1 (i.e., agents always drop the food they are holding upon moving), then the goal is never achieved. The analysis above allows us to conclude that the foraging protocol displays a degree of resilience against the fault considered. This, however, decreases when the probability of faults increases. Note that, while these results are in line with our intuition, they could not previously be obtained formally.

6 Conclusions

We have introduced a method for injecting faults into probabilistic swarm systems and presented an implementation built from an existing toolkit for verifying such systems. To the best of our knowledge, this gives the first method and toolkit that enables the assessment of resilience to faults of swarm systems that are unbounded in size. We used these to assess the resilience of a foraging protocol; other protocols are likely to be analysable in a similar way. Another possible extension we have not pursued here is to consider more than one fault occurring at each time-step. We leave this for future work.

Acknowledgements

Alessio Lomuscio is supported by a Royal Academy of Engineering Chair in Emerging Technologies.