Symbolic Synthesis of Fault-Tolerance Ratios in Parameterised Multi-Agent Systems

1 Introduction

A key criterion when assessing protocols in multi-agent systems (MAS) is establishing their correctness against a set of specifications. While important, this is often not sufficient for deployment in several scenarios of practical significance. Even if a protocol can be shown to be demonstrably correct, the designer has no information on the impact of possible faults and malfunctions at runtime. This is of importance in large MAS where the individual risk of failure is high, as is the case in robotic swarms [Winfield et al., 2005].

It is therefore of interest not just to establish correctness, but the degree of fault-tolerance of a protocol with respect to possible faults in the system. In the case of MAS composed of a fixed number of agents known at design time, techniques inspired by safety-analysis [Bozzano and Villafiorita, 2007], allow the engineer to study the consequences of a variety of faults against specifications of interest [Ezekiel and Lomuscio, 2009; 2017]. For example in [Ezekiel et al., 2011] the resilience of an autonomous submarine AUTOSUB6000 against possible faults was assessed in this manner.

Often, however, the number of agents constituting a MAS is not known in advance, or indeed changes at runtime. This is the case in several areas of artificial intelligence including robotic swarms for monitoring or repair, auctions, etc. In these cases, it is useful to determine the maximal ratio of faulty agents (as a proportion of the whole population) that the protocol can tolerate against some specification. For example, in a flocking protocol we may be interested in the percentage of drones that need to be faulty for the rest of the swarm to lose its ability to fly in formation [Kouvaros and Lomuscio, 2017]. Determining this ratio can have significant consequences on engineering aspects of the system.

Under general conditions, determining this ratio is undecidable [Apt and Kozen, 1986]. In [Kouvaros and Lomuscio, 2017], a method for checking a class of systems of interest against a given ratio of faults is put forward. This induces a procedure for calculating an approximation of the ratio. However, this calculation rests on model checking systems of varying sizes and is therefore computationally expensive and often entirely impractical. In this paper we develop a novel technique to derive the fault tolerance ratio symbolically. The ratio, as we explain, is incorporated into a model that encodes various combinations of faulty and correct agents operating at runtime. This symbolic calculation, which amounts to solving a version of the parameterised model checking (PMC) problem [Kouvaros and Lomuscio, 2016] in combination with a generalised model checking algorithm, enables us to synthesise the ratio as a one-shot procedure.

Related work. The PMC problem has been extensively studied [Bloem et al., 2015]. More recently, it has also been used to study fault tolerance in distributed algorithms [Aminof et al., 2018; John et al., 2013; Zhang et al., 2009]. However, these approaches either are not amenable to analysing MAS (due to, for instance, a lack of epistemic specifications) or do not tackle the issue we tackle here of finding the ratio of faulty to non-faulty components.

The rest of the paper is organised as follows. In Section 2 we fix the notation and introduce the parameterised semantics upon which the framework is developed. In Section 3 we present a generalised model checking procedure which can be used to synthesise the ratio of faulty agents in a MAS of a fixed number of agents. We build on this in Section 4 where, by combining this with results in parameterised model checking, we derive a provably sound procedure for MAS of arbitrary size. We present an implementation of the technique in Section 5 and report on its use on transport and aggregation protocols for swarm systems. We conclude in Section 6.

2 Background

Models. Parameterised interleaved interpreted systems (PIISs) give a model to reason about MAS composed of an unbounded number of agents by extending interleaved interpreted systems (IIS) [Lomuscio et al., 2010]. The presentation here follows that in [Kouvaros and Lomuscio, 2017]. A PIIS is made up of an agent template, which describes the behaviour of individual agents and an environment which captures the rest of the state of the system. The framework can accommodate a finite number of different agent templates, but for simplicity we present the definitions with just one.

