=Paper=
{{Paper
|id=Vol-1431/paper3
|storemode=property
|title=Combining Enumerative and Symbolic - Techniques for Diagnosis of Discrete-Event Systems
|pdfUrl=https://ceur-ws.org/Vol-1431/paper3.pdf
|volume=Vol-1431
|dblpUrl=https://dblp.org/rec/conf/vecos/BoussifGK15
}}
==Combining Enumerative and Symbolic - Techniques for Diagnosis of Discrete-Event Systems==
https://ceur-ws.org/Vol-1431/paper3.pdf
Combining Enumerative and Symbolic
Techniques for Diagnosis of Discrete-Event
Systems
Abderraouf Boussif Mohamed Ghazel Kais Klai
Univ. Lille Nord de France, Univ. Lille Nord de France, LIPN, CNRS UMR 7030,
F-59000 Lille, France F-59000 Lille, France Univ. Paris 13, Sorbonne Paris Cité,
IFSTTAR, Cosys/Estas, IFSTTAR, Cosys/Estas,
F-59650 Villenveuve d’Ascq, France F-59650 Villenveuve d’Ascq, France
FR FR FR
abderraouf.boussif@ifsttar.fr mohamed.ghazel@ifsttar.fr kais.klai@lipn.univ-paris13.fr
In this paper, an efficient approach to verify diagnosability of discrete-event systems is proposed. The
approach consists in constructing a hybrid diagnoser based on the symbolic observation graph (SOG), which
is a technique that combines symbolic and enumerative representations in order to build a deterministic
observer from a partially observed model. The construction of the diagnoser as well as the verification of
diagnosability are performed simultaneously on-the-fly, which can considerably reduce the generated state
space of the diagnoser and thus the overall running time. Furthermore, the proposed approach provides
a heuristic strategy in order to converge fast into the necessary part, of the diagnoser, for analysing
diagnosability.
Discrete-Event Systems, Diagnosability Analysis, Symbolic Observer Graph, On-the-Fly Verification.
1. INTRODUCTION further developed later. In this paper, (Sampath et al.
1995), the original definition of diagnosability was
In automated monitoring and fault diagnosis of introduced in the language context. A systematic
complex dynamic systems, one of the central tasks method to check diagnosability based on a dedicated
is to detect and identify the occurrence of failures deterministic version of the model derived from the
as early as possible. This task has become an original system, a so-called diagnoser, was also
active research area in recent years (Zaytoon and provided. It consists of a specific observer of the
Lafortune 2013). From the theoretical point of view system associated with a labelling function that
and at a high level of abstraction, Discrete-Event attributes to each state (or macro-state), in this
Systems (DESs) are more suitable for performing observer, a label indicating whether the state is
diagnosis analysis on complex systems (Cassandras reached by a faulty execution or not, i.e. an execution
and Lafortune 2007). where some particular unobservable events, called
faults, have occurred or not.
One of the main issues in diagnosis activity that
must be addressed is diagnosability investigation. Other automata-based approaches (Jiang et al.
Analysing diagnosability of a system intends to 2001; Yoo and Lafortune 2002), aiming to reduce
determine accurately whether any predetermined computational complexity have been then proposed.
failure or class of failures can be detected and In (Yoo and Lafortune 2002), a polynomial-time
identified within a finite delay following its occurrence algorithm for checking diagnosability based on
(Sampath et al. 1995). a structure called verifier is adopted. In (Jiang
et al. 2001), an algorithm based on the twin plant
Diagnosability verification has received considerable structure (a parallel composition of the investigated
attention since the seminal paper by (Sampath automaton with itself) is proposed. Reformulations
et al. 1995), which provides a basic concept and of these works in model-checking framework were
a formal definition of diagnosability analysis and first proposed in (Cimatti et al. 2003) and extended
fault diagnosis of DESs that were adopted and in (Boussif and Ghazel 2015). The goal is to check
diagnosability property in the same way as to check while transitions between macro-states are
any safety property. represented by enumerate observable events.
Furthermore, some works on diagnosability of 2. We design an appropriate algorithm, for
DESs turned to Petri nets (PNs) formalism, simultaneously constructing the diagnoser and
benefiting from the mathematical and graphical checking diagnosability on-the-fly. Actually, the
representations capability and the well-developed verification process is stopped (only a part
theory underlying PNs (Peterson 1981). (Ushio of the diagnoser is built) as soon as the
et al. 1998) extended Sampath’s study to systems diagnosability is proven to be unsatisfied,
modelled by PNs with the assumption that some which can considerably reduce the generated
places are observables whereas all of the transitions state space of the diagnoser. Furthermore,
are unobservable. A diagnoser is constructed from the proposed algorithm is endowed with a
the reachability graph. In (Wen and Li 2005), heuristic strategy in order to converge fast
the authors proposed a sufficient condition for into the necessary part of the diagnoser for
testing diagnosability by checking the structure diagnosability analysis.
of T -invariants of a PN. In (Cabasino et al.
2009) the modified basis reachability graph (MBRG) The paper is structured as follows. In Section 2,
and basis reachability diagnoser (BRD), which we introduce the basic background needed to deal
provide a compact representation of the reachability with diagnosability and to develop our approach. In
graph, were developed. In (Basile et al. 2012), an Section 3, we recall the notion of diagnosability as
approach for checking diagnosability by quantifying well as the original diagnoser approach. Section 4 is
the finite delay of diagnosability (the so-called K- devoted to discuss the Symbolic Observation Graph
diagnosability) was proposed by using the integer adapted to the context of this paper. In Section 5,
linear programming (ILP) technique. A structure the verification approach is sketched out then an on-
called verifier net (VN) was introduced in (Cabasino the-fly algorithm based on the SOG is presented.
et al. 2014) to deal with diagnosability for both Section 6 discusses the pertinent existing work in
bounded and unbounded PNs. Recently, (Liu et al. relation with the present work. Finally, conclusion
2014a) has proposed an on-the-fly and incremental remarks and future research directions are given in
diagnosis technique to construct a diagnoser from a Section 7.
bounded PN in order to verify diagnosability and K-
diagnosability properties. 2. PRELIMINARIES
To get a general overview on the literature pertaining We first recall some standard notations that will be
to diagnosis of DESs, the reader can refer to the used in the sequel. Let Σ be a finite alphabet of
recent survey in (Zaytoon and Lafortune 2013), events (actions). A string is a finite sequence of
where theoretical and practical issues, tools and events in Σ. denotes the empty string. Given a
other issues in relation with diagnosis are discussed. string s, the length of s is denoted by |s|. The set
of all strings formed by events in Σ is denoted by Σ∗ .
The challenge of analysing diagnosability is the
Any subset of Σ∗ is called a language. Given a string
combinatorial explosion problem that appears during
s ∈ L, L/s , {t ∈ Σ∗ |s.t ∈ L} is called the post-
the building of the intermediate models (diagnoser,
language of L after s and defined as L/s. L is said
verifier, twin plant, MBRG, etc.). This is due to the
to be extension-closed when L.Σ∗ = L.
high complexity of these constructed models and to
the generation of the whole state-space which may The approach introduced in this paper applies
have considerable time and memory cost. to discrete-events systems modelled by Labelled
Transitions Systems (LTSs for short). The formal
To partially overcome this problem, we propose,
definition of LTS is as follows.
in this paper, an efficient approach to construct
a hybrid diagnoser on-the-fly, in the sense of
Definition 1 (LTS): An LTS over Σ is defined by a
combining enumerative and symbolic techniques.
4-tuple hQ, Σ, →, q0 i, where:
The contributions of this paper are twofold:
• Q is a finite set of states;
1. We provide a behavioural diagnoser based
on the Symbolic Observation Graph (Haddad • Σ is a finite set of events;
et al. 2004) which is an efficient binary
decision diagram (BDD) based abstraction of • →⊆ Q × Σ × Q is the transition relation;
the model state space. Thus, macro-states of
• q0 ∈ Q is the initial state.
the diagnoser will be compacted using BDDs
In the remainder of this section, we consider a given assume that the LTS G under consideration satisfies
LTS G = hQ, Σ, →, q0 i. For q, q 0 ∈ Q and σ ∈ Σ, we the following two assumptions:
σ
denote q −→ q 0 , (q, σ, q 0 ) ∈→. q → means that ∃q 0 ∈
Q:q−
σ
→ q 0 . If s = σ1 , σ2 , . . . , σn is a string (sequence 1. The language generated by G is live, i.e. there
of events), s̄ denotes the set of actions occurring in s. is an executable transition from any state of the
Moreover, q −
s
→ q 0 denotes that ∃q1 , q2 , . . . , qn−1 ∈ Q system.
σ1 σ2 σn ∗
such that, q −→ q1 −→ . . . qn−1 −−→ q0 . q −
→ q0 2. The LTS G is finite, in term of the state space,
0 s
denotes that q is reachable from q (i.e. q − → q 0 for and does not contain cycles formed only by
∗
some s ∈ Σ∗ ), and q − →E q 0 holds if s̄ ⊆ E. unobservable events.
σ
We denote by Enable(q) the set of events σ s.t. q −
→, 3.1. Definition of diagnosability
for a set of states Q0 ⊆ Q, EnableE (Q0 ) denote the
0 Diagnosability is an important property in the
set of enabled eventsS from the set of states Q , i.e.
0 monitoring and fault diagnosis activities. In simple
Enable(Q ) denotes q∈Q0 Enable(q).
terms, it refers to the ability to infer accurately,
An execution from the initial state q0 of an LTS G is from a partially observed execution, about the
σ1 σn
a finite sequence of transitions π = q0 −→ q1 . . . −−→ faulty behaviour within a finite delay after possible
qn . The event-trace of π, denoted by T r(π), is the occurrences of faults. The original definition of
sequence of events σ1 , . . . , σn , π[i] stands for the diagnosability, introduced in the seminal work of
σ1
prefix of π truncated at state qi , i.e., π[i] = q0 −→ (Sampath et al. 1995) is recalled in the following.
σi
q1 . . . −→ qi and last(π) represents the last state of
π. The set of finite executions of LTS G from the initial Definition 2 (diagnosability (Sampath et al. 1995))
state q0 is denoted by Runs(G). The behaviour of G A prefix-closed and live language L is said to be
is described by its language L(G) = {s ∈ Σ∗ |q0 −
s
→}. diagnosable with respect to the projection function P
and with respect to a failure class of faults Σf if the
As we are interested in diagnosis issues, partial following holds
observation plays a central role. In this regard, some
events in Σ are observable, i.e. their occurrence can (∃ni ∈ N) [∀s ∈ Ψ(Σf )] (∀t ∈ L/s) [|t| ≥ ni ⇒ D]
be observed, while the rest are unobservable. U Thus,
where the diagnosability condition D is
the event set Σ can be partitioned as Σ = Σo Σu ,
where Σo denotes the set of observable events and ω ∈ P −1 [P (s.t)] ⇒ Σf ∈ ω.
Σu the set of unobservable events. To reflect the
limitation on observation, we define the projection with Ψ(Σf ) is the set of finite sequences that
function P : Σ∗ → Σ∗o . In the usual manner, P (σ) = σ terminate with a faulty event from Σf .
for σ ∈ Σo ; P (σ) = for σ ∈ Σu , and P (sσ) =
P (s)P (σ), where s ∈ Σ∗ , σ ∈ Σ. Thus, P simply The above definition means the following. Let s be
erases the unobservable events in any event-trace. any sequence generated by the LTS G that ends with
The inverse projection operation PL−1 is defined by a failure event from Σf , and let t be any sufficiently
PL−1 (y) = {s ∈ L(G) : P (s) = y}. Any two executions long continuation of s. Condition D then requires that
π and π 0 are called indistinguishable with respect to every sequence ω belonging to the language that
the projection function P if they can generate the produces the same observable trace as sequence
same observed event-trace. With a slight abuse of s.t (P (ω) = P (s.t)) must hold a failure event from
notation, we write P (π) = P (π 0 ) if π and π 0 are Σf . In other terms, diagnosability requires that every
indistinguishable. failure event leads to observations distinct enough to
identify the failure type within a finite delay.
In the context of fault diagnosis, let Σf ⊆ Σu
denote the set of failure events. They are usually 3.2. Verification of diagnosability
represented using unobservable events, since their
detection and diagnosis would be trivial if they were In order to analyse diagnosability, (Sampath
observable. We partition the set ofUfailureUevents
U into et al. 1995) has proposed a systematic approach
disjoint failure classes Σf = Σf1 Σf2 · · · Σfm , that consists in building a specific model called
with Σfi denotes the failure class fi . diagnoser. It is a deterministic automaton whose
transitions correspond to the observable events of
the system and whose states are estimation system
3. DIAGNOSABILITY ANALYSIS
state associated with labels to indicate if a state is
In this work, only diagnosability analysis of reached by an observable trace containing a faulty
permanent faults is considered. Once a fault has event or not.
occurred, the system remains irreparably faulty. We
Definition 3 (Diagnoser (Sampath et al. 1995)) The diagnoser Gd corresponding to the LTS G
is depicted in Figure 2. There exists a cycle
Let G = hQ, Σ, →, q0 i be an LTS to be diagnosed. of f -uncertain states composed of {3F, 7N } and
A diagnoser of G is a deterministic LTS Gd = {5F, 10F, 12N } w.r.t. the observable sequence (bd)∗ .
hX , Σo , →d , X0 i associated with a tagging function This cycle corresponds to two cycles in the LTS
Diag : X → 24 , with 4 = {N, F } (for only one class G. The 1st one, which is composed of states
of failures). with N means normal and F means {3}, {4}, {5} w.r.t. the sequence (bud)∗ , which is
faulty. reachable from the faulty sequence f a. The 2nd
cycle, which is composed of states {7}, {11}, {12}
Each diagnoser state x has the form x = and reached by the fault-free sequence a. Thus
{(q1 , l1 ), . . . , (qn , ln )}, with qi ∈ Q and li ∈ 4. If we can infer, according to Theorem 1, that there
∀i = 1, . . . , n, we have li = N (resp. li = F ), the exists an f -indeterminate cycle in the diagnoser and
diagnoser state x is said to be N -certain (resp. F - consequently the LTS G is not diagnosable w.r.t. to
certain), otherwise F -uncertain state. faulty class Σf and the projection function P .
For more details about the formal framework and a
algorithmic procedure of constructing the diagnoser, start {1N } {3F, 7N }
we refer the reader to the original paper (Sampath
et al. 1995).
d b
We define an f -indeterminate cycle in a diagnoser
to be a cycle composed exclusively of F -uncertain
diagnoser states and corresponding to the presence {6F } {5F, 10F, 12N }
t
of two cycling traces, in the system, that sharing the
same observable events, such that the faulty event t
f from the class Σf occurs in the 1st trace but not
in the 2nd . The notion of f -indeterminate cycle is Figure 2: Diagnoser Gd of the LTS G
very important, since it helps to give a necessary and
sufficient condition for diagnosability analysis.
It is worth noticing that the diagnoser can be used
Theorem 1 ((Sampath et al. 1995))
either off-line to check diagnosability or on-the-fly by
A system modelled by an LTS G is diagnosable if connecting it to the system in order to provide on-line
and only if there are no f -indeterminate cycles in its diagnosis upon the occurrence of observable events.
diagnoser Gd for any class of faults Σf .
4. SYMBOLIC OBSERVATION GRAPH (SOG)
3.3. Example
In this section, we present the so-called symbolic
Let us consider the LTS G in Figure 1 (adapted from observation graph (Haddad et al. 2004) and we
(Sampath et al. 1995)). The set of observable events show how it is used to abstract LTS behaviour. In
is Σo = {a, b, d, t} and the set of unobservable events (Haddad et al. 2004), the authors have introduced
is Σu = {u, f } with f a faulty event in Σf . the SOG as an abstraction of the reachability
graph of concurrent systems and showed that the
a b u verification of an event-based formula of LTL/X on
2 3 4 5
the SOG is equivalent to the verification on the
f d original reachability graph. The construction of the
SOG is guided by the set of observable events.
t The SOG is defined as a graph where each node
start 1 8 9 u 10 6
b is a set of states linked by unobserved events and
a each arc is labelled with an observable event. The
f t
SOG nodes are called aggregates and may be
b u
7 11 12 represented and handled efficiently using decision
diagram techniques (BDDs, see for instance (Bryant
d 1992)). The SOG is said to be hybrid since it is
both an explicit and a symbolic structure: the graph
is represented explicitly while the nodes are sets of
Figure 1: The LTS G states encoded and managed symbolically. Despite
the exponential theoretical complexity of the size of
a SOG, it has a very moderate size in practice (see
(Haddad et al. 2004; Klai and Petrucci 2008); (Klai Using the results of Section 4, we would use the
and Poitrenaud 2008) for experimental results). SOG to perform a hybrid diagnoser construction.
In order to capture the feature of analysing
In the following, we first define what an aggregate diagnosability which is tracking the ambiguous
is formally, before providing a formal definition of a behaviour of the system, i.e. normal and faulty
SOG associated with an LTS. executions which share the same observable events,
we modify the structure of the aggregate, introduced
Definition 4 (aggregate) in Definition 4, by splitting the set of states (managed
using BDDs) into tow sets of states in the same
Consider
U the LTS G = hQ, Σ, →, q0 i with Σ = aggregate: one set contains normal states, i.e.
Σo Σu . An aggregate a is a non empty set of states states reachable by fault-free sequences, and the
satisfying: q ∈ a ⇔ SaturateΣu (q) ⊆ a; where other contains faulty states, i.e. states reachable by
∗
SaturateΣu (q) = {q 0 ∈ Q|q −
→Σu q 0 }. sequences containing one (or more) faulty events.
Both of sets are represented and managed using
In the following, SaturateΣu is extended to BDDs.
sets
S of states as follows: SaturateΣu (Q0 ) =
q∈Q0 SaturateΣu (q). Figure 3 depicts the general form of a diagnoser
aggregate where two BDDs represent two sets of
Definition 5 (symbolic observation graph) states; BDDn represents the set of normal states,
while BDDf represents the set of faulty ones. The
The deterministic symbolic observation graph set of faulty states may be reached from the set of
SOG(G) associated with an LTS G is an LTS normal states by the occurrence of a faulty event,
hA, Σo , →Σo , a0 i where: and thus a faulty transition form BDDn to BDDf
may exist in any diagnoser aggregate. Depending on
1. A is a finite set of aggregates such that: the executed behaviour, i.e. the executed sequence,
a) There is an aggregate a0 ∈ A s.t. a0 = the diagnoser aggregate may contain the two sets
SaturateΣu (q0 ); of states (BDDs) or only one set. If a diagnoser
b) For each a ∈ A and for each σ ∈ Σo , if aggregate contains only BDDn (resp. BDDf ), it
∃q ∈ a, q 0 ∈
σ
→ q 0 then Saturate({q 0 ∈
/ a: q − / is called an N -certain (resp. F -certain) diagnoser
a|∃q ∈ a, q −
σ 0 0
→ q }) equals a for some aggregate, else it is an F -uncertain diagnoser
aggregate a0 and (a, σ, a0 ) ∈→Σo ; aggregate in the same way as in the classic
diagnoser (Definition 3).
2. →Σo ⊆ A × Σo × A is the transition relation,
obtained by applying 1.b). The dashed arrows show the different possibilities
that a transition from a diagnoser aggregate can
The SOG can be constructed by starting with produce. For instance, observable event b enabled
the initial aggregate a0 and iteratively adding new by the diagnoser aggregate can be enabled from
aggregates as long as the condition of 1.b) holds both normal and faulty sets or from only one set.
(see (Haddad et al. 2004) for a construction This feature will be considered during the on-the-fly
algorithm). construction of our hybrid diagnoser, since we do not
need to construct the diagnoser aggregates reached
through an observable event from only the faulty set
5. USING SOGS TO ANALYSE of an aggregate. Moreover, this information will be
DIAGNOSABILITY used to establish some heuristics that prioritizing the
branches to be followed while building the hybrid
In this section, we discuss how the SOG is used in diagnoser.
order to build a hybrid diagnoser and we provide an
on-the-fly algorithm to construct the hybrid diagnoser
and to verify diagnosability simultaneously.
The underlying idea behind using SOG for diag-
nosability analysis is basically to tackle the state
explosion phenomenon raised when building the
diagnoser. It is worth recalling here that the Sam-
path’s diagnoser is computed with an exponential
complexity regarding the state space of the model
Figure 3: A diagnoser aggregate
(Sampath et al. 1995). Obviously, this represents a
serious limit of the diagnoser based approach when
large models are handled.
Definition 6 (diagnoser aggregate) b. a0 .Qf =
U SaturateΣu (Img(a0 .Qn , f ) ∪
Consider an LTS G = hQ, Σ, →, q0 i with Σ = Σo Σu Img(a.Qf, σ)).
and Σf ⊂ Σu . A diagnoser aggregate a = hQn , Qf i
is a non empty set of states satisfying: 2. If σ ∈ Enable(a.Qn )\Enable(a.Qf ) then:
∗f ∗ a. a0 .Qn = SaturateΣu \Σf (Img(a.Qn , σ)).
1. ∀q ∈ Q s.t. q0 −−→ q (i.e. q is reachable by a
b. a0 .Qf = SaturateΣu (Img(a0 .Qn , f )).
faulty sequence): q ∈ a ⇔ SaturateΣu (q) ⊆
a.Qf ; 3. If σ ∈ Enable(a.Qf )\Enable(a.Qn ) then:
2. ∀q ∈ Q s.t. q0 −
∗
→Σ\Σf q (i.e. q is a. a0 .Qn = ∅.
reachable by a fault-free sequence): q ∈ b. a0 .Qf = SaturateΣu (Img(a.Qf , σ)).
a ⇔ Q0 = SaturateΣu \Σf (q) ⊆ a.Qn ∧
SaturateΣu (Img(Q0 , f ) ⊆ a.Qf . These rules preserve a specific fault propagation.
From an F -uncertain diagnoser aggregate, we can
s s0
3. ∀q, q 0 ∈ a, ∃s, s0 ∈ Σ∗ , s.t. q0 −
→ q, q0 −→ q 0 , and reach either another F -uncertain, an F -normal
0 or an F -certain diagnoser aggregate, from an N -
P (s) = P (s )
certain diagnoser aggregate, we can reach either
with SaturateΣu \Σf (q)={q 0 ∈ Q|q →Σu \Σf q 0 }, and another N -certain diagnoser aggregate or an F -
f uncertain one, and finally from an F -certian
Img(Q0 , f )={q 0 |q ∈ Q0 : → q 0 }, i.e. it returns
q −
the set of immediate successors of states in Q0 diagnoser aggregate, we can reach only another F -
through the occurrence of event f . certain diagnoser aggregate, which depicts exactly
the hypothesis of permanent failures. Figure 4
To simplify the notation, we denote by a.Qn (resp. illustrates these points.
a.Qf ) the set of normal (resp. faulty) states in an
aggregate a.
5.1. Constructing the hybrid diagnoser N -certain F -uncertain
We now introduce the hybrid diagnoser which is a
modified SOG built from the LTS model G.
Definition 7 (hybrid diagnoser)
F -certain
The hybrid diagnoser DSOG (G) associated with an
LTS G is a modified SOG hΓ, Σo , →SOG , Γ0 i.
Figure 4: Fault propagation on the hybrid diagnoser
1. Γ is a finite set of diagnoser aggregates.
2. Γ0 is the initial diagnoser aggregate with; Example 1 Figure 5 represents the hybrid diag-
noser associated with the LTS of Example 1, de-
a) Γ0 .Qn = SaturateΣu \Σf (q0 ); picted in Figure 1. As it is intended to construct
b) Γ0 .Qf =SaturateΣu (Img(Γ0 .Qn , f )). the hybrid diagnoser on-the-fly, it is more convenient
to represent the hybrid diagnoser as a tree-like
3. →SOG ⊆ Γ × Σo × Γ is the transition relation, structure.
defined as below,
∀a, a0 ∈ Γ, σ ∈ Σo s.t. σ ∈ Enable(a.Qn ∪a.Qf ): The initial aggregate composed of the initial state
σ of the LTS and the state 2 reachable from state
→SOG a0 ⇔ a0 .Qn = SaturateΣu \Σf (Img(a.Qn , σ))
a−
1 by the occurrence of faulty event f . Both of the
∧ a0 .Qf =SaturateΣu (Img(a0 .Qn , f ) ∪ diagnoser aggregates (2) and (3) contain two sets
Img(a.Qf, σ)) of states (each one is represented by a BDD).
After the occurrence of event d we reach diagnoser
To summarize, the hybrid diagnoser DSOG (G) is aggregate (4), which is the same as diagnoser
constructed as follows: let the current aggregate of aggregate (2) thus, there exists a cycle on the
the diagnoser be a, and the next observed event be hybrid diagnoser composed of aggregates (2) and
σ. The target diagnoser aggregate a0 of the hybrid (3) by executing the observable event sequence
diagnoser is computed following these rules: (bd)∗ . Diagnoser aggregate (5) is reached after the
occurrence of event t and it contains only the set
1. If σ ∈ Enable(a.Qn ) ∩ Enable(a.Qf ) then: of faulty states thus, it is an F -certain diagnoser
a. a0 .Qn = SaturateΣu \Σf (Img(a.Qn , σ)). aggregate. As F -certain diagnoser aggregates are
not necessary to analyse diagnosability, in on-the- • EnableObs(S) returns the set of observed
fly constructing of the hybrid diagnoser, we do events that are enabled by at least one of the
not construct them. Indeed, one knows that all states in set S.
the subsequent aggregates will be F -certain as
well. Besides, computing such aggregates is not • SaturateΣi (), as defined before, computes the
necessary for online diagnosis. various states reached through events from set
Σi .
• Stack is an ordered set of 5-uplet, which
contains two sets of states (Sn , Sf ) and three
sets of events (Evtf , Evtn , Evt) with Evt =
(Evtn ∪ Evtf )\(Evtn ∩ Evtf ).
• IsU ncertain() is a function that returns
Boolean value (true if the encountered cycle
is composed of only f -uncertain diagnoser
aggregates and f alse otherwise).
• IsIndeterminate(): is a function that returns
Boolean value (true if the existing cycle is an f -
indeterminate cycle and f aulse otherwise. This
function will be discussed later.
• RemoveLast(S) is an operation that removes,
then returns, the last event of a set S.
Figure 5: Hybrid diagnoser of the LTS in Figure 1.
• For the sake of simplicity, we consider that Σf
We recall that our goal is to avoid the state-explosion contains only one faulty event, generalization
problem, not only by providing this compact form to a set of faulty events is straightforward.
(SOGs) to build the hybrid diagnoser but also by
constructing the hybrid diagnoser on-the-fly and The initialization step (lines 1-11) serves to compute
verifying diagnosability simultaneously. Constructing the initial diagnoser aggregate, handle it efficiently
the hybrid diagnoser on-the-fly serves to avoid using OBDD (function Reduce()), and push it,
generating the whole state space of the diagnoser associated with its enabled observable events, into
even if the system is diagnosable, i.e. as we deal the stack. The construction of the hybrid diagnoser
with permanent faults, we do not need to construct is performed using a depth first exploration: As long
the part, of the hybrid diagnoser, containing only F - as the stack in not empty, a new observable event t,
certain diagnoser aggregates since such a part is not enabled by the diagnoser aggregate a at the top of
necessary for analysing diagnosability (see (Liu et al. the stack, is removed from the set of enabled events
2014a) for more details). (Evt) and then processed. If such an event does
not exist, the corresponding aggregate is poped from
Hereafter, we provide the SOG-based algorithm the stack (lines 13-15). Otherwise, if the set Evtn of
needed for on-the-fly construction of the hybrid events enabled by the set of normal states Sn of the
diagnoser. The following function and data structures diagnoser aggregate a, is empty then the aggregate
are used: a is poped from the stack (lines 16 and 18). This step
serves to avoid the construction of the subsequent
• Img(S, t), as described previously, returns the F -certain diagnoser aggregates, i.e. since this part
set of immediate successors of the states of a of the hybrid diagnoser is not necessary to analyse
set S through the occurrence of event t. diagnosability.
• OBDDs (Ordered Binary Decision Diagram)
The computation of the new aggregate a0 , reachable
are used to represent the sets of states
through an observable event from aggregate a, is
belonging to an aggregate, i.e. the set of
completed by saturation on the unobservable events
normal states and the set of faulty states in
(lines 20-26). If a0 has already been encountered
an aggregate. This task is performed by the
(i.e. existence of a cycle) then the hybrid diagnoser
function Reduce().
is updated by adding a new edge (lines 27-28)
• The hybrid diagnoser is represented by a and if the cycle is uncertain (i.e., contains only
standard graph representation with a set of f -uncertain diagnoser aggregates), the function
vertices, namely V , and a set of edges, namely IsIndeterminate() is launched in order to detect
E, connecting these aggregates and labelled whether there exists an f -indeterminate cycle or
with observable events. not (line 29-32). If the cycle is an f -indeterminate
one then we output that the model is undiagnosable reached by executing the observed event-sequence
and we stop the diagnoser construction. Otherwise, a(bd)∗ .
construction is continued, a0 with its enabled
observable events are pushed into the stack, and Algorithm 1 On-the-fly algorithm to construct the
so on. When the stack is empty, then the necessary hybrid diagnoser
part of the diagnoser, for analysing diagnosability,
DiagSOG (LT S, Σo , Σu , f );
is completely built, we output that the model is
Diagnoser aggregate a, a0 ;
diagnosable.
Set of vertices V ;
As mentioned in Section 3, diagnosability analysis Set of edges E;
is performed by searching two infinite executions Set of Events Evtn , Evtf , Evt;
that share the same observed event-sequences Set of states Sn , Sf , Sn0 , Sf0 ;
such that one sequence contains a faulty event Stack st = ∅;
and not the other one. That means to search an
f -indeterminate cycle in the diagnoser (Sampath 1: Sn = SaturateΣu \f (q0 );
et al. 1995). The same procedure is used in our 2: Sf = Img(Sn , f );
case, i.e. searching f -indeterminate cycles in the 3: if (Sf 6= ∅) then
hybrid diagnoser. Two steps are needed to check 4: Sf = SaturateΣu (Sf );
the existence of f -indeterminate cycles when a cycle 5: end if
of F -uncertain diagnoser aggregate is found in the 6: a = hSn , Sf i;
hybrid diagnoser: 7: Reduce (a, Σu );
8: V = a; E = ∅;
1. Extract the observed event-sequence that 9: Evtn = EnableObs(Sn );
leads to this cycle (of F -uncertain diagnoser 10: Evtf = EnableObs(Sf );
aggregates). 11: st.Push(hSn , Sf , Evtn , Evtf , Evti;
12: while (st 6= ∅) do
2. Check if this observed event-sequence corre- 13: hSn , Sf , Evtn , Evtf , Evti = st.Top();
sponds to two cycle in the LTS model. One 14: if Evt = ∅ then
cycle is reached by a fault-free event-sequence 15: hSn0 , Sf0 , Evtn , Evtf , Evti = st.Pop();
and the other one is reached by a faulty event- 16: else
sequence. 17: if (Evtn = ∅ then
18: hSn0 , Sf0 , Evtn , Evtf , Evti = st.Pop();
This task is performed by function 19: else
IsIndeterminate() in the Algorithm 1 (line 28) 20: t = RemoveLast(Evt);
which calls a specific function (path exists()) from 21: Sn0 = Img(Sn , t);
the digraph library (Rushton 2012). (digraph is 22: Sn0 = SaturateΣu \f (Sn0 );
a library dedicated for searching cycles from the 23: Sf0 = Img(Sf , t) ∪ Img(Sn0 , f );
system model). 24: Sn0 = SaturateΣu (Sf0 );
25: a0 = hSn0 , Sf0 i;
We emphasize that verification of the existence of
26: Reduce (a0 , Σu );
f -indeterminate cycles is performed on-the-fly in
27: if (∃w ∈ V | w = a0 ); then
parallel to the process of constructing the hybrid t
diagnoser, i.e. the process of constructing the hybrid 28: E =E∪a→ − SOG w;
diagnoser runs and when a cycle of F -uncertain 29: if (IsU ncertain()) then
diagnoser aggregates is found, we check whether 30: if (IsIndeterminate()) then
this cycle corresponds to an f -indeterminate cycle 31: return UNDIAGNOSABLE;
or not. If it is the case (i.e. the cycle is an f - 32: end if
indeterminate cycle), then the whole process is 33: end if
stopped and a negative verdict is emitted regarding 34: else
diagnosability, else the building process is continued. 35: V = V ∪ {a0 };
t
36: E =E∪a→ − SOG a0 ;
Example 2 Let us take again LTS G of Figure 1 and 37: Evtn = EnableObs(Sn0 );
its hybrid diagnoser (Figure 5). We have a cycle, in 38: Evtf = EnableObs(Sf0 ;
the hybrid diagnoser, composed of only F -uncertain 39: st.PushhSn0 , Sf0 , Evtn , Evtf , Evti;
diagnoser aggregates (2) (3). Once the algorithm 40: end if
of construction arrives at this cycle, we check if 41: end if
this cycle is an f -indeterminate one or not, before 42: end if
continuing the construction process. The cycle of 43: end while
f -uncertain diagnoser aggregates (2) (3) is 44: return DIAGNOSABLE;
In LTS G, the observed event-sequence a(bd)∗
corresponds to two event-sequences:
1. The faulty sequence f a(bud)∗ that leads to a
cycle composed of states 3, 4, and 5.
2. The fault-free sequence a(bud)∗ that leads to a
cycle composed of states 7, 11, 12.
Thus, we can infer that the cycle, in the hybrid
diagnoser, composed of diagnoser aggregates (2) Figure 6: Types of enabled transitions from an
and (3) is an f -indeterminate cycle. Thus, we stop aggregate
constructing the hybrid diagnoser and we output that
LTS G is non diagnosable with respect the fault f .
to direct the construction of the hybrid diagnoser and
5.2. A heuristic strategy to improve the building to potentially speed up the verification process. We
algorithm note that in the actual version of the algorithm, this
heuristic strategy is not implemented.
Our algorithm for constructing the hybrid diagnoser
is based on a depth-first search (DFS) to investigate
the state space (diagnoser aggregate in the devel- 6. RELATED WORKS
oped tree-like structures) execution by execution.
Generally, no rules are defined to select the execu- In the literature, there are several diagnoser-based
tion to be investigated first, i.e. the order of execution approaches for analysing diagnosability inspired
exploring is arbitrary. However, as we deal with from the seminal work of (Sampath et al. 1995). In
diagnosability analysis, in our case, the diagnoser (Zad et al. 2003) a state-based approach for on-line
aggregate structure provides some information that passive fault diagnosis was introduced. In the state-
can be exploited to direct the search in such a way based approach, it is assumed that the set of states
as to increase the chances of quickly obtaining a di- of the system model can be partitioned according
agnosability verdict by exploring the most promising to the faulty or normal condition of the system. In
executions at first. this work, a specific diagnoser is constructed as
a finite state machine that takes information from
When we deal with diagnosability analysis, the the system (i.e. sequences of inputs/outputs) and
interesting executions of the system are those which generates an estimate of the condition of the system
share the same observed event-sequence such (i.e., faulty or normal). Establishing of this diagnoser
that some of them contain a faulty event and the has exponential time complexity. However, a model
others are fault-free. This is reduced to track the reduction scheme with polynomial time complexity is
observed event-sequences, in the hybrid diagnoser, proposed to reduce the computational complexity of
leading to F -uncertain aggregates. Generally, there the procedure.
exists three types of enabled transitions from any
aggregate, as depicted in Figure 6. (Schumann et al. 2004) propose a symbolic
framework based on binary decision diagrams
1. Transitions enabled only by states from the for the diagnosis of DESs. A symbolic version
faulty set (Figure 6.(a)). As said before, this of Sampath’s diagnoser was proposed, while
type of branches will not be explored. requiring considerably lower space and time than
the enumerative approach of (Sampath et al.
2. Transitions enabled only by states from the
1995). Recently, (Liu et al. 2014a) propose an
normal set (Figure 6.(b)). In this case, we need
on-the-fly algorithm for constructing and checking
to continue the construction since other faults
diagnosability of discrete-event systems modelled by
may occur in the future.
LPNs using an enumerative approach. The goal is
3. Transitions enabled from both normal and to avoid the construction of the whole state-space
faulty sets (Figure 6.(c)). In this case, the of the diagnoser especially when the system is not
reached diagnoser aggregate will be certainly diagnosable. The approach was experimented over
F -uncertain. a Petri net benchmark and the obtained results
were promising compared to those of Sampath’s
This last type of transitions is the most-promising to approach. A tool, called OF-PENDA (Liu et al.
find an f -indeterminate cycle since we know, a priori, 2014b), was developed based on this approach to
that the new diagnoser aggregate will be certainly an analyse diagnosability, K-diagnosability and Kmin -
f -uncertain aggregate, contrary to the other above diagnosability of systems, modelled by Labelled Petri
cases. Thus, it will be the first to be explored in order Nets.
The approach proposed in this paper, takes on Automatic Control, pages 46(8), 1318–1321,
advantage from these two last approaches (i.e., 2001.
(Schumann et al. 2004) and (Liu et al. 2014a)) by
combining the symbolic representation of diagnoser T. S. Yoo and S. Lafortune. Polynomial-time
states and on-the-fly techniques for constructing the verification of diagnosability of partially observed
hybrid diagnoser and verifying diagnosability. We discrete-event systems. IEEE Transactions on
believe that this approach will improve efficiently Automatic Control, pages 47(9), 1491–1495,
analysis of diagnosability in terms of runtime 2002.
and memory resources. We still need to apply A. Cimatti, C. Pecheur, and R. Cavada. Formal
the approach on several benchmarks in order to verification of diagnosability via symbolic model
assess its efficiency. Indeed, determining analytical checking. Int. Joint Conference on Artificial
complexity while considering the worst case is not Intelligence, 2003.
appropriate for such an on-the-fly approach.
A. Boussif and M. Ghazel. Diagnosability analysis
of input/output discrete event system using model
7. CONCLUSION checking. The 5th International Workshop on
Dependable Control of Discrete Systems, 2015.
In this work, we have developed an on-the-fly
approach for diagnosability analysis, based on a J. Peterson. Petri Net Theory and the Modeling of
hybrid diagnoser. The approach is based on the Systems. Prentice Hall PTR, 1981.
symbolic observation graph (SOG), which is a
paradigm that combines symbolic and enumerative T. Ushio, I. Onishi, and K. Okuda. Fault detection
representations in order to build a deterministic based on Petri net models with faulty behaviors.
observer from a partially observed model. The Systems, Man, and Cybernetics, pages 113–118,
approach aims to improve the efficiently in terms 1998.
of runtime and memory resources when analysing Y. Wen and C. Li. A polynomial algorithm for
diagnosability. checking diagnosability of Petri nets. IEEE
International Conference on Systems, Man and
Several future directions are considered. First, Cybernetics, 3:2542–2547, 2005.
we wish to make experimentations over case-
studies in order to assess the efficiency and the M. P. Cabasino, A. Giua, S. Lafortune, and C. Seatzu.
scalability of our approach and also to compare Diagnosability analysis of bounded Petri nets.
the obtained results with those provided by other Proceedings of the 48th IEEE Conference on
existing approaches. Then, we will investigate Decision and Control (CDC) held jointly with 28th
some other practical versions of diagnosability, Chinese Control Conference, pages 1254–1260,
namely K-diagnosability and Kmin -diagnosability. 2009.
Finally, we intend to extend the proposed approach
for analysing diagnosability based on the verifier F. Basile, P. Chiacchio, and G. De Tommasi. On
approach by means of a non deterministic version k-diagnosability of Petri nets via integer linear
of the symbolic observation graph. programming. Automatica, 48(9):2047–2058,
2012.
REFERENCES M. P. Cabasino, A. Giua, and C. Seatzu. Diagnosabil-
ity of discrete-event systems using labeled Petri
J. Zaytoon and S. Lafortune. Overview of fault nets. IEEE Transactions on Automation Science
diagnosis methods for discrete event systems. and Engineering, 11(1):144–153, 2014.
Annual Reviews in Control, pages 308–320, 2013. B. Liu, M. Ghazel, and A. Toguyéni. Toward an
C. G. Cassandras and S. Lafortune. Introduction to efficient approach for diagnosability analysis of
discrete event systems. Second Edition, Springer, des modeled by labeled petri nets. Proceeding of
2007. the 13th European Control Conference, 2014a.
M. Sampath, R. Sengupta, and S. Lafortune. S. Haddad, J.-M. Ilié, K. Klai, and F. Wang. Design
Diagnosability of discrete-event systems. IEEE and Evaluation of a Symbolic and Abstraction-
Transactions on Automatic Control, pages 1555– based Model Checker. 2nd International Sympo-
1575, 40(9), 1995. sium on Automated Technology for Verification and
Analysis (ATVA’04), pages 198–210, 2004.
S. Jiang, Z. Huang, V. Chandra, and R. Kumar.
A polynomial algorithm for testing diagnosability R. E. Bryant. Symbolic boolean manipulation with
of discrete-event systems. IEEE Transactions ordered binary-decision diagrams. ACM Comput.
Surv., 24(3):293–318, 1992.
K. Klai and L. Petrucci. Modular construction of the
symbolic observation graph. The 8th International
Conference on Application of concurrency to
System Design, pages 23–27, 2008.
K. Klai and D. Poitrenaud. MC-SOG: An LTL model
checker based on symbolic observation graphs.
Proceedings of the 29th International Conference
on Application and Theory of Petri Nets, pages
23–27, 2008.
A. Rushton. A directed graph conainer. http://
www.andyrhshton.co.un/programming/stlplus-
library-collection, 2012.
S. H. Zad, R .H. Kwong, and W. M. Wonham. Fault
diagnosis in discrete-event systems: Framework
and model reduction. IEEE Transactions on
Automatic Control, 48(7):1199–1212, 2003.
A. Schumann, Y. Pencole, and S. Thiebaux.
Diagnosis of discrete event systems using ordered
binary decision diagrams. 15th International
Workshop on Principles of Diagnosis, 2004.
B. Liu, M. Ghazel, and A. Toguyéni. OF-PENDA:
A software tool for fault diagnosis of discrete
event systems modeled by labeled petri nets.
International Worshop Petri Nets for Adaptive
Discrete-Event Control Systems, 2014b.