=Paper= {{Paper |id=Vol-2289/paper1 |storemode=property |title=Preferential Discrete Model-based Diagnosis for Intermittent and Permanent Faults |pdfUrl=https://ceur-ws.org/Vol-2289/paper1.pdf |volume=Vol-2289 |authors=Valentin Bouziat,Xavier Pucel,Stéphanie Rousse |dblpUrl=https://dblp.org/rec/conf/safeprocess/BouziatPRT18 }} ==Preferential Discrete Model-based Diagnosis for Intermittent and Permanent Faults== https://ceur-ws.org/Vol-2289/paper1.pdf

Preferential Discrete Model-based Diagnosis
for Intermittent and Permanent Faults
Valentin Bouziat1 and Xavier Pucel1 and Stéphanie Roussel1 and Louise Travé-Massuyès2
1
ONERA / DTIS, Université de Toulouse, F-31055 Toulouse – France
e-mail: firstname.name@onera.fr
2
LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France
e-mail: louise@laas.fr

Abstract In this paper, we describe how such requirements can cre-
ate situations where the robotic system produces an obser-
In this paper we consider the diagnosis of inter- vation sequence for which the diagnoser has no explanation.
mittent and permanent faults in discrete event sys- From the point of view of concurrent systems, the physical
tems. We present a logic based modeling ap- system sent a message (an observation) that the diagnoser
proach associated with conditional preferences in did not expect, thus creating a deadlock. In such a situa-
order to produce a single diagnosis at each time tion, the entire decision process supported by the diagnostic
step. Like all incomplete diagnosis approaches, engine fails. This is why we are interested in detecting dead-
ours is subject to deadlocks between the system lock scenarios at the design time.
and its diagnoser. In this paper, we address the The paper is structured as follows. We start with a presen-
detection of such deadlocks at design time with tation of the state of the art in Section 2. We then introduce
the rich semantic model-checker E LECTRUM. our modeling formalism in Section 3, and describe the dead-
lock issue in Section 4. We propose a verification method at
1 Introduction design time based on the model-checker E LECTRUM [1] in
Section 5, and present experimental results on small multi-
Using robots in situations where teleoperation is impossible
robot systems in Section 6. Perspectives are discussed in
or difficult requires the robots to have some level of deci-
Section 7.
sional 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 2 Related Work
to external disturbances. This requires an elaborate fault Our work addresses the diagnosis of discrete event systems.
management strategy, which can be challenging to design, In [2] the authors define a framework for the diagnosis of
especially when the mission is complex and the robot is systems modeled by finite state machines subject to perma-
subject to many faults. We are therefore interested in tech- nent faults. The authors describe the construction of a di-
niques that facilitate the identification of non-nominal oper- agnoser that allows an incremental computation of the di-
ation modes, the detection of faults, and the estimation of agnosis. However, their diagnoser requires memorizing all
the remaining capabilities of the robot. the possible state-diagnosis pairs, which severely limits its
We propose a modeling formalism constructed so that it scalability. Their definition of diagnosability illustrates the
meets three requirements. First, it should incrementally cal- importance of validating the performance of a diagnoser at
culate a single diagnosis at each time step. This require- design time.
ment stems from constraints on system performance: one Our formalism associates propositional logic constraints
can not afford to compute all possible diagnoses on a large with a conditional preference theory from [3]. It is inspired
system for a long period of time. Moreover, considering the by the formalism used in [4] to produce incremental diag-
complete robotic system, the diagnostic module is in our noses. In this related work, the authors just point at the risk
case associated with a deterministic planner which expects of encountering a deadlock. In [5], the same authors pro-
a single diagnosis as input. Second, we require our for- pose to detect deadlock scenarios between a system and its
malism to take into account both permanent and intermit- diagnoser by an iterative model-checking approach but this
tent faults, in particular to distinguish disturbances (noise, approach is difficult to implement and no associated experi-
false contact, etc.), supposedly intermittent, from degrada- mentations are provided.
tions (breakdowns, etc.), often permanent. Third, since the The problem of deadlocks between a system and its di-
diagnosis is used to make autonomous decisions, we want agnoser occurs in [6] where the diagnoser goes back in the
to avoid going back and modifying a diagnosis previously execution of the diagnoser in order to find a consistent ex-
issued. We also forbid from producing a sequence of di- planation. This solution violates our third requirement ex-
agnoses that does not correspond to a possible evolution plained above. Our goal is to produce reliable diagnoses, or
of the system (for example to remove a permanent fault). no diagnosis at all.
Although we do not require strict correctness (we accept A classical way to order diagnoses is to prefer the min-
delays, slight deviations), this requirement cannot be satis- imal ones, this approach knows several variants compared
fied if the diagnoser deviates too much from the real system in [7]. Other approaches like [8] order faults according to
state. some criterion, and deduce an order on diagnoses. In all
these approaches, the diagnosis ordering is unconditional, switch light
i.e. observations have no effect on the preference order be-
tween 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 obser-
vations.
The diagnosis of intermittent faults is discussed in the lit- fwire flight
erature from different points of view. In [9], the same func-
tion is called multiple times, but while faults manifest them-
selves in an intermittent manner, the underlying diagnosis Figure 1: A simple system composed of a lamp and a switch
is constant from one test to another. In [10], a repair event
is associated with each fault, and the diagnosis task consists spre (p). We consider that a pair of states belongs to the tran-
in detecting for each fault which event (fault or repair) hap- sition relation ∆ if and only if the corresponding assignment
pened last. A diagnoser is built to allow incremental evalua- satisfies the formulas of ∆p .
tion, which involves the previously mentioned scaling prob-
lems since all diagnoses are kept in memory. Definition 3 (Transition). A pair of states (spre , snow ) ∈
S 2 is a transition, denoted (spre , snow ) ∈ ∆, if and only if
3 Diagnosis model σspre ,snow |= ∆p .
Our diagnosis model is a tuple (s0 , ∆, Γ), where s0 is the In the remaining of this paper, we do not distinguish ∆
initial system state, ∆ is the behavioral model of the system and ∆p .
and Γ is the conditional preference model. We assume that In order to reason about the possible evolutions of the
the system evolves with discrete events dynamics and that system state, and the associated observation sequences, we
all time steps have the same duration. define consistent state sequences and consistent observation
sequences as follows.
3.1 Variables
Definition 4 (Consistent state sequence). A state sequence
We use a set of propositional variables P to describe the state (s0 , s1 , . . . , sn ) ∈ S n is consistent if and only if ∀i ∈ [1, n],
of the system. P is partitioned into two subsets O and E, (si−1 , si ) ∈ ∆.
which respectively represent the elements of the system that
are observed and those to be estimated. At each discrete Definition 5 (Consistent observation sequence). An obser-
time step, given a truth assignment to the variables from O, vation sequence (o0 , o1 , . . . , on ) is consistent if and only if
our goal is to estimate the value for the variables from E. there exist a consistent state sequence (s0 , s1 , . . . , sn ) such
that ∀i ∈ [0, n], ∀o ∈ O, si (o) = oi (o).
Notations For a variable set X, we define an assignment as In the following, when there is no ambiguity, state and
a function from X to {>, ⊥} that associates to each variable observation sequences are assumed to be consistent.
x from X the boolean value true (>) or false (⊥). We write Given a previous state and an observation of the system,
x and x the assignments to {x} such that x (x) = > and we define the set of candidates for diagnosis as the set of
x (x) = ⊥. For a set of variables X = {x1 , . . ., xn }, if for i ∈ states that are compatible with the previous state, the obser-
[1, n], fi is an assignment {xi } → {>, ⊥}, then f1 f2 . . . fn vation and the behavioral model ∆.
denotes the f assignment on X such that ∀xi ∈ X, f (xi ) = Definition 6 (Diagnosis candidates). The set S∆ (spre , o) of
fi (xi ). For example, a b c is the assignment to {a, b, c} diagnosis candidates for a previous state spre and an obser-
that assigns true to a and false to b and c. vation o is defined by:
Definition 1 (Observation). An observation, denoted o, is
an assignment of the variables of O. S∆ (spre , o) = snow ∈ S |(spre , snow ) ∈ ∆ and
Definition 2 (State). A state, denoted s, is an assignment of ∀o ∈ O, snow (o) = o(o)
the variables of P. S denotes the set of states.
Example 1. The system illustrated in Figure 1 is composed
3.2 Behavioral Model of a lamp controlled by a switch. This system may be subject
The behavioral model ∆ ⊆ S 2 is the transition relation of to a permanent fault and an intermittent fault, our goal is to
the system. In order to refer to the state of the system at the estimate their presence or absence. The set O is composed
previous time step, we introduce a bijective function pre of light which is true when the light is on, false otherwise,
on the set P. For a variable p in P, pre(p) represents the and switch which is true when the switch is closed (current
value of the variable p at the previous time step. Formally, flows), false otherwise. The set E contains two variables rep-
we define a variable set Ppre = {pre_p | p ∈ P} such that resenting the two faults that may occur: fwire represents an
∀p ∈ P, pre(p) = pre_p. ∆ is represented by a set of intermittent loose contact in the wire and flight a perma-
propositional logic formulas ∆p that can relate to both the nent lamp failure.
variables of P and those of Ppre . The two rules of ∆ represent the following behavior: the
A pair of states (spre , snow ) belongs to the transition re- lamp glows when the switch is closed and when there is no
lation ∆ when the system can be in the state spre at time fault on the wire nor in the lamp (δ1 ). If the bulb of the lamp
t − 1 and in the state snow at time t. To formally link ∆ was broken at the previous state, then it is at the present time
to ∆p , for any pair of states (spre , snow ), we define the as- (δ2 ), i.e. the fault flight is permanent. In the initial state
signment σspre ,snow on variables from P ∪ Ppre such that s0 = light switch flight fwire , the lamp glows and there is
∀p ∈ P, σspre ,snow (p) = snow (p) and σspre ,snow (pre(p)) = no fault.
ensures the diagnoser is deterministic. This raises the ques-
tion of the order in which preferences are applied, that we
light ↔ switch ∧ ¬flight ∧ ¬fwire (δ1 ) address now.
∆=
pre_flight → flight (δ2 )
Definition 8 (Conditional preference model). A conditional
From the behavioral model ∆, we can calculate diagno- preference model Γ is a sequence of conditional preferences
sis candidates. For instance, at time step 1, s0 is the pre- (γ1 , γ2 ,..,γn ) with γi = condi : ei ≺ ei for i ∈ [1, n] such
vious system state, let us consider the observation o1 = that each variable e from E is the target of exactly one pref-
light switch. The candidate states set is S∆ (s0 , o1 ) = erence.
{snow , s0now , s00now } with:
We require Γ to be an acyclic preference model, which
snow = light switch flight fwire guarantees its consistence (see [12]). For example, the fol-
lowing two preferences form a cycle: a : b ≺ b and
s0now = light switch flight fwire
b : a ≺ a. In the first preference the value of a depends
s00now = light switch flight fwire on that of b, and in the second preference the exact oppo-
site happens. While the literature contains work on cyclic
In the state snow , the intermittent fault is present alone; in
preference networks [12], in this paper we assume that Γ
s0now , the permanent fault is present alone; both faults are
is acyclic. This means that the condition of a preference γi
present in s00now .
cannot use variables that are the target of the following pref-
3.3 Single diagnosis choice erences in the sequence. Formally, ∀i ∈ [1, n] , the scope of
the condition condi is a subset of Ppre ∪O∪{ej |1 ≤ j < i}.
For a given previous state and observation, in order to pro- From a preference model Γ, it is possible to define a
duce a single diagnosis, we have to choose a single state partial order ≺Γ between pairs of states as follows. Intu-
from all the candidates of S∆ (spre , o). This choice is dic- itively, as in a lexicographic order, we consider preferences
tated by the conditional preference model Γ that consists in γi in their index order in Γ and we apply at each index
an ordered set of conditional preferences. the order relation ≺γi defined above. This order is partial
A conditional preference relates to a variable to be esti- because it compares only pairs of transitions (spre , snow )
mated and indicates under which condition we prefer the and (spre 0 , snow 0 ) that have the same previous state (i.e.
diagnoses that assign true of false to this variable to the spre = spre 0 ) and whose successor states produce the same
other diagnoses. Our modeling formalism makes it easy observation (i.e. ∀o ∈ Osnow (o) = snow 0 (o)).
for a preference condition to refer to past variables, which Formally, ∀spre , s, s 0 ∈ S 3 , (spre , s) is strictly preferred
would not be possible with the more usual “next” operator to (spre , s 0 ) by Γ (denoted (spre , s) ≺Γ (spre , s 0 )) if and
[11]. A preference is a form of “soft constraint”, it is only
only if there exists i ∈ [1, n] such that for all j < i,
applied when there exists diagnoses with both values for the (spre , s) ≈γj (spre , s 0 ) and (spre , s) ≺γi (spre , s 0 ).
variable. A formal definition follows.
Although the ≺Γ order is partial on S 2 , it is complete on
Definition 7 (Conditional preference). A conditional pref- any set of diagnosis candidates. We use this order relation
erence γ on a variable e of E, is denoted cond : e ≺ e. The to define the preferred diagnosis at each time step.
preference’s condition cond is a propositional formula on
P ∪ Ppre . The variable e is called the preference’s target. Proposition 1. Let spre be a state, o an observation, ∆ a
behavioral model and Γ a preference model. If s and s 0 are
Note that cond : e ≺ e is equivalent to ¬cond : e ≺ e. two candidate states for spre and o (s, s 0 ∈ S∆ (spre , o)2 )
For a variable e from E, the conditional preference cond : such that s 6= s 0 then we have either (spre , s) ≺Γ (spre , s 0 )
e ≺ e expresses a preference for states in which e is true to or (spre , s 0 ) ≺Γ (spre , s).
those where e is false if and only if cond is satisfied.
Formally, a preference γ = cond : e ≺ e defines Proof By Definition 6, s and s 0 belong to S∆ (spre , o)
a partial order ≺γ an equivalence relation ≈γ between implies that ∀o ∈ O, s(o) = s 0 (o). Therefore, s 6= s 0
pairs of transitions as follows. For all triples spre , s, s 0 ∈ means that there is a variable e ∈ E such that s(e) 6= s 0 (e).
S 3 , γ strictly prefers the transition (spre , s) to transition So, there exists a preference γ ∈ Γ such that s ≈γ s 0
(spre , s 0 ) (denoted (spre , s) ≺γ (spre , s 0 )) if and only if does not hold. Let i be the index of the first preference
σspre ,s |= cond ↔ e and σspre ,s 0 2 cond ↔ e. Tran- of the sequence in this case. Formally, γi is such that
sitions (spre , s) and (spre , s 0 ) are equivalent to γ (denoted ∀j < i, (spre , s) ≈γj (spre , s 0 ), (spre , s) ≈γi (spre , s 0 )
(spre , s) ≈γ (spre , s 0 )) if and only if (σspre ,s |= cond ↔ does not hold. This means that (spre , s) ≺γi (spre , s 0 ) or
e) ⇔ (σspre ,s 0 |= cond ↔ e). (spre , s 0 ) ≺γi (spre , s). From the order ≺Γ , we then have
(spre , s) ≺Γ (spre , s 0 ) or (spre , s 0 ) ≺Γ (spre , s).
Example 2. Let us consider the preference γ = ¬light :
flight ≺ flight . This preference indicates that if both flight 3.4 Estimation process
and flight are part of some diagnosis candidate, then flight is At each step, given the set of candidate states S∆ (spre , o)
preferred if and only if ¬light holds. Formally, we prefer we select the state preferred by the conditional preference
diagnoses that satisfy ¬light ↔ flight . For the states model Γ.
snow , s0now and s00now in Example 1, as ¬light holds, we
prefer the states in which flight holds, i.e. the states s0now Definition 9 (Estimated state). The estimated state ŝ =
and s00now . Formally, s0now ≺γ snow , s00now ≺γ snow and estim(spre , o) for a previous state spre and an observation
s00now ≈γ s0now . o is the element of S∆ (spre , o) preferred by ≺Γ . Formally,
ŝ = estim(spre , o) if and only if:
We assume that in Γ, all estimated variables are the target
of a conditional preference. While not always necessary, it 1. ŝ ∈ S∆ (spre , o), and
2. ∀snow ∈ S∆ (spre , o) such that snow 6= ŝ, we have be false because the lamp glows while (δ2 ) requires flight
(spre , ŝ) ≺Γ (spre , snow ). to be true since the associated fault is permanent.
From the initial state s0 , we now define the sequence of Therefore, there is an estimated state sequence for
estimated states that is produced by the diagnoser for a given (o0 , o1 , o2 ): this is the sequence (s0 , ŝ1 , ŝ2 ). How-
observation sequence. ever, since there is no estimated state sequence for
(o0 , o1 , o2 , o3 ), the pair system-diagnoser is in a deadlock
Definition 10 (Estimated state sequence). A state sequence situation for this observation sequence.
(s0 , ŝ1 , ŝ2 , ..., ŝk ) is the estimated state sequence for the
observation sequence (o0 , o1 , o2 ,...,ok ) if and only if ∀i ∈ In the previous example, the deadlock situation could be
[1, k], ŝi = estim(ŝi−1 , oi ). eliminated by changing the order or conditions of prefer-
ences. However, as soon as one is interested in more com-
Example 3. Let us associate the lamp model ∆ from Exam- plex systems, it becomes difficult to anticipate the deadlock
ple 1 to the following preferences: situations and even more to solve them. In this paper, we fo-

pre_fwire : fwire ≺ fwire (γ1 )
cus on detecting these deadlocks and leave their resolution
Γ= for future work.
⊥ : flight ≺ flight (γ2 )
The first preference (γ1 ) declares that we prefer the value 5 Deadlock Checking
for fwire that was estimated at the previous time step. This
In this section, we show how to use a model-checker to iden-
mechanism makes it possible to bring some stability to the
tify deadlock scenarios at the design phase of the diagnostic
diagnosis since fwire is an intermittent fault: if ∆ allows
model.
both diagnoses for fwire , we prefer to maintain the diagno-
sis that was chosen at the previous time step. 5.1 Deadlock checker
The preference (γ2 ) indicates that we always prefer to
The verification method we propose is inspired from the
assume that flight is absent.
Twin-Plant [13] technique, which makes it possible to ver-
In Example 1, with s0 = light switch flight fwire ) as ify the diagnosability of a system by constructing the syn-
the previous state and o1 = light switch as the observa- chronous product of two finite state machines.
tion, the set of diagnosis candidates S∆ (spre , o) contains Our method is similar since it involves constructing a
the three states snow = light switch flight fwire , snow 0 = deadlock verifier by synchronizing two state machines. The
light switch flight fwire and s00now = light switch flight fwire . first state machine represents the system and is constrained
By applying (γ1 ) first, as pre_fwire holds in the three only by the transition relation ∆. We use it to generate con-
states, we prefer the states in which fwire . In our case, sistent observation sequences. The second state machine is
only snow 0 satisfies this criterion. As there is only one di- the diagnoser built from the whole estimation model. It is
agnosis left, we do not need to apply preference (γ2 ). The also constrained by ∆, but it deterministically selects the
preferred single state is ŝ1 = estim(s0 , o1 ) = snow 0 = next state by applying Γ preferences. The verifier is the
product of these two state machines synchronized on ob-
light switch flight fwire . servable variables at each time step. Deadlock checking
then consists in checking whether there exists an observa-
4 Deadlock tion sequence that leads the verifier to a state in which the
A deadlock situation occurs when the diagnoser has previ- system has a successor state, but the diagnoser has none.
ously estimated a state ŝ different from the current system In order to distinguish the states of the two state machines
state s, and receives an observation o in contradiction with presented above, i.e. the state of the system and that of the
ŝ and ∆. In such a situation the candidates set for ŝ and o is diagnoser, we introduce two variable sets Psys and Pest that
empty and the diagnoser is unable to return a diagnosis. are direct copies of P. We also use a est_sat variable that
Definition 11 (Deadlock). An estimation model (s0 , ∆, Γ) indicates whether the diagnoser has a successor state.
is in a deadlock situation for an observation sequence Definition 12 (Verifier variables). The set of the verifier
(o0 , o1 , o2 , . . . , ok ) with k > 1 1 if and only if: variables is defined by Pverif = Psys ∪ Pest ∪ {est_sat},
1. there exists an estimated state sequence for where :
(o0 , . . . , ok−1 ), and • Psys = {p_sys | p ∈ P} is the set of variables describ-
2. there exist no estimated state sequence for (o0 , . . . , ok ) ing the system state ;
Example 4. Let (o0 , o1 , o2 , o3 ) be the observation sequence • Pest = {p_est | p ∈ P} is the set of variables describ-
produced by the system and along with the associated state ing the diagnoser state;
sequence (s0 , s1 , s2 , s3 ) described in Figure 2.
When observation o1 is received, Γ selects the preferred Step i oi si ŝi
state sˆ1 = light switch flight fwire . Then for observation 0 light switch flight fwire flight fwire
o2 , we are in the situation described in Example 3 and the
preferred state is ŝ2 = light switch flight fwire . Observation 1 light switch flight fwire flight fwire
o3 is in contradiction with the previously estimated state. In 2 light switch flight fwire flight fwire
fact the estimator has estimated flight in the previous state, 3 light switch flight fwire /
meaning that variable pre_flight is true. Rules of ∆ are not
consistent with such a configuration: (δ1 ) requires flight to
Figure 2: Deadlock scenario for Example 4. In columns si
1
There can be no deadlock at ŝ1 because we assume that the and ŝi , we omit variables from O whose values are identical
diagnoser is correctly initialized at s0 . to the column oi , and we only represent variables from E).
• est_sat indicates whether there is an estimated state estimated state sequence (ŝ0 , ŝ1 , . . . , ŝn−1 ) for the partial
for the diagnoser. sequence (o0 , o1 , . . . , on−1 ) and that there does not exist
A state of the verifier is an assignment on variables of Pverif . an estimated state sequence (ŝ0 , ŝ1 , . . . , ŝn ) for the com-
plete sequence. We then build the verifier’s state sequence
In order to define the state machine resulting from the (s0verif , s1verif , . . . , snverif ) as follows:
synchronous product, we successively define the initial state
of the verifier (Definition 13) and its transition relation (Def- • ∀i ∈ [0, n], ∀p ∈ P, siverif (p_sys) = si (p),
inition 14).
• ∀i ∈ [0, n − 1], ∀p ∈ P, siverif (p_est) = ŝi (p),
Definition 13 (Verifier initial state). The initial state s0verif
of the verifier is such that: • ∀i ∈ [0, n − 1], siverif (est_sat) = >,