The agent template T = 〈L, ι,Act, P, t〉 defines a finite, non-empty set of local agent states L together with a distinguished initial state ι ∈ L. The non-empty set Act = A ∪ AE ∪ GS gives the actions that can be performed by the agents, which are either asynchronous actions, agentenvironment actions or global-synchronous actions. Each type of action gives a different communication pattern between the agents, as outlined in Definition 2. The actions are performed in compliance with a protocol P : L → P(Act) that defines which actions are enabled in each state. The agent's transition function t : L × Act → L describes the evolution of the agent's state: given its local state and the action performed, it returns its new local state.

Similarly, the environment e = 〈Le, ιe,Acte, Pe, te〉 defines a finite, non-empty set of local states Le, a distinguished initial state ιe ∈ Le, a non-empty set of actions Acte = Ae ∪ AE ∪ GS, a protocol Pe : Le → P(Acte), and a transition function te : Le ×Acte → Le.

Definition 1 (PIIS). A parameterised interleaved interpreted system is a tuple S = 〈T, e, V〉, where V : L → 2AP is a labelling function on the agent template's states for a set AP of atomic propositions.

Each PIIS describes an unbounded collection of concrete systems obtained by choosing different numbers of agents in the system. Given a PIIS S and n ∈ Z+ the IIS S(n) of n agents is the result of the composition of n copies of T with the environment. We denote the set of concrete agents instantiated from T by A = {1, . . . , n}. A global state g = 〈l1, . . . , ln, le〉 is a tuple of local states for all the agents and the environment in S(n); it describes the system at a particular instant of time. For a global state g we write g.i to denote the local state of agent i in g and g.e to denote the state of the environment in g. The system's global states evolve over time in compliance with the global transition relation.

Definition 2 (Global transition relation). The global transition relation R ⊆ G × Act ∪ Acte × G on a set G of global states is defined as (g, a, g′ ) ∈ R iff one of the following holds:

• (Asynchronous). (i) a ∈ A∪Ae; (ii) there is i ∈ A∪{e} s.t. a ∈ P(g.i) and t(g.i, a) = g′ .i; (iii) for all j ̸= i, g.j = g′ .j.
• (Agent-environment). (i) a ∈ AE; (ii) there is i ∈ A s.t. a ∈ P(g.i) and t(g.i, a) = g′ .i; (iii) a ∈ Pe(g.e) and te(g.e, a) = g′ .e; (iv) for all j ̸= i, j ̸= e, g.j = g′ .j.
• (Global-synchronous). (i) a ∈ GS; (ii) for all i ∈ A, a ∈ P(g.i) and t(g.i, a) = g′ .i; (iii) a ∈ Pe(g.e) and te(g.e, a) = g′ .e.

We sometimes write g → g′ for ∃a: (g, a, g′ ) ∈ R.

Above R defines precisely one action to be performed at each time step. If this is an asynchronous action, then exactly one agent participates in the global transition; if it is an agent-environment action, then exactly one agent and the environment participate in the global transition; if it is a globalsynchronous action, then all the agents and the environment participate in the global transition.

Having defined the global transition relation, we can proceed to give the concrete semantics describing the behaviour of a system S(n) composed of n agents and an environment.

Definition 3 (Concrete semantics). Given a PIIS S and n ∈ Z+, the IIS S(n) is a tuple S(n) = 〈G, g0,R, V 〉, where G ⊆ Ln × Le is the set of reachable global states via R from the initial global state g0 = 〈ι, . . . , ι, ιe〉, and V : G → 2AP×A is the labelling function on the global states defined by (p, i) ∈ V (g) iff p ∈ V(g.i), for each p ∈ AP, i ∈ A, where AP is a finite set of atomic propositions.

Notice that for each atomic proposition p we create a copy for each of the n agents and label a global state with (p, i) if the agent i is at a local state labelled with p by the template labelling function.

A path π is an infinite sequence π = g0a0 g1a1 g2 . . . such that (gi , ai , gi+1 ) ∈ R for every i ≥ 0. We write π(i) for the i-th state in π. The set of all paths originating from a state g is denoted by Π(g).

Specifications. We now define the logic ICTLK\X which extends the temporal-epistemic logic CTLK without the next time operator by introducing indexed atomic propositions and indexed epistemic modalities that are quantified over the concrete agents [Kouvaros and Lomuscio, 2016]. Given a set IND of indices, a set AP of atomic propositions, ICTLK\X formulae are defined by the following BNF grammar:

