=Paper= {{Paper |id=Vol-1507/dx15paper36 |storemode=property |title=Random Generator of k-Diagnosable Discrete Event Systems |pdfUrl=https://ceur-ws.org/Vol-1507/dx15paper36.pdf |volume=Vol-1507 |dblpUrl=https://dblp.org/rec/conf/safeprocess/Pencole15 }} ==Random Generator of k-Diagnosable Discrete Event Systems== https://ceur-ws.org/Vol-1507/dx15paper36.pdf
                        Proceedings of the 26th International Workshop on Principles of Diagnosis




                  Random generator of k-diagnosable discrete event systems

                                             Yannick Pencolé1 2
                    1
                      CNRS, LAAS, 7 avenue du colonel Roche, F-31400 Toulouse, France
                            2
                              Univ de Toulouse, LAAS, F-31400 Toulouse, France
                                       e-mail: yannick.pencole@laas.fr



                         Abstract                                    2. diagnosability algorithms: the fact that a fault f is k-
                                                                        diagnosable is usually the worst case for this type of
     This paper presents a random generator of dis-
                                                                        algorithms (as they all look for the existence of an am-
     crete event systems that are by construction k-
                                                                        biguous scenario to conclude the system is not diag-
     diagnosable. The aim of this generator is to pro-
                                                                        nosable).
     vide an almost infinite set of diagnosable systems
     for creating benchmarks. The goal of such bench-                  The paper is organised as follows. After formally re-
     marks is to provide a solid set of examples to test            calling the problem that motivates the generation of bench-
     and compare algorithms that solve many prob-                   marks, we describe the fundamental property which is being
     lems around diagnosable discrete event systems.                used for the effective generation of systems where a given
                                                                    fault f is k-diagnosable. Then the description of the algo-
1 Introduction                                                      rithm of the generator is provided as well as some details
                                                                    about its effective implementation.
For many years, the problem of fault diagnosis in discrete
event systems has been actively addressed by different sci-
entific communities such as DX (AI-based diagnosis) [1;
                                                                    2 Background
2], FDI (Fault Detection and Isolation), DES (Discrete              This paper addresses the random generation of benchmarks
Event Systems) [3]. Depending on the community, many                for the problem of the fault diagnosis of discrete event sys-
differents aspects of the same problem have been addressed          tem. This problem is briefly recalled in this section. We
such as the design of efficient diagnosers, the checking of di-     assume that the reader is familiar with the notations of the
agnosability properties, the effective modelling of real sys-       language theory (notion of Kleene closure, prefixes,...).
tems. When dealing with performance, most of the contri-
butions present experimental results on specific examples of        2.1 Modelling
their own usually inspired or based on real world systems.          We suppose that the system under monitoring behaves as an
The main problem about these contributions is that they are         event generator that can be modelled as an automaton.
not really comparable as they are not applied on the same           Definition 1 (System description). The model (system de-
benchmarks. Moreover, used benchmarks may not be al-                scription) SD of a discrete event system S is a finite state
ways completly defined in a paper due, most of the time, to         automaton SD = (Q, Σ, T, q0 ) where:
confidential data that cannot be published so other academic
contributors cannot use them for comparison purposes. In              • Q is a finite set of states;
order to analyse and boost the effective performance of algo-         • Σ is a finite set of events;
rithms addressing the fault diagnosis problem in DES, com-            • T ⊆ Q × T × Q is a finite set of transitions;
mon and fully available benchmarks become a necessity.
   This paper addresses the random generation of k-                   • q0 is the initial state of the system.
diagnosable systems. We here propose the possibility to                Σ is the set of events that the system can produce. Among
generate (and store on a web page) k-diagnosable systems            Σ we distinguish events that are observable Σo ⊆ Σ and
that have been generated without any kind of bias that would        events that are not observable. When the system operates,
come from a specific diagnosis/diagnosability method. By            its effective behaviour is represented by a trace of the au-
doing so, we propose to design a random category for                tomaton (also called a run).
benchmarks as the SAT community proposed for SAT prob-
                                                                    Definition 2 (Trace). A trace τ ∈ Σ∗ of the system is a finite
lems and to get the same advantages by comparing different
                                                                    sequence of events associated with a transition path from the
diagnosis/diagnosability approaches on the same but ran-
                                                                    initial state q0 to a state q in the model of the system.
dom systems. The choice of generating k-diagnosable sys-
tems is motivated by the fact that they can be used as exam-           The set of traces of the system is the language generated
ples for:                                                           by its model and is denoted L(S) (so the automaton SD
                                                                    generates the language L(S)). Let PΣ0 (τ ) be the classical
   1. diagnosis algorithms: given a fault f , we know by con-
                                                                    projection of a sequence τ of Σ∗ on the alphabet Σ0 recur-
      struction that the most precise algorithm will determine
                                                                    sively defined as follows:
      its occurrence with certainty within the next k observa-
      tions after the occurrence of f ;                              1. PΣ0 (ε) = ε;




                                                              277
                          Proceedings of the 26th International Workshop on Principles of Diagnosis


  2. PΣ0 (τ.e) = PΣ0 (τ ) if e 6∈ Σ0 ;                                Definition 8 (Diagnosability). The fault f is diagnosable in
                                                                      a system S if:
  3. PΣ0 (τ.e) = PΣ0 (τ ).e if e ∈ Σ0 .
                                                                                        ∃n ∈ N+ , Diagnosable(n)
  Based on this notion of projection, we can associate with
any trace of the system its observable part.                          where Diagnosable(n) stands for:
Definition 3 (Observable trace). Let τ be a trace of the sys-                   ∀τ1 .f ∈ L(S), ∀τ2 : τ1 .f.τ2 ∈ L(S)
tem, the observable trace στ is the projection of τ over the                             |PΣo (τ2 )| ≥ n ⇒
set of observable events Σo :
                                                                          (∀τ ∈ L(S), (PΣo (τ ) = PΣo (τ1 .f.τ2 ) ⇒ f ∈ τ )).
                         στ = PΣo (τ ).                               Definition 9 (k-Diagnosability). The fault f is k-
                                                                      diagnosable, k ∈ N+ , in a system S if:
2.2 Diagnosis problem and solution
                                                                               Diagnosable(k) ∧ ¬Diagnosable(k − 1).
Now we are ready to define the classical Fault diagnosis
problem on DES.                                                          Diagnosability is a property that relies on the liveness
                                                                      of the observability of the system which means that, to be
Definition 4 (Fault). A fault is a non-observable event f ∈           (k)-diagnosable, a system must not generate unbounded se-
Σ.                                                                    quences of unobservable events (no cycle of unobservable
   A fault is represented as a special type of non-observable         events in SD). Throughout this paper, we consider that the
event that can occur on the underlying system. Once the               observability of the system is live.
event has occurred, we say that the fault is active in the sys-
tem, otherwise it is inactive. We consider here the problem           3 Random Generator
of permanent faults as initially introduced in [4].                   The aim of this section is to present the algorithm that is
Definition 5 (Diagnosis problem). A diagnosis problem is              being used to randomly generate a discrete event systems
a triple (SD, OBS, FAULTS) where SD is the model of                   where a fault f is k-dignosable and that has been imple-
a system, OBS is the sequence of observations of Σ?o and              mented inside the Diades software. We focus on the gener-
FAULTS is the set of fault events defined over SD.                    ation of a system with one fault only. (see th conclusion for
                                                                      the generation for n, n > 1 faults).
  Informally speaking, (SD, OBS, FAULTS) represents
the problem of finding the set of active faults from FAULTS           3.1 Signatures and fault ambiguity
that have occurred relying on the model SD and the se-                The algorithm that generates a k-diagnosable system relies
quence of observations OBS.                                           on the notion of signatures. Let f be a faulty event, the sig-
Definition 6 (Diagnosis Candidate). A diagnosis candidate             nature of f is the set of observable traces resulting from the
is a couple (q, F ) where q is a state of SD (q ∈ Q) and F is         projection of system traces that contain at least one occur-
a set of faults.                                                      rence of an event f before the last observation of the trace.
   A diagnosis candidate represents the fact that the under-          Definition 10 (Signature). The signature of an event f into
lying system is in state q and the set F of faults has occurred       a system S is the language Sig(f ) ⊆ Σ?o such that
before reaching state q.                                                  Sig(f ) ={στ |τ = τ1 .o.τ2 ∈ L(S),
Definition 7 (Solution Diagnosis). The solution ∆ of the                           f ∈ τ1 , o ∈ Σo , τ2 ∈ Σ? , στ = PΣo (τ )}.
problem (SD, OBS, FAULTS) is the set of diagnosis can-
                                                                          In the following, we will also denote by Sig(¬f ) the set
didates (q, F ) such that there exists for each of them at least
                                                                      of observable traces associated with the traces of the sys-
one trace τ of SD such that:
                                                                      tem that do not contain any fault f before the last obser-
  1. the observable trace of τ is exactly the sequence                vation. Intuitively speaking, as long as the current observ-
     OBS = o1 . . . om and the last event of τ is om ;                able trace is in Sig(¬f ) ∩ Sig(f ), we know that the system
                                                                      may have produced a faulty trace or a non-faulty trace be-
  2. the set of fault events that has occurred in τ is exactly
                                                                      fore the last observation. k-diagnosability ensures that the
     F;
                                                                      ambiguity can last at most for k observations. The principle
  3. the final state of τ is q.                                       of the generator relies on the following result that formal-
                                                                      izes this intuition. Let L ARGEST P REFIXES(τ, n) = {τi0 :
   Informally, candidate (q, F ) is part of the solution if it is
                                                                      τ = τi0 τi , |τi | = i, i ∈ {0, . . . , n − 1}} be the set of the n
possible to find out in SD a behaviour of the system satisfy-
                                                                      largest prefixes of τ (τ being a prefix of itself).
ing OBS which leads to the state q after the last observation
of OBS and in which the faults F have occurred.                       Theorem 1. In the system S, the event f is k-diagnosable
                                                                      if and only if:
2.3 Diagnosability                                                       1. For any observable trace σ in Sig(¬f ) ∩ Sig(f ), there
Diagnosability is a property of the system that asserts                      exists n < k such that L ARGEST P REFIXES(σ, n) ⊆
whether a fault f of a system S can be always diagnosed                      Sig(¬f ) ∩ Sig(f ) and L ARGEST P REFIXES(σ, n +
with certainty after the observation of a finite set of obser-               1) 6⊆ Sig(¬f ) ∩ Sig(f ).
vations [4]. In other words, once the fault f has occurred in            2. There        exists    at        least   one      observable
S, it is sufficient to wait a certain amount of observations to              trace σ in Sig(¬f ) ∩ Sig(f ) such that
ensure that any candidate (q, F ) of the solution contains f                 L ARGEST P REFIXES(σ, k − 1) ⊆ Sig(¬f ) ∩ Sig(f )
(f ∈ F ).                                                                    and an observable o such that σo ∈ Sig(f ).




                                                                278
                          Proceedings of the 26th International Workshop on Principles of Diagnosis


    Proof: (⇒)Let τ1 .f be a trace of the system S. As S is              Algorithm 1 General algorithm for the random generation
k-diagnosable, there exists m ≤ k such that ∀τ2 : τ1 .f.τ2 ∈             of k-diagnosable systems.
L(S), |PΣo (τ2 )| ≥ m ⇒ (∀τ ∈ L(S), (PΣo (τ ) =                             Input: k ∈ N, k ≥ 1
PΣo (τ1 .f.τ2 ) ⇒ f ∈ τ )). Consider one of these                           Input: f an event
trace τ1 .f.τ2 such that τ2 contains exactly m observa-                     Input: deg maximal output degree
tions (PΣo (τ2 ) = o1 . . . om ). k-diagnosability implies                  (Σo , Σ) ← G ENERATE E VENTS()
that there exists a minimal integer n ∈ {1, . . . , m − 1}                  S←∅
such that PΣo (τ1 .f ).o1 . . . on+1 ⇒ f ∈ τ as soon as                     AmbSig(f ) ← G ENERATE A MB S IGNATURE(k,Σo , deg)
τ ∈ L(S) and PΣo (τ ) = PΣo (τ1 .f ).o1 . . . on+1 , there-
fore PΣo (τ1 .f ).o1 . . . on+1 ∈ Sig(f ) \ Sig(¬f ) and ∀i ∈              /* AmbSig(f ) = (Q, Σo , T, q0 , A) a deterministic au-
{1, . . . , n}, PΣo (τ1 .f ).o1 . . . oi ∈ Sig(f ) ∩ Sig(¬f ). So          tomaton */
L ARGEST P REFIXES(PΣo (τ1 .f ).o1 . . . on , n) ⊆ Sig(¬f ) ∩              MF[q0 ] ← G ENERATE S TATES()
Sig(f ).        So for any τ1 .f there exists n < k                        MNF[q0 ] ← G ENERATE S TATES()
such that L ARGEST P REFIXES(PΣo (τ1 .f ).o1 . . . on , n) ⊆               for all q ∈ Q in Breadth-First Order from q0 do
Sig(¬f ) ∩ Sig(f ). Now, remark that for any observ-                          (Σfo , Σo¬f ) ← R ANDOM S PLIT(Σo , q)
able sequence σ that belongs to Sig(¬f ) ∩ Sig(f ), there                     S ← S∪ G EN FAULT E XTS∗ (MF[q],Σfo ,deg)
must exist a trace τ1 .f.τ2 of the system, with τ2 con-                       S ← S∪ G EN N OM E XTS∗ (MNF[q],Σ¬f    o ,deg)
taining at least one observable event, such that σ =                                       o
                                                                              for all q −→ q 0 ∈ T do
PΣo (τ1 .f.τ2 ), so there must exist n < k such that σ ∈                        if MF[q 0 ] = ∅ then
L ARGEST P REFIXES(PΣo (τ1 .f ).o1 . . . on , n) ⊆ Sig(¬f ) ∩                        MF[q 0 ] ← G ENERATE S TATES()
Sig(f ) so, for any σ that belongs to Sig(¬f ) ∩ Sig(f ),                            MNF[q 0 ] ← G ENERATE S TATES()
there is no set L ARGEST P REFIXES(σ, n + 1) that only con-                     end if
tains ambiguous signatures.                                                     S ← S∪
    Finally, as S is k-diagnosable, we know that there exists                   G EN N OM E XTS(MNF[q],MNF[q 0 ],o,deg)
at least one trace τ.f.τ1 .o1 , such that τ is a trace of the sys-              if q 0 6∈ A then
tem that does not contain f , τ1 is a finite continuation of τ.f                     S ← S∪ G EN N OM E XTS(MF[q],MF[q 0 ],o,deg)
that is unobservable and o1 is observable and there is a fi-                    else
nite continuation τ2 o2 τ3 o3 . . . τk ok with PΣo (τi ) = ε such                    if q ∈ A then
that for any i ∈ {1, . . . , k − 1}, PΣo (τ.f.τ1 .o1 . . . τi oi ) ∈                    S ← S∪ G EN E XTS(MF[q],MF[q 0 ],o,deg)
Sig(¬f ) ∩ Sig(f ) PΣo (τ.f.τ1 .o1 . . . τk ok ) ∈ Sig(f ) \                         else
Sig(¬f ) which implies the condition 2 with σ =                                         S ← S∪
PΣo (τ.f.τ1 .o1 . . . τk−1 ok−1 ).                                                      G EN FAULT E XTS(MF[q],MF[q 0 ],o,deg)
(⇐) Suppose now that conditions 1 and 2 hold. Consider                               end if
an observable trace σ that is ambiguous (σ ∈ Sig(f ) ∩                          end if
Sig(¬f )). Condition 1 states that there exists n < k such                    end for
that L ARGEST P REFIXES(σ, n) ⊆ Sig(¬f ) ∩ Sig(f ) and                     end for
L ARGEST P REFIXES(σ, n + 1) 6⊆ Sig(¬f ) ∩ Sig(f ). Con-                   Output: S where f is k-diagnosable.
sider now any largest observable trace σ 0 such that |σ 0 | −
|σ| = m and σ ∈ L ARGEST P REFIXES(σ 0 , m) ⊆ Sig(¬f )∩
                                                                            The generation is composed of two steps. The first one
Sig(f ), it follows that L ARGEST P REFIXES(σ 0 , m + n) ⊆
                                                                         is the generation of the ambiguous signature with G ENER -
Sig(¬f ) ∩ Sig(f ) and L ARGEST P REFIXES(σ 0 , m + n +
                                                                         ATE A MB S IGNATURE . The result of this function is a de-
1) 6⊆ Sig(¬f ) ∩ Sig(f ). As σ 0 is one of the largest ob-
                                                                         terministic automaton AmbSig(f ) = (Q, Σo , T, q0 , A) that
servable trace holding this condition, any observable trace
                                                                         actually generates the language Sig(f )∩Sig(¬f ) (any tran-
σ 0 o, o ∈ Σo , is either in Sig(f ) or in Sig(¬f ) but not in
                                                                         sition path from state q0 to an accepting state of A rep-
both of them. Condition 1 states that m + n < k, so k ob-
                                                                         resents a sequence of Sig(f ) ∩ Sig(¬f )). The automa-
servations at least are required to solve the ambiguity. Con-
                                                                         ton AmbSig(f ) is generated with respect to the conditions
dition 2 states that there exists at least such an observable
                                                                         1 and 2 that are defined in Theorem 1 to ensure the k-
trace σ 0 with m + n = k − 1 and an observation o so that
                                                                         diagnosability of the resulting system S. The second step of
σ 0 o is definitively in Sig(f ) so f can be diagnosed with
                                                                         the generation is the effective generation of S based on the
certainty in this case with exactly k observations. Hence the
                                                                         ambiguous signature AmbSig(f ). The idea is to map every
result.
                                                                         state q of AmbSig(f ) with two sets of states in S denoted
                                                                         M F [q] and M N F [q]. Given any path σ of AmbSig(f ) that
3.2 Algorithm                                                            leads to state q with, as a last observation, the event o, any
                                                                         state of M F [q] (resp. M N F [q]) will be reached by at least
The principle of the random generator is depicted in Al-                 one transition path τ of S starting from a state of M F [q0 ]
gorithm 1. Given a parameter k and a fault event f , the                 (resp. M N F [q0 ]) that ends with a transition labelled with o
algorithm randomly generates a system S where the event                  and the observable projection of τ is exactly σ. The differ-
f is k-diagnosable by construction. We also provide an-                  ence between M F and M N F is that any underlying path
other parameter deg which is the maximal number of output                of S leading to a state of M F [q] (resp. M N F [q]) has an
transitions that is allowed per state during the generation of           observable projection which is a prefix of Sig(f ) (resp. a
the system. Parameter deg is important for the creation of               prefix of Sig(¬f )). To generate S we explore AmbSig(f )
benchmarks as the output degree has a strong influence on                from its initial state in a breadth-first search manner. For a
the diagnosis/diagnosability computations.                               given state q, we have to consider three types of transition




                                                                   279
                         Proceedings of the 26th International Workshop on Principles of Diagnosis


generations going out of any state of M F [q], M N F [q]. The         rameters like the number of (un)observable events the output
first ones are the transition paths that will lead to an observa-     degree of transitions, the parameter k, the minimal number
tion o that belongs to AmbSig(f ), the second one is the set          of observable events involved in the ambiguous signature,
of transition paths that do not lead to an observation o that         the number of states (still experimental). One particular pa-
belongs to AmbSig(f ) but lead to an observation o0 that              rameter is the seed parameter that allows the generation of
belongs to Sig(f ) only and the third one is the set of transi-       the same system (the seed ensures the same generation of
tion paths that do not lead to an observation o that belongs          random numbers). By construction, the algorithm is linear
to AmbSig(f ) but lead to an observation o00 that belongs to          in the number of states. A set of pre-computed benchmarks
Sig(¬f ) only.                                                        as well as the implemented generator are available at the
   The second and third cases are handled by randomly split-          following url:
ting Σo into two subsets (Σfo , Σ¬fo ) each of them only con-         http://homepages.laas.fr/ypencole/benchmarks
taining observable events that are not output event of q in
AmbSig(f ) (R ANDOM S PLIT(Σo , q)). Then given Σfo , we              4 Conclusions
randomly generate faulty extensions for a subset of Σfo (the          To test and compare diagnosis and/or diagnosability algo-
selection of the subset is also random and might even be              rithms, fully detailed and available benchmarks are a ne-
empty if q has no output events in AmbSig(f ), indeed if q            cessity. In order to test how generic is an algorithm, we
has no output events, it must be extended to ensure that the          propose here an algorithm that randomly generates systems
observability of the system is live). An extension is a set of        where a fault f is k-diagnosable. We also propose an im-
acyclic and unobservable transition paths that lead to a tran-        plementation within the D IA D ES framework. Extension to
sition labeled with an observable event from Σfo . A faulty           generate systems with n k-diagnosable faults is easy, it re-
extension ensures that an event f has at least occurred on            quires to repeat the generation of the ambiguous signatures
any generated transition path before the observable transi-           for the n faults and explore them in parallel to generate the
tion (G EN FAULT E XTS). Given Σ¬f    o , we proceed the same         k-diagnosable system. Our short-term perspective is to im-
way to generate non-faulty extensions (G EN N OM E XTS).              prove the generator to allow a better control of the number
As, in these two cases, the traces generated by these ex-             of generated states. A fixed number of generated states re-
tensions are not associated with observable traces involved           quires to add new constraints in the generation that prop-
in AmbSig(f ) any more, it is sufficient to generate further          agate during the generation process. Without any control
extensions on these traces and guarantee that the observ-             about this propagation, the generation may just fail as it
able language associated with these further extensions is live        could become an over-constrained problem. Our perspec-
(this procedure is denoted by the ∗ in G EN N OM E XTS∗ and           tive is to also go one step further by generating diagnosable
G EN FAULT E XTS∗ ).                                                  systems that are component-based in order to scale up the
   The last case to handle now is the case where the observ-          size of the generated system. The D IA D ES framework al-
able event o is an output event of q in AmbSig(f ), which             ready has a tool to generate component-based systems [5]
                                                            o
means that there exists one and only one transition q −→ q 0          which ensures that any component is globally consistent, but
in AmbSig(f ). If q 0 has never been visited, the set of states       adding the constraint of diagnosability makes the generation
M F [q 0 ] and M N F [q 0 ] are generated first. A nominal ex-        far more complex to implement.
tension is generated from M N F [q] to M N F [q 0 ]. Depend-
ing on the status of q 0 , the extension between M F [q] and          References
M F [q 0 ] is different. If q 0 6∈ A, it means that any prefix        [1] Gianfranco Lamperti and Marina Zanella. Diagnosis of
generated by AmbSig(f ) with paths from q0 to q 0 are pre-                discrete-event systems from uncertain temporal obser-
fixes of sequences in Sig(f ) ∩ Sig(¬f ) but they are not in              vations. Artificial Intelligence, 137:91–163, 2002.
Sig(f ) ∩ Sig(¬f ), they can therefore be only in Sig(¬f ):           [2] Yannick Pencolé and Marie-Odile Cordier. A formal
extensions between M F [q] and M F [q 0 ] are then nominal
                                                                          framework for the decentralised diagnosis of large scale
extensions. Now, if q 0 ∈ A, there are two cases. If q 6∈ A,
                                                                          discrete event systems and its application to telecommu-
it means the system must become faulty between the states
                                                                          nication networks. Artificial Intelligence, 164(2):121–
of M F [q] and M F [q 0 ] so that paths of the system that reach
                                                                          170, 2005.
any state of M F [q 0 ] is associated with an observable trace
that belongs to Sig(f ) (G EN FAULT E XTS). If q ∈ A, any             [3] Janan Zaytoon and Stéphane Lafortune. Overview of
path that reaches a state of M F [q] is already faulty (its ob-           fault diagnosis methods for discrete event systems. An-
servable trace is already in Sig(f )), any type of extension              nual Reviews in Control, 37:308–320, 2013.
from M F [q] to M F [q 0 ] is therefore possible (faulty or not),     [4] Meera Sampath, Raja Sengupta, Stéphane Lafortune,
hence the use of G EN E XTS.                                              Kasim Sinnamohideen, and Demosthenis Teneketzis.
                                                                          Diagnosability of discrete-event systems. Transactions
3.3 Implementation                                                        on Automatic Control, 40(9):1555–1575, 9 1995.
Algorithm 1 is implemented with the help of the Diades                [5] Yannick Pencolé. Fault diagnosis in discrete-event sys-
library package [5]. Diades is a set of C++ libraries                     tems: How to analyse algorithm performance? In Di-
that implement discrete event systems in a component-                     agnostic reasoning: Model Analysis and Performance,
based way, different diagnosis algorithms as defined in                   pages 19–25, Montpellier, France, 2012.
the spectrum of [6] (from component-based algorithms                  [6] Anika Schumann, Yannick Pencolé, and Sylvie
to diagnoser-based algorithms). D IA D ES also imple-                     Thiébaux. A spectrum of symbolic on-line diagnosis
ments a diagnosability checker as well as an accuracy                     approaches. In 17th International Workshop on Princi-
checker. The generator results in a Linux terminal command                ples of Diagnosis, pages 194–201, Nashville, TN USA,
dd-diagnosable-des-generate with a set of pa-                             2007.




                                                                280