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. 2
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. 3
Our diagnosis model is a tuple (s0 ; ; ), where s0 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. 3.1
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 f>; ?g that associates to each variable x from X the boolean value true (>) or false (?). We write x and x the assignments to fxg such that x (x) = > and x (x) = ?. For a set of variables X = fx1, : : :, xng, if for i 2 [1; n], fi is an assignment fxig ! f>; ?g, then f1 f2 : : : fn denotes the f assignment on X such that 8xi 2 X; f (xi) = fi(xi). For example, a b c is the assignment to fa; b; cg 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. 3.2
The behavioral model S2 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 Ppre = fpre_p j p 2 Pg such that 8p 2 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 Ppre.
A pair of states (spre ; snow ) belongs to the transition relation when the system can be in the state spre at time t 1 and in the state snow at time t. To formally link to p, for any pair of states (spre ; snow ), we define the assignment spre;snow on variables from P [ Ppre such that 8p 2 P; spre;snow (p) = snow (p) and spre;snow (pre(p)) = switch
light fwire spre (p). We consider that a pair of states belongs to the transition relation if and only if the corresponding assignment satisfies the formulas of p.
spre;snow j= Definition 3 (Transition). A pair of states (spre ; snow ) 2 S2 is a transition, denoted (spre ; snow ) 2 , if and only if p.
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.
Definition 4 (Consistent state sequence). A state sequence (s0 ; s1 ; : : : ; sn ) 2 Sn is consistent if and only if 8i 2 [1; n]; (si 1; si) 2 .
Definition 5 (Consistent observation sequence). An observation sequence (o0; o1; : : : ; on) is consistent if and only if there exist a consistent state sequence (s0; s1; : : : ; sn) such that 8i 2 [0; n]; 8o 2 O; si (o) = oi(o).
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 (spre ; o) of diagnosis candidates for a previous state spre and an observation o is defined by:
S (spre ; o) = snow 2 S j(spre ; snow ) 2 and 8o 2 O; snow (o) = o(o) 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: fwire represents an intermittent loose contact in the wire and flight 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 flight is permanent. In the initial state s0 = light switch flight fwire , the lamp glows and there is no fault. light $ switch ^ :flight ^ :fwire ( 1)
pre_flight ! flight ( 2) fsnow; s0now; s0n0owg with:
From the behavioral model , we can calculate diagnosis candidates. For instance, at time step 1, s0 is the previous system state, let us consider the observation o1 = light switch. The candidate states set is S (s0 ; o1) = snow s0now s0n0ow = = = light switch flight fwire light switch flight fwire light switch flight fwire In the state snow, the intermittent fault is present alone; in s0now, the permanent fault is present alone; both faults are present in s0n0ow. 3.3
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 (spre ; 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 [ Ppre. 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 spre ; s; s0 2 S3, strictly prefers the transition (spre ; s) to transition (spre ; s0) (denoted (spre ; s) (spre ; s0)) if and only if spre ;s j= cond $ e and spre ;s0 2 cond $ e. Transitions (spre ; s) and (spre ; s0) are equivalent to (denoted (spre ; s) (spre ; s0)) if and only if ( spre ;s j= cond $ e) , ( spre ;s0 j= cond $ e).
Example 2. Let us consider the preference = :light : flight . This preference indicates that if both flight flight and flight are part of some diagnosis candidate, then flight is preferred if and only if :light holds. Formally, we prefer diagnoses that satisfy :light $ flight. For the states snow, s0now and s0n0ow in Example 1, as :light holds, we prefer the states in which flight holds, i.e. the states s0now and s0n0ow. Formally, s0now snow, s0n0ow snow and s0n0ow
s0now.
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.
Definition 8 (Conditional preference model). A conditional preference model is a sequence of conditional preferences ( 1; 2,.., n) with i = condi : ei ei for i 2 [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, 8i 2 [1; n] , the scope of the condition condi is a subset of Ppre [ O [ fejj1 j < ig.
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 (spre ; snow ) and (spre 0; snow 0) that have the same previous state (i.e. spre = spre 0) and whose successor states produce the same observation (i.e. 8o 2 Osnow (o) = snow 0(o)).
Formally, 8spre ; s; s0 2 S3, (spre ; s) is strictly preferred to (spre ; s0) by (denoted (spre ; s) (spre ; s0)) if and only if there exists i 2 [1; n] such that for all j < i, j (spre ; s0) and (spre ; s) i (spre ; s0). (spre ; s)
Although the order is partial on S2, 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 spre be a state, o an observation, a behavioral model and a preference model. If s and s0 are two candidate states for spre and o (s; s0 2 S (spre ; o)2) such that s 6= s0 then we have either (spre ; s) (spre ; s0) or (spre ; s0) (spre ; s).
Proof By Definition 6, s and s0 belong to S (spre ; o) implies that 8o 2 O; s(o) = s0(o). Therefore, s 6= s0 means that there is a variable e 2 E such that s(e) 6= s0(e). So, there exists a preference 2 such that s s0 does not hold. Let i be the index of the first preference of the sequence in this case. Formally, i is such that 8j < i, (spre ; s) j (spre ; s0), (spre ; s) i (spre ; s0) does not hold. This means that (spre ; s) i (spre ; s0) or (spre ; s0) i (spre ; s). From the order , we then have (spre ; s) (spre ; s0) or (spre ; s0) (spre ; s). 3.4
At each step, given the set of candidate states S (spre ; o) we select the state preferred by the conditional preference model .
Definition 9 (Estimated state). The estimated state s^ = estim(spre ; o) for a previous state spre and an observation o is the element of S (spre ; o) preferred by . Formally, s^ = estim(spre ; o) if and only if: 1. s^ 2 S (spre ; o), and 2. 8snow 2 S (spre ; o) such that snow 6= s^, we have (spre ; ^s) (spre ; snow ).
From the initial state s0 , we now define the sequence of estimated states that is produced by the diagnoser for a given observation sequence.
Definition 10 (Estimated state sequence). A state sequence (s0; ^s1 ; ^s2 , ..., ^sk ) is the estimated state sequence for the observation sequence (o0; o1; o2,...,ok) if and only if 8i 2 [1; k]; ^si = estim(^si 1 ; oi).
Example 3. Let us associate the lamp model ple 1 to the following preferences: from Exam= pre_fwire : fwire ? : flight fwire
The first preference ( 1) declares that we prefer the value for fwire that was estimated at the previous time step. This mechanism makes it possible to bring some stability to the diagnosis since fwire is an intermittent fault: if allows both diagnoses for fwire, 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 flight is absent.
In Example 1, with s0 = light switch flight fwire ) as the previous state and o1 = light switch as the observation, the set of diagnosis candidates S (spre ; o) contains the three states snow = light switch flight fwire , snow 0 = light switch flight fwire and s0n0ow = light switch flight fwire .
By applying ( 1) first, as pre_fwire holds in the three states, we prefer the states in which fwire . In our case, only snow 0 satisfies this criterion. As there is only one diagnosis left, we do not need to apply preference ( 2). The preferred single state is ^s1 = estim(s0; o1) = snow 0 = light switch flight fwire . 4
A deadlock situation occurs when the diagnoser has previously estimated a state s^ different from the current system state s, and receives an observation o in contradiction with s^ and . In such a situation the candidates set for s^ and o is empty and the diagnoser is unable to return a diagnosis. Definition 11 (Deadlock). An estimation model (s0; ; ) is in a deadlock situation for an observation sequence (o0; o1; o2, . . . , ok) with k > 1 1 if and only if: 1. there exists an estimated state sequence for (o0; : : : ; ok 1), and 2. there exist no estimated state sequence for (o0; : : : ; ok) Example 4. Let (o0; o1; o2; o3) be the observation sequence produced by the system and along with the associated state sequence (s0; s1; s2; s3) described in Figure 2.
When observation o1 is received, selects the preferred state s^1 = light switch flight fwire . Then for observation o2, we are in the situation described in Example 3 and the preferred state is ^s2 = light switch flight fwire . Observation o3 is in contradiction with the previously estimated state. In fact the estimator has estimated flight in the previous state, meaning that variable pre_flight is true. Rules of are not consistent with such a configuration: ( 1) requires flight to 1There can be no deadlock at s^1 because we assume that the diagnoser is correctly initialized at s0. be false because the lamp glows while ( 2) requires flight to be true since the associated fault is permanent.
Therefore, there is an estimated state sequence for (o0 ; o1 ; o2 ): this is the sequence (s0 ; ^s1 ; ^s2 ). However, since there is no estimated state sequence for (o0 ; o1 ; o2 ; o3 ), 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. 5
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 Psys and Pest 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 Pverif = Psys [ Pest [ fest_satg, where :
Psys = fp_sys j p 2 Pg is the set of variables describing the system state ; Pest = fp_est j p 2 Pg is the set of variables describing the diagnoser state; Step i 0 1 2 3
oi light switch light switch light switch light switch
si flight fwire flight fwire flight fwire flight fwire ^si / flight fwire flight fwire flight fwire est_sat indicates whether there is an estimated state for the diagnoser.
A state of the verifier is an assignment on variables of Pverif.
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).
Definition 13 (Verifier initial state). The initial state s0verif of the verifier is such that: 8p 2 P, s0verif (p_sys) = s0 (p), 8p 2 P, s0verif (p_est) = s0 (p), s0verif (est_sat) = >.
Definition 14 (Verifier transition relation). Let spvreerif and snveorwif be two verifier states. The pair (spvreerif ; snveorwif ) is a verifier transition if and only if: (1) variables associated with observations take the same value on system and diagnoser sides, (2) the system transition described by variables of Psys 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 Pest satisfies and .
Formally : 8o 2 O; spvreerif (sys_o) = spvreerif (est_o) and 8o 2 O; snvoerwif (sys_o) = snvoerwif (est_o) 9(spre ; snow ) 2 ; 8p 2 P; spre (p) = spvreerif (sys_p) and snow (p) = snvoerwif (sys_p) est_sat $ 0 9(spre ; snow ) 2 ; 1 B 8p 2 P; spre (p) = spvreerif (est_p) and C @ A 8p 2 O; snow (p) = snvoerwif (est_p) (1) (2) (3) 1 C C
C 1CCC (4)
C CCCACCCA est_sat ! 0 9(spre ; snow ) 2 ; 8p 2 P; spre (p) = spvreerif (est_p) and snow (p) = snvoerwif (est_p) and 0 6 9sbest 2 S; (spre ; sbest) 2 (spre ; sbest) ; and (spre ; snow ) Proposition 2. An estimation model (s0; ; ) is subject to a deadlock if and only if the associated verifier contains a path in which est_sat is false. The deadlock scenario is the observation sequence corresponding to the states of the verifier.
Proof Suppose that the estimation model is subject to a deadlock. According to Definition 11, there exists an observation sequence (o0 ; o1 ; : : : ; on ) generated by a consistent state sequence (s0 ; s1 ; : : : ; sn ), such that there is an estimated state sequence (^s0 ; ^s1 ; : : : ; ^sn 1 ) for the partial sequence (o0 ; o1 ; : : : ; on 1 ) and that there does not exist an estimated state sequence (^s0 ; ^s1 ; : : : ; ^sn ) for the complete sequence. We then build the verifier’s state sequence (s0verif ; s1verif ; : : : ; snverif ) as follows: 8i 2 [0; n]; 8p 2 P; siverif (p_sys) = si (p), for i < n 1, siverif (est_sat) = > and (^si ; ^si+1 ) 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; for i < n 1, siverif (est_sat) = > and (^si ; ^si+1 ) 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 (s0verif ; s1verif ; : : : ; snverif ) in wich sverif is the only state n in which false is assigned to est_sat. We then build two states sequences (s0 ; s1 ; : : : ; sn ) and (s0 ; ^s1 ; : : : ; ^sn 1 ) as follows: 8i 2 [0; n]; 8p 2 P; si (p) = siverif (p_sys), 8i 2 [0; n
1]; 8p 2 P; ^si (p) = siverif (p_est) We prove that these state sequences are consistent with . From Definition 14, est_sat is false (last time step) implies that no state snow allows to satisfy the right part of the condition (equation 3) for spre = ^sn 1 . This means that no state meets the Definition 6. There is a deadlock for the observation sequence generated by (s0 ; s1 ; : : : ; sn ). 5.2
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 = condi : ei ei . The quantified form of i is the formula i defined by: i = (8ei; 9ei+1; : : : ; en; ) ! (ei $ condi)
The quantified form i is composed of two parts. The left part is only satisfied when for both truth values variable ei, 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 ei is assigned to true if and only if the condition condi 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 ^spre , an observation o, a candidate s^ 2 S (^spre ; o), s^ = estim(^spre ; o) if and only if the assignment ^spre ;s^ satisfies conjunction Vi2[1;n] i.
Proof. Let ^spre be a previous estimated state, o an observation and s^ a state in S (^spre ; o). We inductively show that s^ is preferred for the preference sequence ( 1; : : : ; k) if and only if the assignment ^spre ;s^ satisfies Vi2[1;k] i.
For k = 1, the set of free variables in formula lhs1 = 8e1; 9e2; : : : en; is the set O, since all the variables in E are quantified. The formula lhs1 is satisfied by an observation o if and only if both oe1 and oe1 have an extension in P [ Ppre that satisfies . This means S (^spre ; o) contains at least two states s and s0 with s(e1) 6= s0(e1). Among these two states, the one that satisfies cond1 $ e1 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 ^spre ;s^ 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 s^ is preferred for the preference sequence ( 1; : : : ; k 1) if and only if the assignment ^spre ;s^ satisfies Vi2[1;k 1] i. Since s and s0 belong to S (^spre ; o), since s is a state preferred for ( 1; : : : ; k 1) and since ^spre ;s0 satisfies Vi2[1;k 1] i, then for all i < k, s(ei) = s0(ei).
The set of free
variables in formula lhsk = 8ek; 9ek+1; : : : en; is the set O [ fei j i < kg. An assignment op to these variables satisfies lhsk if and only if op ek and op ek both have an extension to P [ Ppre that satisfies .
If for a given assignment op to O [ fei j i < kg the formula lhsk does not hold, then for all s and s0 in S (^spre ; o), s(ek) = s0(ek). 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 s0 such that ^spre ;s0 satisfy Vi2[1;k 1] i are the same ones for which ^spre ;s0 satisfy Vi2[1;k] i and the induction is valid.
If for a given assignment op to O[fei j i < kg the formula lhsk holds, then S (^spre ; o) contains at least two states s pred delta[fwire,light,flight,
switch,preF_flight : Bool] { (isTrue[preF_flight] => isTrue[flight]) and (isTrue[light] <=> ( isTrue[switch] and !isTrue[flight] and !isTrue[fwire])) } var one sig RealSystem { var fwire : Bool, var preF_fwire : Bool, var light : Bool, var flight : Bool, var switch : Bool, var preF_flight : Bool, } fact always_delta_RealSystem { always { delta[RealSystem.fwire, RealSystem.preF_fwire, RealSystem.light, RealSystem.flight, RealSystem.switch,
RealSystem.preF_flight]} } fact synch_obs { always {
Estimator.light = RealSystem.light
Estimator.switch = RealSystem.switch} } and s0 such that for all i < k, s(ei) = s0(ei) and s(ek) 6= s0(ek). Between these two states, the one in which condk $ ek is true is the preferred state by preference k. As the states preferred by k are exactly the ones for which the assignment ^spre ;s^ 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 ei (operator all), and at least one possible valuation for variables ej; 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 of the preferences are described by a fact.
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). 6
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. 7
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. 1 2 3 4 5 1 1 1 2 2
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. nb of robots grid size deadlock
no deadlock 1586 3925 10593 13561 [13] Alessandro Cimatti, Charles Pecheur, and Roberto Cavada. Formal verification of diagnosability via symbolic model checking. In Proceedings of the 18th international joint conference on Artificial intelligence, pages 363–369. Morgan Kaufmann Publishers Inc., 2003. [16] Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2, system description. Journal on Satisfiability, Boolean Modeling and Computation, 7:59–64, 2010.
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg. Lightweight specification and analysis of dynamic systems with rich configurations. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, pages 373–383, New York, NY, USA, 2016.
Meera Sampath, Raja Sengupta, Stéphane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneketzis. Diagnosability of discrete-event systems. IEEE Transactions on automatic control, 40(9):1555–1575, 1995. Craig Boutilier, Ronen I Brafman, Carmel Domshlak, Holger H Hoos, and David Poole. Preference-based constrained optimization with cp-nets. Computational Intelligence, 20(2):137–157, 2004.
Cedric Pralet, Xavier Pucel, and Stéphanie Roussel. Diagnosis of intermittent faults with conditional preferences. In Proceedings of the 27th International Workshop on Principles of Diagnosis (DX’16), 2016. Xavier Pucel and Stéphanie Roussel. Intermittent fault diagnosis as discrete signal estimation: Trackability analysis. In Proceedings of the 28th International Workshop on Principles of Diagnosis (DX’17), 2017.
Marie-Odile Cordier, Philippe Dague, François Lévy, Jacky Montmain, Marcel Staroswiecki, and Louise Travé-Massuyès. Conflicts versus analytical redundancy relations: a comparative analysis of the model based diagnosis approach from the artificial intelligence and automatic control perspectives. IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), 34(5):2163–2177, 2004.
Alexander Felfernig and Monika Schubert. Fastdiag: A diagnosis algorithm for inconsistent constraint sets. In Proceedings of the 21st International Workshop on