where p ∈ AP and v ∈ IND. The epistemic modality Kiφ is read as "agent i regards φ as being epistemically possible". The temporal modality E(φ1Uφ2) denotes "for some path, at some point φ2 holds and before then φ1 is true along the path"; and EG(φ) denotes "for some path, φ holds at every state". We also use standard CTL abbreviations such as Fφ ≡ true Uφ. The universal quantifier allows us to express properties irrespective of the number of agents in the system. An ICTLK\X formula is said to be a sentence if every variable appearing the formula is in the scope of a universal quantifier. Hereafter we consider only sentences.

Definition 4 (Satisfaction of ICTLK\X). The satisfaction relation |= for an IIS S(n), and an ICTLK\X sentence φ is inductively defined as follows (the clauses for the atomic propositions and the Boolean operators are omitted):

(S(n), g) |= E(φ1Uφ2) iff

(S(n), g) |= EGφ

(S(n), g) |=Kiφ

• for some π ∈ Π(g), for some i ≥ 0 (S(n), π(i)) |= φ2 and for all 0 ≤ j < i, (S(n), π(j)) |= φ1;
• iff for some π ∈ Π(g), for all i ≥ 0, (S(n), π(i)) |= φ;

iff for some g′ ∈ G with g.i = g′ .i it is the case that (S(n), g′ ) |= φ;

Notice that, since all agents are behaviourally identical, the evaluation of a universally quantified formula is equivalent to the evaluation of only one of its ground instantiations, where the variables in an instantiation are mapped to different agents [Kouvaros and Lomuscio, 2016]. Hereafter, we will only consider such ground instantiations.

Two fragments of this logic are important for our purposes: the existential fragment ECTLK\X is obtained by restricting negation to only being applied to propositions, i.e. replacing ¬φ by ¬(p, v) in the syntax. The dual universal fragment ACTLK\X is the negation of this fragment, i.e. the language {¬φ | φ ∈ ECTLK \ X}.

Our specifications will be expressed in ACTLK\X. A formula φ is said to be true in S(n), denoted S(n) |= φ, if (S(n), g0) |= φ. We will use a definition of cutoffs similar to that given in [Kouvaros and Lomuscio, 2013b].

Definition 5 (Cutoff). An integer c ∈ Z+ is said to be a cutoff for a PIIS S if for all ACTLK\X formulas φ we have that S(c) |= φ implies S(n) |= φ for all n ≥ c.

Faults. We will assume that a faulty PIIS S f = 〈(T, T f ), ef , V f 〉 can be constructed from a given PIIS S = 〈T, e, V 〉 according to the faults we wish to consider. The full details of the faults that can be considered and how the corresponding faulty PIIS is constructed are omitted for space and can be found in [Kouvaros and Lomuscio, 2017]. The faulty PIIS S f is constructed from the non-faulty PIIS S by adding a second agent template T f that may, in addition to performing all the behaviours T performs, also perform certain faulty behaviours. The environment is modified suitably for synchronisation purposes and the valuation function is extended to label states with a new atomic proposition faulty that holds in agent i's local state precisely if agent i has exhibited faulty behaviour at some point in the past. We denote by S f ((nn, nf )) the concrete system with nn non-faulty agents and nf faulty ones instantiated from T and T f respectively. Also note that formulae are evaluated on a faulty PIIS by quantifying only over non-faulty agents.

3 Ratio Synthesis

As a stepping stone to parameterised fault tolerance, we now define the notion of fault tolerance for concrete MAS of a fixed size.

Definition 6 (Fault Tolerance). Given a faulty PIIS S f , a ratio λ ∈ [0, 1], an integer n ∈ Z+ and an ACTLK\X formula φ, we say that size n instances of S f are λ-tolerant with respect to φ if it is the case that:

If this is the case we write S f |=λn φ.

