We extend in this work the existing approach to analyse diagnosability in discrete event systems (DES) using satisfiability algorithms (SAT), in order to analyse the diagnosability in distributed DES (DDES) and we test this extension. For this, we handle observable and non observable communication events at the same time. We also propose an adaptation to use incremental SAT over the existing and the extended approaches to overcome some of the limitations, especially concerning the length and the distance of the cycles that witness the non diagnosability of the fault, and improve the process of dealing with the reachability limit when scaling up to large systems.
Diagnosis task is mainly using the available observations to explain the difference between the expected behavior of a system and its real behavior which may contain some faults. Many works have been done to study the automatic approaches to system fault diagnosis. They all try to deal with the main problem, i.e. the compromise between the number of possible diagnoses to the considered faults and the number of observations which must be given to make the decision. Diagnosis problem is NP-hard and one always needs to cope with an explosion in the number of system model states. Moreover, the diagnosis decision is not always certain, and thus running a diagnosis algorithm may not be accurate. For example, two sets of observations provided by different sets of sensors or at different times may lead to different diagnoses. This uncertainty raises the problem of diagnosability which is essential while designing the system model. After that, the model based diagnosis will be used in applications to explain any anomaly, with a guarantee of correctness and precision at least for anticipated faults. Diagnosability of the considered systems is a property defined to answer the question about the possibility to distinguish any possible faulty behavior in the system from any other behavior without this fault (i.e., correct or with a different fault) within a finite time after the occurrence of the fault. A fault is diagnosable if it can be surely identified from the partial observation available in a finite delay after its occurrence. A system is diagnosable if every possible fault in it is diagnosable. This property provides information before getting into finding the explanations of the fault. It also helps in designing a robust system against faults and in positioning the sensors to manage the observation requirements. The main difficulty in diagnosability algorithms is related to the states number explosion. Another difficulty appears when checking diagnosability of a system which is actually diagnosable, i.e. the inexistence of a counterexample witnessing non diagnosability. Thus all possibilities need to be tested as for proving the non existence of a plan in a planning problem, and usually in this case some approximations are used to avoid exploring all the search space.
The paper is structured as follows. Section 2 will introduce the system transition models for centralized DES and recall the traditional definition of the diagnosability in those models and the state of the art of encoding this definition as a satisfiability problem in propositional logic. Section 3 will present our first contribution, an extension of this state of the art to DDES with observable and non observable communication events in the same model, and will give experimental results of this extension. Section 4 is devoted to our second contribution, using incremental SAT calls to overcome the limitation when the number of steps required to check diagnosability, i.e., the length of possible paths with cycles witnessing non diagnosability, is large, and will present experimental results showing how the method scales up. Section 5 will present related works and section 6 will conclude and give our perspectives for future work. 2
We recall first the definitions of DES models we use and of diagnosability for these models. 2.1
We will use finite state machines (FSM) to model systems.
We define labeled transition systems following[
As we aim at studying the diagnosability of DDES using
SAT solvers, we will follow the model of [
It is straightforward to show that any LTS can be
represented as an SLTS (one takes dlog(|X|)e Boolean variables
and represents states by different valuations of these
variables; one assigns to each occurence of an event e labeling
a transition (x, e, y) a pair hφ, ci, with φ expressing the
valuation of x and c the valuation changes between x and
y). And reciprocally any SLTS can be mapped to an LTS
(see Definition 2.4 in[
The formal definition of diagnosability of a fault f in a
centralized system modeled by (an LTS or SLTS) T was
proposed by [
able in a system T iff ∃k ∈ N, ∀sf ∈ L(T ), ∀t ∈ L(T )/sf , |t| ≥ k ⇒ A fault f is diagnos∀p ∈ L(T ), (P (p) = P (sf .t) ⇒ f ∈ p).
In this formula, L(T ) denotes the prefix-closed language of T whose words are called trajectories, sf any trajectory ending by the fault f , L(T )/s the post-language of L(T ) after s, i.e., {t ∈ Σ∗|s.t ∈ L(T )} and P the projection of trajectories on observable events. The above definition states that for each trajectory sf ending with fault f in T , for each t that is an extension of sf in T with enough events, every trajectory p in T that is equivalent to sf .t in terms of observation should contain in it f . As usual, it will be assumed that L(T ) is live (i.e., for any state, there is at least one transition issued from this state) and convergent (i.e., there is no cycle made up only of unobservable events).
A system T is said to be diagnosable iff any fault f ∈ Σf
is diagnosable in T . In order to avoid exponential
complexity in the number of faults during diagnosability analysis,
only one fault at a time is checked for diagnosability. It will
thus be assumed in the following that there exists only one
fault event f (Σf = {f }), without restriction on the
number of its occurrences. Diagnosability checking has been
proved in [
An immediate rephrasing of the definition 3 shows thatT is
non diagnosable iff it exists a pair of trajectories
corresponding to cycles (and thus to infinite paths), a faulty one and
a correct one, sharing the same observable events. Which
is equivalent to the existence of an ambiguous (i.e. made
up of pairs of states respectively reachable by a faulty path
and a correct path) cycle in the product of T by itself,
synchronized on observable events, which is at the origin of the
so called twin plant structure introduced in [
The following formulas express the constraints that must be applied at each time step t or between t and t + 1. 1. The event occurrence eto must be possible in the current state: eto → φ t
for o = hφ, ci ∈ δ(e) and its effects must hold at the next time step: eto → ^ lt+1 l∈c for o = hφ, ci ∈ δ(e) (2.1) (2.2)
2. The present value (T rue or F alse) of a state variable changes to a new value (F alse or T rue, respectively) only if there is a reason for this change, i.e., because of an event that has the new value in its effects (so, change without reason is prohibited). Here is the change from T rue to F alse (the change from F alse to T rue is defined similarly by interchanginga and ¬a): (at ∧ ¬at+1) → (eit1oj1 ∨ · · · ∨ eitkojk ) (2.3) where the ojl = hφjl , cjl i ∈ δ(eil ) are all the occurrences of events eil with ¬a ∈ cji .
We have the same formulas with aˆt and eˆt . ilojl 3. At most one occurrence of a given event can occur at a time and the occurrences of two different events cannot be simultaneous if they interfere (i.e., if they have two contradicting effects or if the precondition of one contradicts the effect of the other): ¬(eto ∧ eto0) ¬(eto ∧ e0ot0) ∀o0 ∈ δ(e0) such that o and o0 interfere ∀{e, e0} ⊆ Σ, e 6= e0, ∀o ∈ δ(e), ∀e ∈ Σ, ∀{o, o0} ⊆ δ(e), o 6= o0 (2.4) (2.5) We have the same formulas with eˆt . o 4. The formulas that connect the two events sequences require that observable events take place in both sequences whenever they take place (use of et): _ eto ↔ et and _ eˆto ↔ e t ∀e ∈ Σo (2.6) o∈δ(e)
o∈δ(e) I0 =
(a0 ∧aˆ0) ∧ a∈A,s0(a)=1
a∈A,s0(a)=0
The conjunction of all the above formulas for a given t is denoted by T (t, t + 1).
A formula for the initial state s0 is: ^ ^ (¬a0 ∧¬aˆ0) (2.7)
At last, the following formula can be defined to encode the fact that a pair of executions is found with the same observable events and no fault in one execution (first line), but one fault in the other (second line), which are infinite (in the form of a non trivial cycle, so containing at least one observable event, 1 at step n; third line), witnessing non diagnosability: ΦTn =
I0 ∧ T (0, 1) ∧ · · · ∧ T (n − 1, n) ∧
From this encoding in propositional logic, follows the
result (theorem 3.2 of [
We extend from centralized systems to distributed systems the satisfiability framework of subsection 2.2 for testing diagnosability and we provide some experimental results.
1This verification that the cycle found is not trivial was not done
in [
In order to model DDES with SLTS, we need to extend these ones by adding communication events to each component. So we use the following definition for a distributed SLTS with k different components (sites):
System (DSLTS) with k components is described by a tuple
T = hA, Σo, Σu, Σf , Σc, δ, s0i where (subscripts i refer to
component i):
• A is a union of disjoint finite sets (Ai)1≤i≤k of
comk
ponent own state variables, A = ∪i=1Ai,
• Σo is a union of disjoint finite sets of component own
k
observable correct events, Σo = ∪i=1Σoi,
• Σu is a union of disjoint finite sets of component own
k
unobservable correct events, Σu = ∪i=1Σui,
• Σf is a union of disjoint finite sets of component own
k
unobservable faulty events, Σf = ∪i=1Σf i,
• Σc is a union of finite sets of (observable or
unobservable) correct communication events, Σc = ∪ik=1Σci,
which are the only events shared by at least two
different components (i.e., ∀i, ∀c ∈ Σci, ∃j 6= i, c ∈ Σcj ),
• δ = (δi), where δi : Σi = Σoi ∪ Σui ∪ Σf i ∪ Σci →
2Li×2Li , assigns to each event a set of pairs hφ, ci in
the propositional language of the component where it
occurs (so, for communication events, in each
component separately where they occur),
• s0 = (s0i) is the initial state (a valuation of each Ai).
In this distributed framework, synchronous communication
is assumed, i.e., communication events are synchronized
such that they all occur simultaneously in all components
where they appear. More precisely, a transition by a
communication event c may occur in a component iff a
simultaneous transition by c occurs in all the other components
where c appears (has at least one occurrence). In particular,
all events before c in trajectories in all these components
necessarily occur before all events after c in these
trajectories. The global model of the system is thus nothing else that
the product of the models of the components, synchronized
on communication events. Notice that we allow in whole
generality communication events to be, partially or totally,
unobservable, so one has in general to wait further
observations to know that some communication event occurred
between two or more components. On the other side,
assuming these communications to be faultless is not actually
a limitation. If a communication process or protocol may be
faulty, it has just to be modeled as a proper component with
its own correct and faulty behaviors (the same that, e.g., for
a wire in an electrical circuit). In this sense,
communications between components are just a modeling concept, not
subject to diagnosis. It will be also assumed that the
observable information is global, i.e. centralized (when observable
information is only local to each component, distributed
diagnosability checking becomes undecidable [
Let T be a DSLTS made up of k components denoted by indexes i, 1 ≤ i ≤ k. In order to express the diagnosability analysis of T as a satisfiability problem, we have to extend the formulas of subsection 2.2 to deal with communication events between components. Let Σc = Σco ∪ Σcu be the k communication events, with Σco = ∪i=1Σcoi the observk able ones and Σcu = ∪i=1Σcui the unobservable ones.
The idea is to treat each communication event as any other event in each of its owners and, as it has been done with events et for e ∈ Σo for synchronizing observable events occurrences in the two executions, to introduce in the same way a global reference variable for each communication event at each time step, in charge of synchronizing any communication event occurrence in any of its owner with occurrences of it in all its other owners. We use one such reference variable for each trajectory, et and eˆt, for unobservable events e ∈ Σcu, and only one for both trajectories, et, for observable events e ∈ Σco as it will also in addition play the role of synchronizing observable events between trajectories exactly as the et for e ∈ Σo. So, we add to the previous propositional variables the new following ones: • eto, eˆto for all e ∈ Σc, o ∈ δ(e) = ∪iδi(e) and t ∈ {0, . . . , n − 1}, • et for all e ∈ Σc, eˆt for all e ∈ Σcu t ∈ {0, . . . , n − 1}. and Formulas in T (t, t + 1) are extended as follows. 1. Formulas (2.1), (2.2), (2.3) and (2.5) extend unchanged to eto and eˆto ∀e ∈ Σc, expressing that a communication event must be possible and has effects in each of its owner components and that two such different events cannot be simultaneous if they interfere. 2. Formulas (2.4) extend to prevent two simultaneous occurrences of a given communication event in the same owner component, i.e. apply ∀e ∈ Σc, ∀i, ∀{oi, oi0} ⊆ δi(e), oi 6= oi0 and the same with eˆ (obviously they do not apply to different owner components, by the very definition of communication events). 3. Finally, the new following formulas express the communication process itself, i.e. the synchronization of the occurrences of any communication event e in all its owners components (S(e) being the set of indexes of the owners components of e) and extend also formulas (2.6) to observable communication events: _ oi∈δi(e)
_ oi∈δi(e) etoi ↔ et and etoi ↔ et and
_ oi∈δi(e)
_ oi∈δi(e) eˆtoi ↔ eˆ
t eˆtoi ↔ e t ∀e ∈ Σcu ∀i ∈ S(e) ∀e ∈ Σco ∀i ∈ S(e) The formula ΦTn is unchanged except that, in the verification that the found cycle (third line) is not trivial, any observable event can be used, so the final disjunct of events et is extended to all e ∈ Σo ∪ Σco. We have thus the result that a DSLTS T is not diagnosable if and only if ∃n ≥ 1, ΦTn is satisfiable. 3.3
We have implemented the above extension in Java. We used the well designed API of the SAT solver Sat4j [6]. If more efficient solvers could have been chosen, it fitted well our clause generator written in Java and only a limited speed up can be awaited from C++ solvers (a speed up of 4, i.e. reduction of 75% of the runtime is often observed).
We have tested our tool on small examples with several communication events with multiple occurrences (three communicating components) with global communication (all components share the same event) or partial communication (only some components share the same event), as in Figure 1, which was the running example in [7].
The total number of propositional variables V arsN um in the generated formula ΦTn after n steps is: V arsN um = n
× (2|A| + 3 PiO=b1s ObOcci + PF aults F aultOcci + 2 PUnobs U nobOcci), where: i=1 i=1 |A| is the total number of state variables, Obs the total number of observable events, ObOcci the total number of occurrences of the observable event ei, F aults the total number of faults, F aultOcci the total number of occurrences of the faulty event ei, U nobs the total number of unobservable correct events, U nobOcci the total number of occurrences of the unobservable correct event ei.
The results are in Table 1, where the columns show the system and the fault considered (3 cases), the steps number n, the numbers of variables and clauses and the runtime.
Which means that f 2 is not diagnosable in C2 alone while it becomes diagnosable when synchronizing C2 and C3. For this last result, we have increased the steps number until reaching 22|A|, which is the theoretical upper bound of the twin plant states represented in the logical formula. As in general it is not always possible to reach this bound in practice, we propose in section 4 using incremental SAT to improve the management of increasing steps number. While Dn = Fn ∧ Cn f 1 is not diagnosable even after synchronizing all three components together. Numbers of variables and clauses are small in comparison to what SAT solvers can handle (up to hundred thousands propositional variables and millions of clauses). These tests are mentioned as a proof of concept. However, to test the tool on larger systems and because of the absence of benchmark in the literature, we have created in subsection 4.2. an example that can be scaled up. 4
We adapt satisfiability algorithms for checking diagnosability of both centralized (subsection 2.2) and distributed (subsection 3.2) DES in order to incrementally process the maximum length of paths with cycles searched for witnessing non diagnosability and we provide experimental results. 4.1
Two cases have to be distinguished while testing
diagnosability using SAT solvers to verify the satisfiability of the
logical formula ΦTn for a given n [
Instead, we propose to adapt the formula ΦTn in order to be tested in an incremental SAT mode by multiple calls to a Conflict Driven Clause Learning (CDCL) solver. Using CDCL solvers in a specialized, incremental, mode is relatively new but already widely used [8] in many applications. In this operation mode, the solver can be called many times with different formulas. However, solvers are designed to work with similar formulas, where clauses are removed and added from calls to calls. Learnt clauses can be kept as soon as the solver can ensure that clauses used to derive them are not removed. This is generally done by adding specialized variables, called assumptions, to each clause that can be removed. By assuming the variable to be F alse, the clause is activated and by assuming the variable to be T rue, the clause is trivially satisfied and no longer used by the solver. What is interesting for our purpose is that the CDCL solver can save clauses learnt during the previous calls and test multiple assumptions in each new call. This means that after n steps we hope that the solver will have learnt some constraints about the behavior of the system. Although we are interested in testing the diagnosability property on a defined system, this property is independent from the system behavior which can be learnt by the solver from the previous calls.
In order to extend the clauses representation given in subsections 2.2 and 3.2 to this mode of operation, we propose to divide the formula ΦTn in two parts. The first partTn describes the first n steps, synchronized on the observations, of the behavior of both trajectories (represented by the conjunction of formulas T (t, t+1), 0 ≤ t ≤ n−1, representing the (t + 1)th step). The second part Dn describes the diagnosability property at step n, i.e., the occurrence of a fault in the n previous steps of the faulty trajectory (given by the formula Fn) and the detection of a cycle at step n (given by the formula Cn). So we obtain, for n ≥ 1: ΦTn = Tn ∧ Dn Tn = I0 ∧ n−1 ^ T (t, t + 1) t=0 Add now at each step j a control variable hj allowing to disable (when its truth value is F alse) or activate (when its truth value is T rue) the formulas Fj and Cj and keep at step n all these controlled formulas for 1 ≤ j ≤ n. We obtain the following ΨTn formula, for n ≥ 1: n ^ j=1 ΨTn = Tn ∧
Dj 0
Dj 0 = Fj 0 ∧ Cj 0 1 ≤ j ≤ n Fj 0 = ¬hj ∨ Fj
Cj 0 = ¬hj ∨ Cj 1 ≤ j ≤ n
ΦTn ≡ ΨTn ∧ hn ∧ n−1 ^ j=1 ¬hj TΦhTnisbayllaowSsAoTnec,alfloornalΨlnTn ≥und1e,rtothreepcloancetrothlevaSrAiaTblceasllseotnting given by Hn = {¬h1, . . . , ¬hn−1, hn} (indicated in a second argument of the call):
SAT (ΦTn ) = SAT (ΨTn , Hn) The idea is now to consider the control variables hj as assumptions and use incremental SAT calls IncSATj under varying assumptions, for 1 ≤ j ≤ n. For this, we use the following recurrence relationships for both formulas ΨT j and assumptions Hj : Ψ0T = I0 H1 = {h1} ΨjT+1 = ΨjT ∧ T (j, j + 1) ∧ Dj+10 j ≥ 0
Hj+1 = Hj [{¬hj , hj+1}] j ≥ 1 where the notation Hj [{assi}] means updating in Hj assumptions hi by their new settings assi, i.e., in the formula above, replacing the truth value of hj , which was T rue, by F alse, and adding the new assumption hj+1 with truth value T rue. From these relationships, the unique call to SAT under given assumptions SAT (ΨTn , Hn) can be replaced, starting with the set of clauses I0, by multiple calls, 0 ≤ j ≤ n − 1, to an incremental SAT under varying assumptions:
IncSATj+1(N ewClausesj+1, N ewAssumptionsj+1) = IncSATj+1(T (j, j + 1) ∧ Dj+10, {¬hj , hj+1}) (4.1) If IncSATj answers SAT, the search is stopped as non diagnosability is proved, if it answers UNSAT, then IncSATj+1 is called. Notice that we used a unique assumption hj for controlling both Fj and Cj as non diagnosability checking requires the presence of both a fault occurrence in the faulty trajectory and of a cycle. But the same framework allows the independent control of formulas by separate assumptions. For sake of simplicity, we also assumed we called IncSAT at each step, but this is not mandatory and indexes j for the successive calls can be decoupled from indexes t for steps. We should also say that, even if IncSAT allows us to reactivate an already disabled clause, we are sure in our case to never use this function (when hk has been set to F alse, it always remains so) and we can thus force the solver to do a hard simplification process that removes the forgotten clauses permanently. As a result of our adaptation we will be able to scale up the size of the tested system and the distance and length of a cycle witnessing non diagnosability. 4.2
We show in this subsection a comparison between our
adapted version of subsection 4.1, that uses incremental
SAT, and the previous versions, for centralized model
(subsection 2.2 following [
The results are in Table 2 for the centralized model (for k = 18, 28, 38, 48, 58 and 98) and in Table 3 for the distributed model (for k = 3, 13, 23, 33, 43 and 63). The length of a pair of executions with cycles witnessing the non diagnosability of f in each example is k + 2 and we consider the satisfiability of the formula ΦkT+2, so the number of steps required for SAT to provide the answer Yes is: |Steps] = k + 2. In order to obtain a fair comparison between IncSAT , which manages internally by handling assumptions the successive satisfiability checks of increasing formulas for j = 1, . . . , k + 2, and SAT, for which k + 2 successive calls are made to the solver with respective formulas ΦTn for n = 1, . . . , k +2, the sum of the k + 2 runtimes of the SAT solver calls are considered in this case (last column in the tables). |Steps| |Clauses| 20 42,614 30 131,714 40 303,736 50 576,466 60 970,156 100 4,334,018
Although these examples remain relatively simple and do
not reflect any potential constraint that could be resumed by
some learnt clauses (e.g. no interfering events), we can
already notice the difference in runtime in favor of our
incremental version in the centralized case and for the two largest
values of k in the distributed case. This difference could be
explained by the fact that generating all variables from the
beginning for all time steps and for all events imply many
meaningless clauses that would add a load on the solver in
the version in [
The first introduction to the notion of diagnosability was by
[
In order to overcome this limitation [
Let us mention here that the two previous works were
interested in centralized systems with simple faults modeled
as distinguished events. The first studies about fault
patterns were introduced in [
The first work that addressed diagnosability analysis in DDES was [7]. A DDES is modeled as a set of communicating FSM. Each FSM has its own events set, communication events being the only ones shared by at least two different FSM. In [7] was introduced an incremental diagnosability test which avoids to build the twin plant for the whole distributed system if not needed. Thus one starts by building a local twin plant for the faulty component to test the existence of a local critical path. If such a path exists one builds the local twin checkers of the neighboring components. Local twin checker is a structure similar to local twin plant, i.e., where each path in it represents a pair of behaviors with the same observations, except that there is no fault information in it since it is constructed from non-faulty component. After constructing local twin checkers, one tries to solve the ambiguity resulting from the existence of a critical path in the local twin plant. This is done by synchronizing on their communication events this local twin plant with the local twin checker of one neighboring component. In other words, one tries to distinguish the faulty path from the correct one by exploiting the observable events in the neighboring components, because theses events occurrences that are consistent with the occurrences of the communication events could solve the ambiguity. The process is repeated until the diagnosability is answered, so only in the worst case has the whole system to be visited. Another important contribution in this work was to delete the unambiguous parts after each synchronization on the communication events, reducing thus the amount of information transferred to next check (if needed). The approach assumed simple faults.
The work by [
After the reduction of diagnosability problem to a path
finding problem by [
By extending the state of the art works for centralized DES, we have expressed diagnosability analysis of DDES as a satisfiability problem by building a propositional formula whose satisfiability, witnessing non diagnosability, can be checked by SAT solvers. We allow both observable and non observable communication events in our model. Our expression of these communication events, which avoids merging all their owner components, helps in reducing the number of clauses used to represent them and this reduction is proportional to the number of their occurrences. We have also proposed an adaptation of the logical formula in order to use incremental SAT calls helping managing the scaling up of the distance and the length of the intended cycles witnessing non diagnosability and thus the size of the tested system. Thus we exploited the clauses learnt about the system behavior in the previous calls. This approach is more practical and more efficient for complex systems than existing ones, as it avoids starting from scratch at each call.
We are now considering the extension of this work to
fault patterns diagnosability [