In this paper we consider the diagnosis of intermittent and permanent faults in discrete event systems. We present a logic based modeling approach associated with conditional preferences in order to produce a single diagnosis at each time step. Like all incomplete diagnosis approaches, ours is subject to deadlocks between the system and its diagnoser. In this paper, we address the detection of such deadlocks at design time with the rich semantic model-checker ELECTRUM.
Using robots in situations where teleoperation is impossible or difficult requires the robots to have some level of decisional autonomy. In particular, an autonomous robot needs to detect and respond appropriately to abnormal losses of performance, due to degradations of the robotic system, or to external disturbances. This requires an elaborate fault management strategy, which can be challenging to design, especially when the mission is complex and the robot is subject to many faults. We are therefore interested in techniques that facilitate the identification of non-nominal operation modes, the detection of faults, and the estimation of the remaining capabilities of the robot.
We propose a modeling formalism constructed so that it meets three requirements. First, it should incrementally calculate a single diagnosis at each time step. This requirement stems from constraints on system performance: one can not afford to compute all possible diagnoses on a large system for a long period of time. Moreover, considering the complete robotic system, the diagnostic module is in our case associated with a deterministic planner which expects a single diagnosis as input. Second, we require our formalism to take into account both permanent and intermittent faults, in particular to distinguish disturbances (noise, false contact, etc.), supposedly intermittent, from degradations (breakdowns, etc.), often permanent. Third, since the diagnosis is used to make autonomous decisions, we want to avoid going back and modifying a diagnosis previously issued. We also forbid from producing a sequence of diagnoses that does not correspond to a possible evolution of the system (for example to remove a permanent fault). Although we do not require strict correctness (we accept delays, slight deviations), this requirement cannot be satisfied if the diagnoser deviates too much from the real system state.
In this paper, we describe how such requirements can create situations where the robotic system produces an observation sequence for which the diagnoser has no explanation. From the point of view of concurrent systems, the physical system sent a message (an observation) that the diagnoser did not expect, thus creating a deadlock. In such a situation, the entire decision process supported by the diagnostic engine fails. This is why we are interested in detecting deadlock scenarios at the design time.
The paper is structured as follows. We start with a presentation of the state of the art in Section 2. We then introduce our modeling formalism in Section 3, and describe the deadlock issue in Section 4. We propose a verification method at design time based on the model-checker ELECTRUM [1] in Section 5, and present experimental results on small multirobot systems in Section 6. Perspectives are discussed in Section 7.
Our work addresses the diagnosis of discrete event systems. In [2] the authors define a framework for the diagnosis of systems modeled by finite state machines subject to permanent faults. The authors describe the construction of a diagnoser that allows an incremental computation of the diagnosis. However, their diagnoser requires memorizing all the possible state-diagnosis pairs, which severely limits its scalability. Their definition of diagnosability illustrates the importance of validating the performance of a diagnoser at design time.
Our formalism associates propositional logic constraints with a conditional preference theory from [3]. It is inspired by the formalism used in [4] to produce incremental diagnoses. In this related work, the authors just point at the risk of encountering a deadlock. In [5], the same authors propose to detect deadlock scenarios between a system and its diagnoser by an iterative model-checking approach but this approach is difficult to implement and no associated experimentations are provided.
The problem of deadlocks between a system and its diagnoser occurs in [6] where the diagnoser goes back in the execution of the diagnoser in order to find a consistent explanation. This solution violates our third requirement explained above. Our goal is to produce reliable diagnoses, or no diagnosis at all.
A classical way to order diagnoses is to prefer the minimal ones, this approach knows several variants compared in [7]. Other approaches like [8] order faults according to some criterion, and deduce an order on diagnoses. In all these approaches, the diagnosis ordering is unconditional, i.e. observations have no effect on the preference order between diagnoses. Our model uses conditional preferences precisely to remove this limitation, and to make it possible to prefer certain diagnoses based on present and past observations.
The diagnosis of intermittent faults is discussed in the literature from different points of view. In [9], the same function is called multiple times, but while faults manifest themselves in an intermittent manner, the underlying diagnosis is constant from one test to another. In [10], a repair event is associated with each fault, and the diagnosis task consists in detecting for each fault which event (fault or repair) happened last. A diagnoser is built to allow incremental evaluation, which involves the previously mentioned scaling problems since all diagnoses are kept in memory.
Our diagnosis model is a tuple (s 0 , ∆, Γ), where s 0 is the initial system state, ∆ is the behavioral model of the system and Γ is the conditional preference model. We assume that the system evolves with discrete events dynamics and that all time steps have the same duration.
We use a set of propositional variables P to describe the state of the system. P is partitioned into two subsets O and E, which respectively represent the elements of the system that are observed and those to be estimated. At each discrete time step, given a truth assignment to the variables from O, our goal is to estimate the value for the variables from E.
Notations For a variable set X, we define an assignment as a function from X to { , ⊥} that associates to each variable x from X the boolean value true ( ) or false (⊥). We write x and x the assignments to {x} such that x (x) = and x (x) = ⊥. For a set of variables X = {x 1 , . . .,
For example, a b c is the assignment to {a, b, c} that assigns true to a and false to b and c. Definition 1 (Observation). An observation, denoted o, is an assignment of the variables of O. Definition 2 (State). A state, denoted s, is an assignment of the variables of P. S denotes the set of states.
The behavioral model ∆ ⊆ S 2 is the transition relation of the system. In order to refer to the state of the system at the previous time step, we introduce a bijective function pre on the set P. For a variable p in P, pre(p) represents the value of the variable p at the previous time step. Formally, we define a variable set P pre = {pre_p | p ∈ P} such that ∀p ∈ P, pre(p) = pre_p. ∆ is represented by a set of propositional logic formulas ∆ p that can relate to both the variables of P and those of P pre .
A pair of states (s pre , s now ) belongs to the transition relation ∆ when the system can be in the state s pre at time t − 1 and in the state s now at time t. To formally link ∆ to ∆ p , for any pair of states (s pre , s now ), we define the assignment σ spre,snow on variables from P ∪ P pre such that ∀p ∈ P, σ spre,snow (p) = s now (p) and σ spre,snow ( In the remaining of this paper, we do not distinguish ∆ and ∆ p .
In order to reason about the possible evolutions of the system state, and the associated observation sequences, we define consistent state sequences and consistent observation sequences as follows.
In the following, when there is no ambiguity, state and observation sequences are assumed to be consistent.
Given a previous state and an observation of the system, we define the set of candidates for diagnosis as the set of states that are compatible with the previous state, the observation and the behavioral model ∆.
Definition 6 (Diagnosis candidates). The set S ∆ (s pre , o) of diagnosis candidates for a previous state s pre and an observation o is defined by:
Example 1. The system illustrated in Figure 1 is composed of a lamp controlled by a switch. This system may be subject to a permanent fault and an intermittent fault, our goal is to estimate their presence or absence. The set O is composed of light which is true when the light is on, false otherwise, and switch which is true when the switch is closed (current flows), false otherwise. The set E contains two variables representing the two faults that may occur: f wire represents an intermittent loose contact in the wire and f light a permanent lamp failure.
The two rules of ∆ represent the following behavior: the lamp glows when the switch is closed and when there is no fault on the wire nor in the lamp (δ 1 ). If the bulb of the lamp was broken at the previous state, then it is at the present time (δ 2 ), i.e. the fault f light is permanent. In the initial state s 0 = light switch f light f wire , the lamp glows and there is no fault.
From the behavioral model ∆, we can calculate diagnosis candidates. For instance, at time step 1, s 0 is the previous system state, let us consider the observation o 1 = light switch. The candidate states set is S ∆ (s 0 , o 1 ) = {s now , s now , s now } with:
In the state s now , the intermittent fault is present alone; in s now , the permanent fault is present alone; both faults are present in s now .
For a given previous state and observation, in order to produce a single diagnosis, we have to choose a single state from all the candidates of S ∆ (s pre , o). This choice is dictated by the conditional preference model Γ that consists in an ordered set of conditional preferences.
A conditional preference relates to a variable to be estimated and indicates under which condition we prefer the diagnoses that assign true of false to this variable to the other diagnoses. Our modeling formalism makes it easy for a preference condition to refer to past variables, which would not be possible with the more usual "next" operator [11]. A preference is a form of "soft constraint", it is only applied when there exists diagnoses with both values for the variable. A formal definition follows. Definition 7 (Conditional preference). A conditional preference γ on a variable e of E, is denoted cond : e ≺ e. The preference's condition cond is a propositional formula on P ∪ P pre . The variable e is called the preference's target.
Note that cond : e ≺ e is equivalent to ¬cond : e ≺ e. For a variable e from E, the conditional preference cond : e ≺ e expresses a preference for states in which e is true to those where e is false if and only if cond is satisfied.
Formally, a preference γ = cond : e ≺ e defines a partial order ≺ γ an equivalence relation ≈ γ between pairs of transitions as follows. For all triples s pre , s, s ∈ S 3 , γ strictly prefers the transition (s pre , s) to transition (s pre , s ) (denoted (s pre , s) ≺ γ (s pre , s )) if and only if σ spre ,s |= cond ↔ e and σ spre ,s cond ↔ e. Transitions (s pre , s) and (s pre , s ) are equivalent to γ (denoted
Example 2. Let us consider the preference γ = ¬light : f light ≺ f light . This preference indicates that if both f light and f light are part of some diagnosis candidate, then f light is preferred if and only if ¬light holds. Formally, we prefer diagnoses that satisfy ¬light ↔ f light . For the states s now , s now and s now in Example 1, as ¬light holds, we prefer the states in which f light holds, i.e. the states s now and s now . Formally, s now ≺ γ s now , s now ≺ γ s now and s now ≈ γ s now .
We assume that in Γ, all estimated variables are the target of a conditional preference. While not always necessary, it ensures the diagnoser is deterministic. This raises the question of the order in which preferences are applied, that we address now.
A conditional preference model Γ is a sequence of conditional preferences (γ 1 , γ 2 ,..,γ n ) with γ i = cond i : e i ≺ e i for i ∈ [1, n] such that each variable e from E is the target of exactly one preference.
We require Γ to be an acyclic preference model, which guarantees its consistence (see [12]). For example, the following two preferences form a cycle: a : b ≺ b and b : a ≺ a. In the first preference the value of a depends on that of b, and in the second preference the exact opposite happens. While the literature contains work on cyclic preference networks [12], in this paper we assume that Γ is acyclic. This means that the condition of a preference γ i cannot use variables that are the target of the following preferences in the sequence. Formally, ∀i ∈ [1, n] , the scope of the condition cond i is a subset of P pre ∪O∪{e j |1 ≤ j < i}.
From a preference model Γ, it is possible to define a partial order ≺ Γ between pairs of states as follows. Intuitively, as in a lexicographic order, we consider preferences γ i in their index order in Γ and we apply at each index the order relation ≺ γi defined above. This order is partial because it compares only pairs of transitions (s pre , s now ) and (s pre , s now ) that have the same previous state (i.e. s pre = s pre ) and whose successor states produce the same observation (i.e. ∀o ∈ Os now (o) = s now (o)).
Formally, ∀s pre , s, s ∈ S 3 , (s pre , s) is strictly preferred to (s pre , s ) by Γ (denoted (s pre , s) ≺ Γ (s pre , s )) if and only if there exists i ∈ [1, n] such that for all j < i, (s pre , s) ≈ γj (s pre , s ) and (s pre , s) ≺ γi (s pre , s ).
Although the ≺ Γ order is partial on S 2 , it is complete on any set of diagnosis candidates. We use this order relation to define the preferred diagnosis at each time step. Proposition 1. Let s pre be a state, o an observation, ∆ a behavioral model and Γ a preference model. If s and s are two candidate states for s pre and o (s, s ∈ S ∆ (s pre , o) 2 ) such that s = s then we have either (s pre , s) ≺ Γ (s pre , s ) or (s pre , s ) ≺ Γ (s pre , s).
Proof By Definition 6, s and s belong to S ∆ (s pre , o) implies that ∀o ∈ O, s(o) = s (o). Therefore, s = s means that there is a variable e ∈ E such that s(e) = s (e). So, there exists a preference γ ∈ Γ such that s ≈ γ s does not hold. Let i be the index of the first preference of the sequence in this case. Formally, γ i is such that ∀j < i, (s pre , s) ≈ γj (s pre , s ), (s pre , s) ≈ γi (s pre , s ) does not hold. This means that (s pre , s) ≺ γi (s pre , s ) or (s pre , s ) ≺ γi (s pre , s). From the order ≺ Γ , we then have (s pre , s) ≺ Γ (s pre , s ) or (s pre , s ) ≺ Γ (s pre , s).
The first preference (γ 1 ) declares that we prefer the value for f wire that was estimated at the previous time step. This mechanism makes it possible to bring some stability to the diagnosis since f wire is an intermittent fault: if ∆ allows both diagnoses for f wire , we prefer to maintain the diagnosis that was chosen at the previous time step.
The preference (γ 2 ) indicates that we always prefer to assume that f light is absent.
In Example 1, with s 0 = light switch f light f wire ) as the previous state and o 1 = light switch as the observation, the set of diagnosis candidates S ∆ (s pre , o) contains the three states s now = light switch f light f wire , s now = light switch f light f wire and s now = light switch f light f wire .
By applying (γ 1 ) first, as pre_f wire holds in the three states, we prefer the states in which f wire . In our case, only s now satisfies this criterion. As there is only one diagnosis left, we do not need to apply preference (γ 2 ). The preferred single state is ŝ1 = estim(s 0 , o 1 ) = s now = light switch f light f wire .
A deadlock situation occurs when the diagnoser has previously estimated a state ŝ different from the current system state s, and receives an observation o in contradiction with ŝ and ∆. In such a situation the candidates set for ŝ and o is empty and the diagnoser is unable to return a diagnosis. Definition 11 (Deadlock). An estimation model (s 0 , ∆, Γ) is in a deadlock situation for an observation sequence (o 0 , o 1 , o 2 , . . . , o k ) with k > 1 1 if and only if:
1. there exists an estimated state sequence for (o 0 , . . . , o k−1 ), and 2. there exist no estimated state sequence for (o 0 , . . . , o k ) Example 4. Let (o 0 , o 1 , o 2 , o 3 ) be the observation sequence produced by the system and along with the associated state sequence (s 0 , s 1 , s 2 , s 3 ) described in Figure 2.
When observation o 1 is received, Γ selects the preferred state ŝ1 = light switch f light f wire . Then for observation o 2 , we are in the situation described in Example 3 and the preferred state is ŝ2 = light switch f light f wire . Observation o 3 is in contradiction with the previously estimated state. In fact the estimator has estimated f light in the previous state, meaning that variable pre_f light is true. Rules of ∆ are not consistent with such a configuration: (δ 1 ) requires f light to 1 There can be no deadlock at ŝ1 because we assume that the diagnoser is correctly initialized at s0. be false because the lamp glows while (δ 2 ) requires f light to be true since the associated fault is permanent.
Therefore, there is an estimated state sequence for (o 0 , o 1 , o 2 ): this is the sequence (s 0 , ŝ1 , ŝ2 ). However, since there is no estimated state sequence for (o 0 , o 1 , o 2 , o 3 ), the pair system-diagnoser is in a deadlock situation for this observation sequence.
In the previous example, the deadlock situation could be eliminated by changing the order or conditions of preferences. However, as soon as one is interested in more complex systems, it becomes difficult to anticipate the deadlock situations and even more to solve them. In this paper, we focus on detecting these deadlocks and leave their resolution for future work.
In this section, we show how to use a model-checker to identify deadlock scenarios at the design phase of the diagnostic model.
The verification method we propose is inspired from the Twin-Plant [13] technique, which makes it possible to verify the diagnosability of a system by constructing the synchronous product of two finite state machines.
Our method is similar since it involves constructing a deadlock verifier by synchronizing two state machines. The first state machine represents the system and is constrained only by the transition relation ∆. We use it to generate consistent observation sequences. The second state machine is the diagnoser built from the whole estimation model. It is also constrained by ∆, but it deterministically selects the next state by applying Γ preferences. The verifier is the product of these two state machines synchronized on observable variables at each time step. Deadlock checking then consists in checking whether there exists an observation sequence that leads the verifier to a state in which the system has a successor state, but the diagnoser has none.
In order to distinguish the states of the two state machines presented above, i.e. the state of the system and that of the diagnoser, we introduce two variable sets P sys and P est that are direct copies of P. We also use a est_sat variable that indicates whether the diagnoser has a successor state. Definition 12 (Verifier variables). The set of the verifier variables is defined by P verif = P sys ∪ P est ∪ {est_sat}, where :
• P sys = {p_sys | p ∈ P} is the set of variables describing the system state ; • est_sat indicates whether there is an estimated state for the diagnoser.
A state of the verifier is an assignment on variables of P verif .
In order to define the state machine resulting from the synchronous product, we successively define the initial state of the verifier (Definition 13) and its transition relation (Definition 14). (1) variables associated with observations take the same value on system and diagnoser sides,
(2) the system transition described by variables of P sys satisfies ∆,
(3) the variable est_sat indicates whether there exists a possible estimated state (i.e. if the candidates set is not empty), and
(4) if est_sat is true, then the diagnoser transition described by variables of P est satisfies ∆ and Γ.
Formally :
∃(spre , snow ) ∈ ∆, ∀p ∈ P, spre (p) = s verif pre (sys_p) and snow (p) = s verif now (sys_p)
(2) ) as follows:
We show that for all i ∈ [0, n − 1], (s verif i , s verif i+1 ) is a transition of the checker: let i be an integer in [0, n − 1], we show that the four parts of Definition 14 are satisfied:
• ∀o ∈ O, ∀p ∈ P, s i (p) = ŝi (p) and s i+1 (p) = ŝi+1 (p). Equation ( 1) holds;
• equation ( 2) holds by construction of the verifier;
) is the pair of states in ∆ satisfying equation ( 3);
• for i = n − 1, the definition of a deadlock implies that there does not exist a pair of states satisfying ∆: equation ( 3) is satisfied;
) is the pair of states in ∆ satisfying equation ( 4); For the reciprocal, let us assume that the checker has a path in which est_sat is false. We consider such a path
is the only state in which false is assigned to est_sat. We then build two states sequences (s 0 , s 1 , . . . , s n ) and (s 0 , ŝ1 , . . . , ŝn−1 ) as follows:
• ∀i ∈ [0, n], ∀p ∈ P, s i (p) = s verif i (p_sys),
We prove that these state sequences are consistent with ∆.
From Definition 14, est_sat is false (last time step) implies that no state s now allows to satisfy the right part of the condition (equation 3) for s pre = ŝn−1 . This means that no state meets the Definition 6. There is a deadlock for the observation sequence generated by (s 0 , s 1 , . . . , s n ).
Model-checking is a set of techniques and computer tools for checking properties on systems. Among the many model-checkers in the literature, NuSMV [14] and NuXMV are known for their effectiveness in checking temporal properties on dynamic systems. They are based on temporal logic like LTL or CTL. Another family of model checkers is specialized in checking properties on structurally complex models, but without temporal dynamics. This is the case of the Alloy Analyzer model-checker [15] which supports a fragment of first order logic.
In the case of deadlock verification, we need to express the temporal dynamics of the system but also the preferences of the diagnoser, which are not easily expressed in propositional logic. We therefore chose to use the modelchecker ELECTRUM [1] which is based on the Alloy language and integrates temporal dynamics as in NuSMV.
The concept of preference is part of the verifier definition. This means that the model-checker language must allow to express them. To do so, we define a quantified form for preferences. Definition 15 (Preference quantified form). Let be Γ = (γ 1 , . . . , γ n ) a preference model in which each preference has form γ i = cond i : e i ≺ e i . The quantified form of γ i is the formula ψ i defined by:
The quantified form ψ i is composed of two parts. The left part is only satisfied when for both truth values variable e i , there is a way to assign the target variables of the following preferences and still satisfy ∆. It represents the cases when the preference is actually applied. The right part expresses the effect of the preference, i.e that e i is assigned to true if and only if the condition cond i is satisfied. Through the following proposition, we show that Γ preferences and their quantified form are equivalent from the point of view of the estimated state for a previous state and an observation. Proposition 3. For a previous estimated state ŝpre , an observation o, a candidate ŝ ∈ S ∆ (ŝ pre , o), ŝ = estim(ŝ pre , o) if and only if the assignment σ ŝpre ,ŝ satisfies conjunction i∈ [1,n]
Proof. Let ŝpre be a previous estimated state, o an observation and ŝ a state in S ∆ (ŝ pre , o). We inductively show that ŝ is preferred for the preference sequence (γ 1 , . . . , γ k ) if and only if the assignment σ ŝpre ,ŝ satisfies i∈ [1,k]
For k = 1, the set of free variables in formula lhs 1 = ∀e 1 , ∃e 2 , . . . e n , ∆ is the set O, since all the variables in E are quantified. The formula lhs 1 is satisfied by an observation o if and only if both oe 1 and oe 1 have an extension in P ∪ P pre that satisfies ∆. This means S ∆ (ŝ pre , o) contains at least two states s and s with s(e 1 ) = s (e 1 ). Among these two states, the one that satisfies cond 1 ↔ e 1 is the preferred state by preference γ 1 , and also satisfies ψ 1 . As the states preferred by γ 1 are exactly the ones for which the assignment σ ŝpre ,ŝ satisfies ψ 1 , then the proposition holds for k = 1.
Let k > 1 and let us assume that the induction is valid at index k − 1, i.e. that ŝ is preferred for the preference sequence (γ 1 , . . . , γ k−1 ) if and only if the assignment σ ŝpre ,ŝ satisfies i∈[1,k−1] ψ i . Since s and s belong to S ∆ (ŝ pre , o), since s is a state preferred for (γ 1 , . . . , γ k−1 ) and since σ ŝpre ,s satisfies i∈[1,k−1] ψ i , then for all i < k, s(e i ) = s (e i ).
The set of free variables in formula lhs k = ∀e k , ∃e k+1 , . . . e n , ∆ is the set O ∪ {e i | i < k}. An assignment op to these variables satisfies lhs k if and only if op e k and op e k both have an extension to P ∪ P pre that satisfies ∆.
If for a given assignment op to O ∪ {e i | i < k} the formula lhs k does not hold, then for all s and s in S ∆ (ŝ pre , o), s(e k ) = s (e k ). Thus, the preference γ k is not applied and the preferred states for (γ 1 , . . . , γ k−1 ) are the also preferred for (γ 1 , . . . , γ k ). In this case, ψ k = and the states s such that σ ŝpre ,s satisfy i∈[1,k−1] ψ i are the same ones for which σ ŝpre ,s satisfy i∈ [1,k] and s such that for all i < k, s(e i ) = s (e i ) and s(e k ) = s (e k ). Between these two states, the one in which cond k ↔ e k is true is the preferred state by preference γ k . As the states preferred by γ k are exactly the ones for which the assignment σ ŝpre ,ŝ satisfies ψ k , thus the induction is valid at index k.
In this section, we illustrate how the verifier defined in Definition 13 and 14 is encoded in ELECTRUM. We illustrate the encoding of the system described in Examples 1 and 3.
To model the system's state machine, we declare a predicate corresponding exactly to the model ∆ then we declare a constraint (a fact in ELECTRUM) that specifies that the system respects the predicate at all time steps (always in ELECTRUM), as illustrated in Figure 3. A similar constraint is declared for the diagnoser's state machine. Finally, we synchronize the variables from O of the observed system with those of the second state machine representing our estimator, as expressed in condition (1) of Definition 14.
To represent the temporal aspect of our formalism, we use the operator ' from ELECTRUM which describes a variable at the next time step. Figure 4 reproduces the intention of the bijective function pre (p_pre value at next state is equal to p value at current state).
ELECTRUM supports the use of relational algebra operators. It is possible for each preference to write a predicate telling us if a preference γ i is applicable, that is, if the two valuations for variable e i (operator all), and at least one possible valuation for variables e j , i < j ≤ n (operator some) are consistent with ∆ an the observation. This corresponds to the left part of the quantified form of a preference. Figure 5 illustrates the definition of predicates that implement these conditions with ELECTRUM operators. The rest The order in which preferences are applied in Γ, is completely induced by the quantification overlays in the quantified forms of preferences (see Definitions 8 and 15).
We experimented our approach on the model of a multirobot mission of customizable size and complexity.
In this mission, one or more robots move on a rectangular grid of variable size, each robot moves towards its destination. The destination can change during the mission according to unspecified dynamics.
Behavioral constraints are declared in ∆ for each robot. robots should move unless they are at their destination. Moreover, robots may be subject to permanent and / or intermittent faults. An intermittent fault slows down or immobilizes the robot for a few moments which is modelled by the fact that a robot takes several time steps to cross a cell. A permanent fault immobilizes the robot permanently. We also estimate the state of the terrain. A robot crosses a normal cell in one time step, but we introduce difficult cells (the robot takes several time steps to go through the cell) and dangerous cells (robot stays forever on the cell).
We observe at every moment the position of robots on the grid and their destination. We estimate the presence of intermittent and permanent faults on each robot, a variable indicating if it can move, as well as the dangerousness of each grid cell. We implement two estimation strategies, one subject to deadlock, the other not (for example always preferring the absence of a permanent fault).
Models are written in Scala language and are automatically translated into ELECTRUM. ELECTRUM proceeds to the verification through different solvers. For our experiments, we set ELECTRUM to use the Sat4j solver [16]. Verifications were performed on a 3.5GHz Intel Core i5-7600 quad-core processor. Figure 6 shows the results of our experiments for different mission parameters.
The first conclusion is that verification is faster for models that are subject to deadlock scenarios than for those that do not encounter such scenarios. This difference is directly related to the fact that when the model-checker finds a deadlock scenario in the model, the search ends immediately and it returns a counterexample corresponding to the sequence of observations. On the contrary, to prove that a model contains no deadlock scenarios, ELECTRUM explores many more possible executions paths for the verifier.
We can then see that the verification is very fast for the first models, but as we enrich P, ∆ and Γ, the number of variables generated for Sat4j and the time required for verification increases exponentially. For examples of larger sizes, it is interesting to note that Sat4j did not have enough memory to process them.
Deadlock detection as proposed in the paper is carried out in the design phase. Hence, high calculation times are not necessarily unacceptable and do not call into question the approach we propose. Let us notice that the results we present here are preliminary results and we are currently working on different ways to improve them. Specifically, we aim to integrate ELECTRUM more closely to avoid the creation of boolean variables where ELECTRUM could handle enumerated variables.
We have developed a generic method to validate the proper behavior of a diagnoser at design stage. In particular, we have showed that it is possible to anticipate deadlock situations.
In this paper, we do not introduce any mechanism to identify the causes and modify the estimation model in order to eliminate deadlock scenarios, but this remains a goal for future work. In particular, there are several ways to treat a deadlock scenario. One can ignore it, as in the deadlocking path the system should stop autonomous operation and wait for operator intervention. One can alter the system's behaviour or instrumentation, which is costly and sometimes impossible. Finally, one can revise the fault management strategy, by changing the preference ordering, or simply diagnosing other elements of the system, such as whether we trust a component instead of its real health status.
In addition, we plan to reuse the automation of modelchecking allowing us to verify the existence of deadlock scenarios for our diagnosers to check other properties related to diagnosis such as diagnosability. Finally, progress on model-checker performance is needed to apply it to multi-robot missions involving large models. QBF solvers [17] are potential tools for finding deadlock scenarios of bounded length, as can express the quantified form of our conditional preferences. It is thus possible to express the presence of a deadlocking path of bounded length as a QBF satisfiability problem.