Intuitively, the above definition says that if a proportion up to λ of the n agents exhibit faulty behaviour then the specification φ is satisfied. In what follows we are concerned with finding how tolerant a system is to faults with respect to a specification. We formalise this decision problem as follows.

1: procedure λ-SYNTHESIS( S f , φ, n ) 2: X←Lambda(S f ((0, n)), ¬φ); 3: if ∃ρ : (g0, ρ) ∈ X then 4: return min {ρ ∈ [0, 1] | (g0, ρ) ∈ X}; 5: else 6: return total; 7: end if 8: end procedure

Definition 7 (λ-synthesis). Given a faulty PIIS S f , an integer n ∈ Z+ and an ACTLK\X formula φ, find λ ∈ [0, 1] such that S f ̸|=λn φ andS f |=λ′ n φ whenever λ′ < λ, or return total if no such λ exists (i.e. the specification is always satisfied).

Our approach is loosely inspired by the procedures for parameter synthesis used in biological modelling [Beneˇs et al., 2016; Barnat et al., 2012] but with important adaptations for our setting of fault tolerance in multi-agents systems. Our procedure, shown in Algorithm 1, passes the system of n faulty agents and the negation of our specification to a subprocedure Lambda, shown in Algorithm 2.

This sub-procedure works similarly to the labelling algorithm for model checking CTL [Clarke et al., 1999]. The algorithm recursively labels the states of a system with the subformulas of the specification under question that they satisfy. Differently from the CTL labelling algorithm, Lambda labels states with both said subformulas and the minimum ratio of faulty agents to total agents that is sufficient for the specification to be satisfied at the state. Thus, Lambda operates on sets of pairs of states and ratios instead of sets of states. Note that since Lambda takes as input the negation of an ACTLK\X formula, the procedure is defined for the existential fragment ECTLK\X of CTLK\X.

We now give some preliminary definitions that we will use in our procedure. For a global state g we use λ(g) to denote the ratio of agents that have exhibited a fault to total agents, i.e.

Given a set of global states X we use ratio(X) to denote the minimum ratio of faulty agents in a state in X. Formally:

For a set X ∈ G × [0, 1] we sometimes simply write X for the projection of X on the states. Formally:

Given X let pre∃(X) denote the pre-image of X defined as:

where next(g) ≜ {g ′ | g → g ′ } expresses the set of successor states of g and pre∃(X) ≜ {g | ∃g′ : g → g′ ∧ g′ ∈ X} denotes the preimage of a set of states X.

Algorithm 2 Labelling Procedure

1: procedure LAMBDA( Sf ((0, n)), φ ) 2: case φ 3: (p, ag) : return {(g, λ(g)) | (p, ag) ∈ V (g)}. 4: ¬(p, ag) : return {(g, λ(g)) | (p, ag) /∈ V (g)}. 5: φ1 ∧ φ2 : return X where (g, ρ) ∈ X iff there are ρ′ and ρ′′ such that (g, ρ′ ) ∈ Lambda(Sf ((0, n)), φ1), (g, ρ′′ ) ∈ Lambda(Sf ((0, n)), φ2) and ρ = max(ρ′ , ρ′′ ). 6: φ1 ∨ φ2 : return X where (g, ρ) ∈ X iff (g, ρ′ ) ∈ Lambda(Sf ((0, n)), φ1) or (g, ρ′′ ) ∈ Lambda(Sf ((0, n)), φ2), for some ρ′ , ρ′′ with ρ = min(ρ′ , ρ′′ ). 7: Kiψ : return LambdaK (Sf ((0, n)), i, ψ). 8: E(φ1Uφ2) : 9: return LambdaEU (Sf ((0, n)), φ1, φ2). 10: EGψ : return LambdaEG(Sf ((0, n)), ψ). 11: end case 12: end procedure 13: procedure LAMBDAK ( Sf ((0, n)), i, φ ) 14: X←Lambda(Sf ((0, n)), φ); 15: return {(g, ρ) ∈ G× [0, 1] | ∃g′ ∈ X : g.i = g′ .i ∧ ρ = ratio({g′ ∈ X | g.i = g′ .i})}. 16: end procedure 17: procedure LAMBDAEU( Sf ((0, n)), φ1, φ2 ) 18: X←Lambda(Sf ((0, n)), φ1); 19: Y←G×{0}; 20: Z←Lambda(Sf ((0, n)), φ2); 21: while Y ̸= Z do 22: Y ← Z; 23: Z ← Z ∪ {(g, ρ) ∈ G× [0, 1] | ∃ρ′ , ρ′′ ∈ [0, 1] : (g, ρ′ ) ∈ pre∃(Z) ∧ (g, ρ′′ ) ∈ X ∧ ρ = max(ρ′ , ρ′′ )}. 24: end while 25: return Z; 26: end procedure 27: procedure LAMBDAEG( Sf ((0, n)), φ ) 28: X←G×{0}; 29: Y←Lambda(Sf ((0, n)), φ); 30: while X ̸= Y do 31: X ← Y; 32: Y ← {(g, ρ) ∈ Y × [0, 1] | ∃ρ′ , ρ′′ ∈ [0, 1] : (g, ρ′ ) ∈ pre∃(Y) ∧ (g, ρ′′ ) ∈ Y ∧ ρ = max(ρ′ , ρ′′ )}. 33: end while 34: return Y; 35: end procedure