• ∀p ∈ P, s0verif (p_sys) = s0 (p), • ∀p ∈ O, snverif (p_est) = on (p),
• ∀p ∈ E, snverif (p_est) = >,
• ∀p ∈ P, s0verif (p_est) = s0 (p),
• snverif (est_sat) = ⊥.
• s0verif (est_sat) = >.
verif
We show that for all i ∈ [0, n − 1], (siverif , si+1
verif
) is a tran-
Definition 14 (Verifier transition relation). Let spre and sition of the checker: let i be an integer in [0, n − 1], we
verif verif verif
snow be two verifier states. The pair (spre , snow ) is a show that the four parts of Definition 14 are satisfied:
verifier transition if and only if:
• ∀o ∈ O, ∀p ∈ P, si (p) = ŝi (p) and si+1 (p) =
(1) variables associated with observations take the same ŝi+1 (p). Equation (1) holds;
value on system and diagnoser sides,
• equation (2) holds by construction of the verifier;
(2) the system transition described by variables of Psys sat-
isfies ∆, • for i < n − 1, siverif (est_sat) = > and (ŝi , ŝi+1 ) is
the pair of states in ∆ satisfying equation (3);
(3) the variable est_sat indicates whether there exists a
possible estimated state (i.e. if the candidates set is not • for i = n − 1, the definition of a deadlock implies
empty), and that there does not exist a pair of states satisfying ∆:
equation (3) is satisfied;
(4) if est_sat is true, then the diagnoser transition de-
scribed by variables of Pest satisfies ∆ and Γ. • for i < n − 1, siverif (est_sat) = > and (ŝi , ŝi+1 ) is
the pair of states in ∆ satisfying equation (4);
Formally :
verif verif
For the reciprocal, let us assume that the checker has a
∀o ∈ O, spre (sys_o) = spre (est_o) and path in which est_sat is false. We consider such a path
(1)
verif
∀o ∈ O, snow verif
(sys_o) = snow (est_o) (s0verif , s1verif , . . . , snverif ) in wich snverif is the only state
in which false is assigned to est_sat. We then build two
∃(spre , snow ) ∈ ∆, ∀p ∈ P, states sequences (s0 , s1 , . . . , sn ) and (s0 , ŝ1 , . . . , ŝn−1 ) as
verif
spre (p) = spre (sys_p) and (2) follows:
verif
snow (p) = snow (sys_p) • ∀i ∈ [0, n], ∀p ∈ P, si (p) = siverif (p_sys),
est_sat
 ↔  • ∀i ∈ [0, n − 1], ∀p ∈ P, ŝi (p) = siverif (p_est)