We now describe the Lambda procedure. The propositional cases are trivial: we can simply label each state which satisfies or does not satisfy the atomic proposition with the ratio of faulty agents at that state. For the conjunction case, notice we need both φ1 and φ2 to hold so the minimum necessary ratio of faults is the largest of the ratios for each of these two to hold. The disjunction case is similar.

For the epistemic modality case, notice we need at least one epistemic successor to satisfy φ so we take the minimum ratio for this to be the case.

For the φ1Uφ2 case, we use a set Z that begins with the states satisfying φ2 and the fault ratios under which this is the case. Then, we add predecessors of this set that satisfy φ1 and label them with the maximum of the ratio needed to ensure they satisfy φ1 and the least ratio needed to ensure a successor satisfies φ2. This is repeated until a fixed point is reached.

For the EGφ case, we begin by finding all the states satisfying φ and labelling them with the ratio needed for this to be the case. Then, we repeatedly reduce this set to include only those states that can reach a successor within the set and possibly increase the label of the state if all the successors have a higher label than it does. This is repeated until a fixed point is reached.

We now show that the output of λ-SYNTHESIS reflects the minimum ratio for which the Fault Tolerance problem would return false w.r.t the concrete system and specification given as input. We prove this by means of two steps.

Theorem 1. Let λ = λ-SYNTHESIS(S f , φ, n) ̸= total for a faulty PIIS S f and an ACTLK\X formula φ. Then S f ̸|=λn φ.

Proof sketch. By definition of λ-SYNTHESIS and an adaptation of the proof for the CTL labelling algorithm [Clarke et al., 1999], we have that ¬φ is satisfied in the submodel of S f ((0, n)) built only from states in which the ratio of agents exhibiting faults is less than or equal to λ. Consequently, we have S f ̸|=λn φ.

Before proceeding with the next part of the proof, we show some intermediate results. Denote by G the set of global states of S f ((0, n)) and G′ the set of global states of S f ((nn, nf )). Refer to the agents in S f ((0, n)) by A and to the agents in S f ((nn, nf )) by A′ .

Definition 8. A bijection ξ : A ↦→ A′ is fault-preserving at some global state g ∈ G iff every agent i ∈ A that has never exhibited a fault in state g is mapped to a non-faulty agent ξ(i) ∈ A′ .

We define a global state g ∈ G and a global state g′ ∈ G′ to be similar, denoted g′ ≈ g, iff there is some fault-preserving bijection ξ such that for every i ∈ A it is the case that g.i = g′ .ξ(i), i.e. every agent is in the same local state as the agent it is mapped to.

Definition 9. A simulation relation ⊏⊆ G′ ×G is defined by g′ ⊏ g iff:

• g′ ≈ g
• For every path π′ in S f ((nn, nf)) there is a path π in S f ((0, n)) such that π′ (i) ⊏ π(i) for every i ≥ 0.
• For every g′1 with g′ .i = g′1 .i there is a g1 with g.i = g1 .i and g′1 ⊏ g1 .

Lemma 1. If g′ ≈ g then g′ ⊏ g.

Proof sketch. The proof idea is to let each faulty agent i in S f ((0, n)) mimic the agent ξ(i) in S f ((nn, nf )).

We can now proceed to prove the second part of the correctness of the λ-SYNTHESIS procedure.

Theorem 2. Let λ = λ-SYNTHESIS(S f , φ, n) ̸= total for a faulty PIIS S f and an ACTLK\X formula φ. Then for all λ′ < λ we have that S f |=λ′ n φ.

Proof sketch. Let nn, nf ∈ Z be such that nn + nf = n and nf /n = λ′ < λ. We need to show that S f ((nn, nf )) |= φ.

Let label (ψ) denote the set of minimal labels computed by Lambda(S f ((0, n)), ψ). We show, by structural induction on ψ, that g′ ⊏ g∧∃ρ : (g, ρ) ∈ label (¬ψ) implies either one of the following: g′ |= ¬ψ, if ψ is a propositional formula; g′ |= ψ, if ψ is not propositional. Then, we can apply this to the initial states with ρ = λ to get our result. The propositional and boolean cases are straightforward. The temporal cases follow from the existentiality of ψ and Lemma 1.

We show the case of ψ = Kiψ′ . We have (g, ρ) ∈ label(Ki¬ψ′ ). We need to show that g′ |= Kiψ. Suppose g′ ̸|= Kiψ. Then, there is a state g′1 with g′ .i = g′1 .i and g′1 |= ¬ψ. By Lemma 1 there is a state g1 in S f (n) with g′1 ⊏ g1 , ratio(g 1 ) = ratio(g ′1 ) ≤ λ′ < λ and g1 |= ¬ψ. Therefore ∃ρ: (g1 , ρ) ∈ label (¬ψ). Since ratio(g 1 ) < λ the latter contradicts that λ is minimum.

Together, Theorem 1 and Theorem 2 show that Algorithm 1 is a sound decision procedure for the λ-synthesis problem.

4 Parameterised Ratio Synthesis

We now introduce a notion of parameterised fault tolerance similar to that in [Kouvaros and Lomuscio, 2017], but, instead of checking a system with a given ratio of faults against a specification, we here determine the minimum ratio of faults for the specification to be violated.

Definition 10 (Parameterised Fault Tolerance). Given a faulty PIIS S f , a ratio λ ∈ [0, 1], and an ACTLK\X formula φ, we say that S f is λ-tolerant with respect to φ if it is the case that S f |=λx φ for all x ∈ Z+. We denote this by S f |=λ φ.

We wish to synthesize the least λ that falsifies a specification, which we formalise in the decision problem below.

Definition 11 (Parameterised λ-synthesis). Given a faulty PIIS S f and an ACTLK\X formula φ, find λ ∈ [0, 1] such that S f ̸|=λ φ and S f |=λ′ φ whenever λ′ < λ or return total if no such λ exists (i.e. the specification is always satisfied).

Instead of tacking this problem directly, we consider a discrete version of it.

Definition 12 (Discrete Parameterised λ-synthesis). Given a faulty PIIS S f , an ACTLK\X formula φ and a discretisation step d ∈ Z+, find the solution to parameterised λ-synthesis to within 1/d.

Notice that a complete decision procedure for this problem cannot exist, as this would give a decision procedure for the parameterised model checking problem, which is known to be undecidable [Apt and Kozen, 1986]. Nonetheless, as for the parameterised model checking problem, it is of interest to explore decidable fragments [Emerson and Namjoshi, 1995; Kouvaros and Lomuscio, 2016]. We do this in the procedure shown in Algorithm 3.

The procedure takes as input the faulty PIIS S f and the step d and then calls a cutoff identification procedure [Kouvaros and Lomuscio, 2013a; 2013b; 2015] to identify a cutoff c for the system composed solely of faulty agents, i.e., the