∃(spre , snow ) ∈ ∆, We prove that these state sequences are consistent with ∆.
verif
∀p ∈ P, spre (p) = spre (est_p) and  (3)
From Definition 14, est_sat is false (last time step) im-

 
verif
∀p ∈ O, snow (p) = snow (est_p) plies that no state snow allows to satisfy the right part of the
condition (equation 3) for spre = ŝn−1 . This means that
est_sat → no state meets the Definition 6. There is a deadlock for the
∃(spre , snow ) ∈ ∆, ∀p ∈ P,
 
observation sequence generated by (s0 , s1 , . . . , sn ).
verif
 spre (p) = spre (est_p) and 
5.2 Choice of the model-checker
 
verif
snow (p) = snow (est_p) and
 
 
 (4) Model-checking is a set of techniques and computer tools
  
 6 ∃sbest ∈ S,
  for checking properties on systems. Among the many
∀o ∈ O, sbest (o) = snow (o), and
  

  
 model-checkers in the literature, NuSMV [14] and NuXMV
(spre , sbest ) ∈ ∆, and

   are known for their effectiveness in checking temporal prop-
(spre , sbest ) ≺Γ (spre , snow ) erties on dynamic systems. They are based on temporal
logic like LTL or CTL. Another family of model checkers is
Proposition 2. An estimation model (s0 , ∆, Γ) is subject to specialized in checking properties on structurally complex
a deadlock if and only if the associated verifier contains a models, but without temporal dynamics. This is the case
path in which est_sat is false. The deadlock scenario is of the Alloy Analyzer model-checker [15] which supports a
the observation sequence corresponding to the states of the fragment of first order logic.
verifier. In the case of deadlock verification, we need to express
the temporal dynamics of the system but also the prefer-
Proof Suppose that the estimation model is subject to a ences of the diagnoser, which are not easily expressed in
deadlock. According to Definition 11, there exists an ob- propositional logic. We therefore chose to use the model-
servation sequence (o0 , o1 , . . . , on ) generated by a consis- checker E LECTRUM [1] which is based on the Alloy lan-
tent state sequence (s0 , s1 , . . . , sn ), such that there is an guage and integrates temporal dynamics as in NuSMV.
5.3 Quantified form of preference pred delta[fwire,light,flight,
switch,preF_flight : Bool] {
The concept of preference is part of the verifier definition. (isTrue[preF_flight] => isTrue[flight])
This means that the model-checker language must allow to and
express them. To do so, we define a quantified form for (isTrue[light] <=> ( isTrue[switch] and
preferences. !isTrue[flight] and
!isTrue[fwire]))
Definition 15 (Preference quantified form). Let be Γ = }
(γ1 , . . . , γn ) a preference model in which each preference var one sig RealSystem {
has form γi = condi : ei ≺ ei . The quantified form of γi is var fwire : Bool,
var preF_fwire : Bool,
the formula ψi defined by: var light : Bool,
var flight : Bool,
ψi = (∀ei , ∃ei+1 , . . . , en , ∆) → (ei ↔ condi ) var switch : Bool,
var preF_flight : Bool,
The quantified form ψi is composed of two parts. The left }
part is only satisfied when for both truth values variable ei , fact always_delta_RealSystem {
there is a way to assign the target variables of the following always {
preferences and still satisfy ∆. It represents the cases when delta[RealSystem.fwire,
RealSystem.preF_fwire,
the preference is actually applied. The right part expresses RealSystem.light,
the effect of the preference, i.e that ei is assigned to true RealSystem.flight,
if and only if the condition condi is satisfied. Through the RealSystem.switch,
following proposition, we show that Γ preferences and their RealSystem.preF_flight]}
}
quantified form are equivalent from the point of view of the fact synch_obs {
estimated state for a previous state and an observation. always {
Proposition 3. For a previous estimated state ŝpre , an Estimator.light = RealSystem.light
Estimator.switch = RealSystem.switch}
observation o, a candidate ŝ ∈ S∆ (ŝpre , o), ŝ = }
estim(ŝpre , V
o) if and only if the assignment σŝpre ,ŝ satisfies
conjunction i∈[1,n] ψi .
Proof. Let ŝpre be a previous estimated state, o an ob- Figure 3: The observed system and observation synchro-
servation and ŝ a state in S∆ (ŝpre , o). We inductively show nization in E LECTRUM.
that ŝ is preferred for the preference sequence V (γ1 , . . . , γk )
if and only if the assignment σŝpre ,ŝ satisfies i∈[1,k] ψi . and s 0 such that for all i < k, s(ei ) = s 0 (ei ) and s(ek ) 6=
For k = 1, the set of free variables in formula lhs1 = s 0 (ek ). Between these two states, the one in which condk ↔
∀e1 , ∃e2 , . . . en , ∆ is the set O, since all the variables in E ek is true is the preferred state by preference γk . As the
are quantified. The formula lhs1 is satisfied by an observa- states preferred by γk are exactly the ones for which the
tion o if and only if both oe1 and oe1 have an extension in assignment σŝpre ,ŝ satisfies ψk , thus the induction is valid at
P ∪ Ppre that satisfies ∆. This means S∆ (ŝpre , o) contains index k.
at least two states s and s 0 with s(e1 ) 6= s 0 (e1 ). Among
these two states, the one that satisfies cond1 ↔ e1 is the 5.4 Model Encoding with E LECTRUM
preferred state by preference γ1 , and also satisfies ψ1 . As In this section, we illustrate how the verifier defined in Def-
the states preferred by γ1 are exactly the ones for which the inition 13 and 14 is encoded in E LECTRUM. We illustrate
assignment σŝpre ,ŝ satisfies ψ1 , then the proposition holds the encoding of the system described in Examples 1 and 3.
for k = 1. To model the system’s state machine, we declare a predi-
Let k > 1 and let us assume that the induction is valid cate corresponding exactly to the model ∆ then we declare
at index k − 1, i.e. that ŝ is preferred for the prefer- a constraint (a fact in E LECTRUM) that specifies that the
ence sequence (γV1 , . . . , γk−1 ) if and only if the assignment system respects the predicate at all time steps (always in
σŝpre ,ŝ satisfies i∈[1,k−1] ψi . Since s and s 0 belong to E LECTRUM), as illustrated in Figure 3. A similar constraint
S∆ (ŝpre , o), since s is a state is declared for the diagnoser’s state machine. Finally, we
V preferred for (γ1 , . . . , γk−1 ) synchronize the variables from O of the observed system
and since σŝpre ,s 0 satisfies i∈[1,k−1] ψi , then for all i < k,
with those of the second state machine representing our es-
s(ei ) = s 0 (ei ). timator, as expressed in condition (1) of Definition 14.
The set of free variables in formula lhsk = To represent the temporal aspect of our formalism, we use
∀ek , ∃ek+1 , . . . en , ∆ is the set O ∪ {ei | i < k}. An assign- the operator ’ from E LECTRUM which describes a variable
ment op to these variables satisfies lhsk if and only if op ek at the next time step. Figure 4 reproduces the intention of
and op ek both have an extension to P ∪ Ppre that satisfies the bijective function pre (p_pre value at next state is equal
∆. to p value at current state).
If for a given assignment op to O ∪ {ei | i < k} the for- E LECTRUM supports the use of relational algebra opera-
mula lhsk does not hold, then for all s and s 0 in S∆ (ŝpre , o), tors. It is possible for each preference to write a predicate
s(ek ) = s 0 (ek ). Thus, the preference γk is not applied and telling us if a preference γi is applicable, that is, if the two
the preferred states for (γ1 , . . . , γk−1 ) are the also preferred valuations for variable ei (operator all), and at least one
for (γ1 , . . . , γk ). In thisVcase, ψk = > and the states s 0 possible valuation for variables ej , i < j ≤ n (operator
such that σŝpre ,s 0 satisfy i∈[1,k−1] ψi are the same ones for some) are consistent with ∆ an the observation. This corre-
V
which σŝpre ,s 0 satisfy i∈[1,k] ψi and the induction is valid. sponds to the left part of the quantified form of a preference.
If for a given assignment op to O∪{ei | i < k} the formula Figure 5 illustrates the definition of predicates that imple-
lhsk holds, then S∆ (ŝpre , o) contains at least two states s ment these conditions with E LECTRUM operators. The rest
fact next_Estimator { (the robot takes several time steps to go through the cell)
always { and dangerous cells (robot stays forever on the cell).
Estimator.preF_flight’ =
Estimator.flight We observe at every moment the position of robots on
Estimator.preF_fwire’ = the grid and their destination. We estimate the presence of
Estimator.fwire } 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 pre-
Figure 4: Temporal dynamics in E LECTRUM. ferring the absence of a permanent fault).
Models are written in Scala language and are automati-
pred pref_fwire_possible{ cally translated into E LECTRUM. E LECTRUM proceeds to
all fwire : Bool |some flight : Bool | the verification through different solvers. For our experi-
delta[fwire,
Estimator.preF_fwire, ments, we set E LECTRUM to use the Sat4j solver [16]. Ver-
Estimator.light, ifications were performed on a 3.5GHz Intel Core i5-7600
flight, quad-core processor. Figure 6 shows the results of our ex-
Estimator.switch, periments for different mission parameters.
Estimator.preF_flight]
} The first conclusion is that verification is faster for mod-
pred pref_fwire_applied{ els that are subject to deadlock scenarios than for those that
isTrue[Estimator.fwire] <=> do not encounter such scenarios. This difference is directly
isTrue[Estimator.preF_fwire] related to the fact that when the model-checker finds a dead-
}
pred pref_flight_possible{ lock scenario in the model, the search ends immediately and
all flight : Bool | it returns a counterexample corresponding to the sequence
delta[Estimator.fwire, of observations. On the contrary, to prove that a model
Estimator.preF_fwire, contains no deadlock scenarios, E LECTRUM explores many
Estimator.light, more possible executions paths for the verifier.
flight,
Estimator.switch, We can then see that the verification is very fast for the
Estimator.preF_flight] first models, but as we enrich P, ∆ and Γ, the number of
} variables generated for Sat4j and the time required for verifi-
pred pref_flight_applied{ cation increases exponentially. For examples of larger sizes,
isTrue[Estimator.flight] <=>
isTrue[False] it is interesting to note that Sat4j did not have enough mem-
} ory to process them.
fact prefs { Deadlock detection as proposed in the paper is carried
always {
pref_flight_possible implies out in the design phase. Hence, high calculation times are
pref_flight_applied not necessarily unacceptable and do not call into question
pref_fwire_possible implies the approach we propose. Let us notice that the results we
pref_fwire_applied present here are preliminary results and we are currently
} working on different ways to improve them. Specifically,
}
we aim to integrate E LECTRUM more closely to avoid the
creation of boolean variables where E LECTRUM could han-
Figure 5: Implementing preferences in E LECTRUM dle enumerated variables.