Algorithm 3 Parameterised λ-Synthesis Decision Procedure

• 1: procedure P-λ-SYNTHESIS( S f , φ, d ) 2: Identify a cutoff c for 〈T f , ef , V f 〉 or return fail; 3: m← total; 4: for n← 1 to max(d, c) do 5: m←min(m, λ-SYNTHESIS(S f , φ, n)); where we define min(total, x) = x 6: end for 7: return m;
• 8: end procedure

PIIS 〈T f , ef , V f 〉. Since cutoffs do not exist in general, by necessity the cited identification procedures are incomplete. In the case a cutoff cannot be identified, then our procedure fails. In the case a cutoff is identified, then our procedure calls the λ-SYNTHESIS procedure on each concrete instance up to the maximum of the cutoff and the discretisation step and returns the minimum result of these calls. We aim to prove that, to within 1/d, this is the least ratio for which φ is falsified. As in the previous section, we do this in two steps.

Theorem 3. Let λ = P-λ-SYNTHESIS(Sf , φ, d) ̸= total for a faulty PIIS S f , an ACTLK\X formula φ and a discretisation step d ∈ Z+. Then S f ̸|=λ φ.

Proof. Note that for some n it is the case that Sf ̸|=λn φ by the correctness of λ-SYNTHESIS. The result follows immediately.

Theorem 4. Let λ = P-λ-SYNTHESIS(Sf , φ, d) ̸= total for a faulty PIIS S f , an ACTLK\X formula φ and a discretisation step d ∈ Z+. Then for all λ′ < λ - (1/d) we have that S f |=λ′ φ.

Proof sketch. Let nn + nf = n with nf/n = λ′ < λ. We need to show S f ((nn, nf )) |= φ.

Denote by c the cutoff for 〈T f , ef , V f 〉. The cases where n ≤ max(d, c) follow directly from the correctness of λ-SYNTHESIS. So, it remains to consider when n > max(d, c). Suppose for a contradiction S f ((nn, nf )) |= ¬φ. Then, the initial state of S f ((0, n)) would be labelled with some λ′′ ≤ λ′ < λ by Lambda(S f ((0, n)), ¬φ). Now consider the PIIS Sλ′′ which is a restriction of 〈T f , ef , V f 〉 to allow at most a ratio of λ′′ faulty agents. By the labelling algorithm we have that Sλ′′ (n) |= ¬φ. Notice that max(d, c) is also a cutoff for Sλ′′ so it follows from this that Sλ′′ (max(d, c)) |= ¬φ. But now we have S f |=λ′′ max(d,c) φ for λ′′ < λ-(1/d), contradicting the minimality of the return value for λ-SYNTHESIS(S f , φ,max(d, c)).

Together, Theorem 3 and Theorem 4 show that Algorithm 3 is a sound decision procedure for the discrete parameterised λ-synthesis problem.

5 Evaluation

We implemented our algorithms in MCMAS-PFTS, a toolkit constructed from MCMAS-P, a model checker for the verification of PIIS [Kouvaros and Lomuscio, 2013b]. The tool takes as input a description of the agent template and the faults to be injected. It then constructs the faulty agent, using the procedures detailed in [Kouvaros and Lomuscio, 2017].

We used MCMAS-PFTS to assess the fault-tolerance of the train-gate-controller, a commonly used benchmark for the verification of MAS, and transport and aggregation protocols in robot swarms. For simplicity, we took the discretisation step to be equal to the cutoff in every case. We are not aware of any other approaches for computing the fault-tolerance ratio of a MAS but to compare the run time of our synthesis approach to a benchmark, we compare it to the run time of the the na¨ıve approach of iteratively checking concrete systems for all possible ratios of faulty to non-faulty agents using the techniques in [Kouvaros and Lomuscio, 2017]. Our results are summarised in Table 1.