of the preferences are described by a fact. 7 Conclusion and future work
The order in which preferences are applied in Γ, is com- We have developed a generic method to validate the proper
pletely induced by the quantification overlays in the quanti- behavior of a diagnoser at design stage. In particular, we
fied forms of preferences (see Definitions 8 and 15). have showed that it is possible to anticipate deadlock situa-
tions.
6 Experimental results In this paper, we do not introduce any mechanism to iden-
We experimented our approach on the model of a multi- tify the causes and modify the estimation model in order to
robot mission of customizable size and complexity. eliminate deadlock scenarios, but this remains a goal for fu-
In this mission, one or more robots move on a rectangular ture work. In particular, there are several ways to treat a
grid of variable size, each robot moves towards its destina- deadlock scenario. One can ignore it, as in the deadlocking
tion. The destination can change during the mission accord- path the system should stop autonomous operation and wait
ing to unspecified dynamics. for operator intervention. One can alter the system’s be-
Behavioral constraints are declared in ∆ for each robot. haviour or instrumentation, which is costly and sometimes
robots should move unless they are at their destination. impossible. Finally, one can revise the fault management
Moreover, robots may be subject to permanent and / or in- strategy, by changing the preference ordering, or simply di-
termittent faults. An intermittent fault slows down or im- agnosing other elements of the system, such as whether we
mobilizes the robot for a few moments which is modelled trust a component instead of its real health status.
by the fact that a robot takes several time steps to cross a In addition, we plan to reuse the automation of model-
cell. A permanent fault immobilizes the robot permanently. checking allowing us to verify the existence of deadlock sce-
We also estimate the state of the terrain. A robot crosses a narios for our diagnosers to check other properties related to
normal cell in one time step, but we introduce difficult cells diagnosis such as diagnosability.
ID nb of robots grid size kPk k∆k kΓk CNF vars CNF clauses deadlock no deadlock
1 1 1x2 13 17 7 1083 1586 0,1s 0,8s
2 1 2x2 21 27 11 3400 3925 0,5s 4,8s
3 1 2x3 29 37 15 13757 10593 7,3s 52,9s
4 2 2x2 34 50 14 12631 13561 6,7s 60,5s
5 2 2x3 46 68 18 65 030 47 669 144,6s 1001,4s

Figure 6: E LECTRUM model checking. Columns kPk, k∆k and kΓk indicate respectively the number of variables of P, the
number of rules of ∆ and the number of preferences in Γ. Columns 7 and 8 indicate respectively the number of variables and
clauses sent to solver Sat4j by E LECTRUM. The last two columns indicate the verification time for a version of the model
subject to a deadlock scenario and another version for which such a scenario does not exist.

Finally, progress on model-checker performance is the Principles of Diagnosis (DX 2010), Portland, OR,
needed to apply it to multi-robot missions involving large USA, pages 31–38, 2010.
models. QBF solvers [17] are potential tools for finding [9] Johan De Kleer. Diagnosing multiple persistent and
deadlock scenarios of bounded length, as can express the intermittent faults. In Proceedings of the 21st interna-
quantified form of our conditional preferences. It is thus tional jont conference on Artifical intelligence, pages
possible to express the presence of a deadlocking path of 733–738. Morgan Kaufmann Publishers Inc., 2009.
bounded length as a QBF satisfiability problem.
[10] Olivier Contant, Stéphane Lafortune, and Demosthe-
References nis Teneketzis. Diagnosis of intermittent faults. Dis-
crete Event Dynamic Systems, 14(2):171–202, 2004.
[1] Nuno Macedo, Julien Brunel, David Chemouil, Alcino
[11] Edmund M. Clarke, Jr., Orna Grumberg, and Doron A.
Cunha, and Denis Kuperberg. Lightweight specifica-
tion and analysis of dynamic systems with rich con- Peled. Model Checking. MIT Press, Cambridge, MA,
figurations. In Proceedings of the 2016 24th ACM USA, 1999.
SIGSOFT International Symposium on Foundations [12] Craig Boutilier, Ronen I Brafman, Carmel Domsh-
of Software Engineering, FSE 2016, pages 373–383, lak, Holger H Hoos, and David Poole. Cp-nets: A
New York, NY, USA, 2016. tool for representing and reasoning with conditional
[2] Meera Sampath, Raja Sengupta, Stéphane Lafortune, ceteris paribus preference statements. J. Artif. Intell.
Kasim Sinnamohideen, and Demosthenis Teneketzis. Res.(JAIR), 21:135–191, 2004.
Diagnosability of discrete-event systems. IEEE Trans- [13] Alessandro Cimatti, Charles Pecheur, and Roberto
actions on automatic control, 40(9):1555–1575, 1995. Cavada. Formal verification of diagnosability via sym-
[3] Craig Boutilier, Ronen I Brafman, Carmel Domshlak, bolic model checking. In Proceedings of the 18th in-
Holger H Hoos, and David Poole. Preference-based ternational joint conference on Artificial intelligence,
constrained optimization with cp-nets. Computational pages 363–369. Morgan Kaufmann Publishers Inc.,
Intelligence, 20(2):137–157, 2004. 2003.
[4] Cedric Pralet, Xavier Pucel, and Stéphanie Roussel. [14] Alessandro Cimatti, Edmund Clarke, Fausto
Diagnosis of intermittent faults with conditional pref- Giunchiglia, and Marco Roveri. Nusmv: a new
erences. In Proceedings of the 27th International symbolic model checker. International Journal on
Workshop on Principles of Diagnosis (DX’16), 2016. Software Tools for Technology Transfer, 2(4):410–
425, Mar 2000.
[5] Xavier Pucel and Stéphanie Roussel. Intermittent fault
[15] Daniel Jackson. Software Abstractions: Logic, Lan-
diagnosis as discrete signal estimation: Trackability
analysis. In Proceedings of the 28th International guage, and Analysis. The MIT Press, 2006.
Workshop on Principles of Diagnosis (DX’17), 2017. [16] Daniel Le Berre and Anne Parrain. The sat4j library,
[6] James Kurien and P Pandurang Nayak. Back to the fu- release 2.2, system description. Journal on Satisfia-
ture for consistency-based trajectory tracking. In Pro- bility, Boolean Modeling and Computation, 7:59–64,
ceedings of the Seventeenth National Conference on 2010.
Artificial Intelligence, pages 370–377, 2000. [17] Massimo Narizzano, Luca Pulina, and Armando Tac-
[7] Marie-Odile Cordier, Philippe Dague, François Lévy, chella. The qbfeval web portal. In Logics in Artificial
Jacky Montmain, Marcel Staroswiecki, and Louise Intelligence, pages 494–497. Springer Berlin Heidel-
Travé-Massuyès. Conflicts versus analytical redun- berg, 2006.
dancy relations: a comparative analysis of the model
based diagnosis approach from the artificial intelli-
gence and automatic control perspectives. IEEE Trans-
actions on Systems, Man, and Cybernetics, Part B (Cy-
bernetics), 34(5):2163–2177, 2004.
[8] Alexander Felfernig and Monika Schubert. Fastdiag:
A diagnosis algorithm for inconsistent constraint sets.
In Proceedings of the 21st International Workshop on