Train-Gate-Controller. We modelled the train-gatecontroller example from [van der Hoek and Wooldridge, 2002] in which arbitrarily many trains are trying to pass through a tunnel. A controller needs to ensure that only one is present in the tunnel at any given time. We modelled the fault representing that a train might remain stuck in the tunnel when it should have left and checked the property "if a train is in the tunnel, it knows no other train is," expressed in ACTLK\X as

We found a cutoff of 3, giving us a fault tolerance ratio of 33%. For this small example, there is no improvement over the na¨ıve approach with both finding the result in 1 second.

Collective transport. We modelled a simplified version of the algorithm described in [Ferrante et al., 2013; Brambilla, 2014]. In this protocol a group of robots are physically connected to an object and need to move it to a target location. However, the robots have limited sensing so may not all perceive the goal and thus need to agree on a direction to move to. Robots that are perceiving the goal will choose a suitable direction and broadcast it to other robots. All the robots, whether they can perceive the goal or not, will calculate the average of the received directions, and collectively move in the same direction.

We made a few assumptions to model the system. In particular, we discretised time, space and direction of movement and assumed that the robots are working on a finite 5 × 5 grid. The grid is allowed to wrap around, so (5, 1) is left of (1, 1) and (1, 5) is above it. We also assumed that each robot only receives broadcasts from 3 of its neighbours. We initialised the robots at coordinates either (1, 1) or (1, 2) or (2, 1) or (2, 2) and their goal located at (3, 5). We modelled a fault consisting of a robot choosing to move in the wrong direction. We checked the property "all non-faulty robots are always moving towards the target," expressed by the formula

We found a cutoff of 2, giving us a fault tolerance ratio of 50% in 16 seconds, compared to 36 seconds using the iterative approach. Hence, the procedure here introduced was an order of magnitude faster than the na¨ıve approach.

Alpha algorithm. Finally, we assessed the fault-tolerance of the Alpha swarm aggregation algorithm [Winfield et al., 2008], a protocol used to aggregate robotic swarms in the areas of operation. Define a robot to be in another robot's neighbourhood if the position of the former is in the range of the latter's sensor. Each robot keeps track of the number of its neighbours. A robot is said to be connected if its neighbourhood is composed of at least α robots, for a threshold α. The behaviour of each of the robots is characterised by their connectivity status and by whether they are in forward motion mode or in coherence motion mode: if a robot is in forward mode and connected, then it moves forward; if it is in forward mode, but not connected, then it performs a 180◦ turn and changes its motion mode to coherence; if it is in coherence mode, but not connected, then it moves forward; finally, if it is in coherence mode and connected, then it performs a random 90◦ turn and changes its motion mode to forward.

We adopted a number of assumptions commonly made to analyse the algorithm [Kouvaros and Lomuscio, 2017; Dixon et al., 2012]. In particular, we fixed a 5 × 5 arena (once again wrapping around), assumed a communication range of 1, and let α = 2. Initially the robots are connected, in forward mode, and collectively have every possible direction of movement. Formally, we adopted the PIIS proposed in [Kouvaros and Lomuscio, 2015]. We injected direction faults which inhibit a robot from changing direction when it should have as a result of, for example, a mechanical failure. We are here interested in analysing the swarm's connectedness property [Dixon et al., 2012] "every non-faulty robot knows that it will be infinitely often connected," expressed in ACTLK\X as

We found a cutoff of 4, giving us a fault tolerance ratio of 33% in 986 seconds, compared to 1980 seconds obtained via the iterative approach. As in the previous example, the procedure was an order of magnitude faster.

6 Conclusions

We have presented a method for computing the ratio of faulty agents that a protocol can tolerate whilst still satisfying a specification. Calculating the ratio is important when deploying systems as potential failure risks can then be assessed and remedial action can be taken. Alternatively, if a protocol is found to be very robust to errors, more faults can be tolerated at runtime, thereby possibly generating savings.

We are not aware of other approaches for addressing the same problem. When performing the evaluation we compared the approach to an iterative procedure of our construction built from [Kouvaros and Lomuscio, 2017]. We found the present approach to be faster by an order of magnitude on significant examples.

In future work we intend to apply this methodology to study resilience properties in further swarm algorithms.