=Paper=
{{Paper
|id=Vol-1256/paper4
|storemode=property
|title=A µ-Calculus Framework for the Diagnosability of Discrete Event Systems
|pdfUrl=https://ceur-ws.org/Vol-1256/paper4.pdf
|volume=Vol-1256
|dblpUrl=https://dblp.org/rec/conf/vecos/GhazelP14
}}
==A µ-Calculus Framework for the Diagnosability of Discrete Event Systems==
https://ceur-ws.org/Vol-1256/paper4.pdf
45
An Operative Formulation of the Diagnosability
of Discrete Event Systems Using a Single
Logical Framework
Florent Peres Mohamed Ghazel
Univ. Lille Nord de France, F-59000 Lille, Univ. Lille Nord de France, F-59000 Lille,
IFSTTAR, COSYS/ESTAS IFSTTAR, COSYS/ESTAS
F-59650 Villeneuve d’Ascq F-59650 Villeneuve d’Ascq
florent.peres@ifsttar.fr mohamed.ghazel@ifsttar.fr
Diagnosability is a procedure whose goal is to determine whether any failure – or a class of failures – can
be determined in finite time after its occurrence. Earlier works on diagnosability of discrete event systems
(DES) establish some intermediary models from the analyzed model and then call some procedures to check
diagnosablity based on these models, while recent works try to give a diagnosability formulation as a model-
checking problem. However, there still lacks a single framework able to handle both of the diagnosability
issues: how to model the problem? and how to decide it? In this paper, we build on some existing works
which have formally established necessary and sufficient conditions for diagnosability of DES and we
propose a generic operative formulation of diagnosability using the µ-calculus logic, which allows resolving
the diagnosability issue within a single formalism.
Diagnosis, Diagnosability, Monitoring, Discrete event system, µ-calculus
1. INTRODUCTION The diagnoser implementation issue comes next.
The Diagnoser ensures online monitoring and
Fault detection and isolation (FDI) is a crucial task, determines whether the system behavior is faulty
both for safety and productivity reasons. Moreover, and which type is the fault.
systems become more and more complex, thus
making monitoring/diagnosis a challenging task Diagnosability of DES has been defined first in
especially in automated systems. A typical issue to the seminal work of Sampath (1995). Some slight
deal with when performing the diagnosis process is variations can also be found like for instance
that of partial observability. Actually, it is often difficult I-diagnosability which makes fault determination
and costly to detect all the changes that may occur conditioned by the occurrence of some indicator
within a complex system. Indeed, for technical and/or events. Such definitions state when a system is
economic reasons, setting enough devices/sensors said diagnosable and some procedures based on
to catch all the information needed for control and intermediate automata models are then needed
supervision is generally unfeasible when dealing with to actually investigate diagnosability. Later, model-
large complex systems. Consequently, it becomes checking techniques were used in Cimatti (2003),
essential to develop efficient techniques to carry Huang (2004) and Grastien (2009), coming closer
out FDI tasks. At a high level, discrete event and closer to an operative definition. Nevertheless,
models Cassandras (2008) are more convenient these works all have a common point: they must
for diagnosis studies than continuous models, first build an intermediary model of the behavior,
which are more appropriate for detailed levels called twin plant, before being able to apply model-
Lin (1994). Basically, two main issues are tackled checking. Thus, none of those works actually gives
when dealing with diagnosis of discrete event a unified operative definition. Such a definition must
models: examinating diagnosability and developing use a language whose semantics describes how to
diagnosers. Diagnosability investigation is performed achieve all the required steps (which is true for the
offline, and consists to determine whether every fault latter cited works) while being able to express the
-or category of faults- can be detected and identified problem as a whole.
in finite time, consecutively to its occurrence.
46
In this paper, an operative definition of diagnosability concatenation operation complies with the property
is developed, while using a slight variant of µ- |ab| = |a| + |b|. Using concatenation, it can be
calculus1 , as it was initially proposed in Park (1976). helpful to confuse the 1-length words (|w| = 1) with
This logic is basically a predicate calculus extended characters, and to consider the empty word as a
with traditional fix-point operators µ and ν. The “hidden” word/character. For w = ab, a and b are
benefits of such a logic is that it is extremely powerful called prefix and suffix of w, respectively. A language
from a theoretical point of view (even modal µ- L is called prefix-closed iff each prefix of each word
calculus can be expressed using µ-calculus), but in L is in L, i.e. (∀w ∈ L)({a | ∃b, w = ab} ⊆ L).
especially that it is decidable for finite DES. Last
but not least, there exists a tool, MEC 5 Griffault For w ∈ L, wi denotes the ith character of w. For
(2004), Vincent (2003), (now incorporated within i ∈ N \ {0} ∀ i > |w|, wi = and w1 is the first
ARC), for checking µ-calculus formulas on Altarica character. By abuse of notation, if α ∈ Σ and w ∈ Σ∗ ,
Arnold (1999) systems. By operative definition, we then α ∈ w iff (∃i)(wi = α).
mean a definition that can be used directly to perform
the diagnosability analysis. Now, we will define diagnosability as given in the
seminal work of Sampath (1995). Let L be a prefix-
Using a single logical framework to give a formulation closed language on the set of events Σ. Σ is
of diagnosability does not necessarily mean that the partitioned into Σo , the set of observable events, and
problem has been simplified. Indeed, we will see Σu the set of all unobservable events, which is in
that some of the steps of our formulation are quite turn partitioned into Σf , the set of all faulty events
close to the cited works, especially those using a twin and Σh = Σu \ Σf denoting the set of unobservable
plant/verifier. Nevertheless, the benefits of using a events which are not faulty (harmless).
single framework is twofold: from a theoretical point
of view, this shows the existence of such a logical We consider the following assumption: once a
operative framework able to express the problem as fault has occurred, the system remains irreparably
a whole. Then from the practical point of view, this faulty, that is to say faults are permanent. More
provides a way to quickly implement and experiment precisely, given a sequence of alternating states
diagnosability only by looking at the semantics, and and transitions, once a fault has occurred, every
hopefully will it be useful to extend the diagnosability subsequent state eventually reached is considered
facilities, as will be shown in the sequel. faulty. From the monitoring point of view, this means
The paper is organized as follows: In section 2, we we do not consider any maintenance operation that
introduce diagnosability of DES as well as some may be performed on the system.
related notations. Section 3 is devoted to give an
overview on the related works. In section 4, we Definition 1 Πf is a partition of the set of faults
U Σf .
discuss our µ-calculus formulation for diagnosability Each subset i is denoted Σfi , that is Πf = i Σfi .
of DES. Section 5 gives a brief discussion about
complexity and finally section 6 concludes the paper Definition 2 Ψ(Σfi ) is the set of sequences ending
while driving some perspectives for this work. with a fault in Σfi : (∀s ∈ L)(∀fi ∈ Σfi )(s|s| = fi ⇔
s ∈ Ψ(Σfi ))
2. DIAGNOSABILITY Definition 3 L/s = {t ∈ Σ∗ |s.t ∈ L} is the set of all
suffixes of s in L.
2.1. Definition
Definition 4 (∀i)((si ∈ Σo ⇒ P (s)i = si ) ∧ (si ∈
To properly give the definition of diagnosability that Σu ⇒ P (s)i = )), defines the projection P (s) of
we consider, we need to introduce some concepts sequence s on the set of observable events Σo : if si is
and notations relative to language theory. observable, then P (s)i = si , but if si is unobservable
then P (s)i = .
An alphabet is a set of characters or symbols,
usually denoted Σ. A word is a sequence –or string–
Definition 5 PL−1 (y) = {s ∈ L|P (s) = y} gives all
of characters. The set of all finite length words,
the sequences s in L for which the projection on Σo
composed of characters in Σ is denoted Σ∗ . A
gives y.
language over Σ is a subset of Σ∗ . A word is empty
if it contains no letter, and is denoted . If w is a
Definition 6 (Diagnosability Sampath (1995))
word then |w| denotes its length, i.e. the length of
the character sequence constituting w (|| = 0). (∀i ∈ Πf )(∃ni ∈ N)(∀s ∈ Ψ(Σfi ))(∀t ∈ L/s)
Two words a and b can be concatenated to form
a new word denoted a.b (or ab for short). The (|t| ≥ ni ∧ w ∈ PL−1 (P (s.t)) ⇒ ∃(f ∈ Σfi )(f ∈ w))
1 Please note the absence of ”modal”
47
Informally speaking, this definition states that a two consecutive occurences of b. Therefore, when a
given language is diagnosable iff for any sequence fault f occurs, the projection on the set of observable
w with the same observable projection than a events results in a sequence starting with b or it
faulty sequence s.t with s|s| ∈ Σfi , and t is will include at least two consecutive b’s. Both cases
sufficiently long, then w necessarily contains a fault cannot be obtained without the occurrence of f .
from Σfi . Reasoning directly on languages is not
always possible, because they are often infinite. An
alternative is to use labeled transition systems (LTS). 3. RELATED WORKS
Several reference works in diagnosis of DES can
Definition 7 A labeled transition system (LTS) is a
be found in the literature, these works can be
tuple (Q, q0 , Σ, −
→), in which:
distinguished mainly according to the notations
• Q is a set of states used, to the framework considered (centralized
vs. distributed, untimed vs. timed), to the type
• q0 is the initial state of faults (permanent vs. transient) or also to the
procedures adopted to investigate diagnosability.
• Σ is a set of events
Sampath (1995) is a pioneer work in the DES
• −
→: Q × Σ × Q is the transition relation diagnosis field, that has been improved in terms
of computational complexity in Yoo (2002). Jiang
We say that an LTS recognizes a word w = x1 . . . xn (2001) proposes an efficient way to investigate
x1 xn diagnosability of DES modeled with state finite
iff q0 −→ . . . −−→, or in other words if the sequence
of events given by w can occur from q0 . The set of automata. In Basile (2010), Cabasino (2010), Genc
recognizable words forms the language recognized (2007), Liu (2014), Ushio (1998) the authors analyze
by the LTS. By extension, we say that an LTS is diagnosis on systems modeled by Petri nets. On
diagnosable (resp. not diagnosable), iff the language the other hand, Tripakis (2002), Jiroveanu (2006),
it recognizes is diagnosable (resp. non-diagnosable). Ghazel (2009) and Basile (2013) deal with diagnosis
within a timed framework, namely based on timed
2.2. Example automata and petri net models. For a complete
overview on the literature pertaining to the diagnosis
For the LTS in Figure 1, the set of observable events of DES, the reader can refer to Zaytoon (2013) which
is {a, b}, while f is a fault (thus unobservable). The offers a wide survey on the state of the art.
LTS is not diagnosable and the explanation is quite
simple: any word of the language (ab)∗, coming In this section, we will briefly discuss existing
from an observable projection, can originate either techniques on diagnosability of DES using a
from a recognized sequence containing a fault (any logical framework for which there is a well defined
word in f (ab)∗ satisfies this), or from a non-faulty operational semantics. One may distinguish two sub-
sequence (any word in (ab)∗ also verifies this). Thus, issues: the first is about developing a diagnosability
there is no length n, such that after this length, one decision procedure transformed into a model-
can always distinguish faulty sequences from normal checking problem; and the second is related to the
ones, based on observed events. specification of the faulty behavior.
On the other hand, the language recognized by the 3.1. Twin Plant
automaton of Figure 2 is diagnosable.
Although diagnosability is not defined using an
a “operative” logical framework, the originality of this
a
0 1 work comes from its efficient decision procedure,
b 0 4 which has been widely reused in several subsequent
b
works. The authors of Jiang (2001) use the same
f
a definition of diagnosability as in Sampath (1995) and
f b propose a polynomial algorithm, thus optimizing the
2 3
2 3 diagnosability decision in comparison with that of
b Sampath (1995). The main idea is to drop the use
a
of a diagnoser when checking whether a model is
Figure 1: A is not diagnos-
Figure 2: B is diagnosable diagnosable.
able
The decision procedure is composed of three steps.
The difference between automata A and B is the From the original LTS G = (X, q0 , Σ, − →), one
appearance order of the observable events after the proceeds as follows:
fault f . In B, a fault may appear either from the initial
state, followed by an occurrence of b, or between
48
• Construction of Go = (Xo , q0 , Σo , −
→o ), the In Huang (2004), the diagnosability problem has
“observable” version of G: been dealt with using a CT L∗ formula for the
first time. Once again, it is still necessary to first
a) Xo = {(x, f ) | x ∈ Q1 ∪ {q0 } ∧ f ⊆ F}, where build a twin plant Gd . Unlike the approach of
e
Q1 = {x ∈ Q | (∃x0 ∈ Q)(∃e ∈ Σo )(x0 − → x)}, i.e. Cimatti (2003), the authors use the same definition
Xo is the set of states which are the destination of as in Sampath (1995). The model expressing the
an observable transition (Q1 ), plus the initial state q0 . system dynamics is extended with a new variable
Each state is labeled with a set of faults f , indicating denoting fault occurrence (Boolean). The twin plant
which ones may have occurred before reaching this is thus analyzed to find states corresponding to the
state. composition of a “faulty” state with a “normal” state
e∈Σ (information given by the added boolean variable) by
b) − →o : Xo × Σo × Xo is such that (x, f ) −−−→ o
o model-checking techniques. In Grastien (2009), the
σ e
(x0 , f 0 ) iff (∃σ ∈ Σ∗u , x00 ∈
X) x −
→ x00
−
→ x 0
∧ authors use a substantially similar method.
f 0 = {fi | σ j ∈ Σfi } ∪ f . This is the observable
reachability: if a state x0 is reachable from a state 3.4. Fault specification
x by an unobservable sequence, or the empty
sequence, directly followed by an observable event Diagnosability can be extended using a more
e, then (x, e, x0 ) is in −
→o . general fault specification: instead of pointing only
faulty states or events, one may also express that
• Construction of Gd = (Go ||Go ) = (Xo × Xo , (qo , qo ), a given behavior is faulty (resp. normal) if it satisfies
⇒), where || is the usual parallel composition,
Σo , = (resp. does not satisfy) a certain formula specifying
for which only the following rule applies, because the faulty (resp. safe) behavior.
the two composed LTS are the same (clones):
a∈Σo 0 a∈Σo 0 In Jiang (2004), the authors use an LTL formula f to
q −−−→ o q r −−−→ o r
a
specify the boundary of the normal (safe) behavior:
⇒ q 0 ||r0
q||r = each state outside this boundary is considered as
to be faulty. In particular, usual faults are specified
• And finally, a cycle-checking pass is needed within using safety properties: if e is a faulty event, then
σ a
Gd : for every cycle q1 = ⇒ qn =⇒ q1 , where σ ∈ Σ∗o and ¬e gives the normal behavior. However, what is
a ∈ Σo , if (∀i, j ∈ [1, n])(qi = (s, f 1 ) ∧ qj = (s0 , f 2 ) ⇒ particularly interesting in this approach lies in the
f 1 = f 2 ) then G is diagnosable. fact that faults may be much more subtle, as for
instance: a deadlock (a blocking preventing any
3.2. Verifier techniqueYoo (2002)
further action of the system); a livelock (the blocking
3.3. Twin plant + “LTL” of certain functionalities in the system: technically
speaking, the system executes some tasks, but does
Several approaches use logical formulas to partially not meet its functional requirements); the repeated
state diagnosability. All these works have in common occurrence of a given event: taken individually, each
the fact that they first build an intermediary LTS, in occurrence is not a fault; but the recurrence of the
such a way to make the diagnosability decision a bit event denotes a faulty behavior; etc. For example,
easier. a nominal behavior could be the following: after a
request, the system must answer by a response (i.e
To the best of our knowledge, the authors of the system is reactive). To specify this requirement
Cimatti (2003) are the first who have used model- one can use the following formula: (request →
checking in order to decide diagnosability: first, the response). Any run which does not satisfy this
model describing the system behavior is composed property is considered as to be faulty.
with itself (by the means of the usual parallel
composition), giving a new structure called twin- In Jéron (2006), Jeron et al. reuse, while generalizing
plant. Two sets of states give the diagnosis them, the ideas discussed previously. The main idea
conditions: the states in the first set have not to be is to use the LTS model to specify both the behavior
confused with those in the second set. Then from to be diagnosed (i.e the “faulty” behavior), and the
the twin-plant, one may check whether there exists a model of the system to be monitored. The idea is
path reaching a critical state q, such that q = (x1 , x2 ) likely to be inspired from the well-known technique
and x1 (from the first component in the parallel called as ”verification with observers”: when it is not
product) satisfies a diagnosis condition, whereas x2 possible to express a given property using a logic (or
(from the second component in the parallel product) when using a logical formula leads to unsatisfying
satisfies another diagnosis condition. If such a performances), it remains possible to instrument the
critical state q is reached, then the original model is behavioral model in order to facilitate the expression
not diagnosable. of the property. This is exactly what is suggested
here: instead of giving a different logical formula
49
for each type of faults to be diagnosed, the system • J>K = true
model is composed with the fault model, then a
method, which is besides generic, is applied to check • J⊥K = false
diagnosability. In Jéron (2006), several fault patterns • J¬φK = not JφK
are given.
Concretely, given Gf the fault model and GM the • Jφ = γK = φ equals γ
model to be diagnosed, GΩ = Gf × GM is first
computed, then a determinization is operated on • Jφ ∧ γK = JφK and JγK
this LTS. Thereafter, on this determinized LTS, the • Jφ ∨ γK = JφK or JγK
unobservable events are abstracted thus obtaining
GΩobs
. Finally this obtained LTS is composed with • J(∃x)(φ)K =ORi∈O Jφ[i/x] K
itself: Gdiag = GΩ obs
× GΩ
obs
. The decision process is
thereby reduced to checking whether there is not a • JR(y1 , . . . , yn )K = (y1 , . . . , yn ) ∈ R
sequence indefinitely “undetermined”, i.e for which • Jλ(x1 , . . . , xn ).φK = {(y1 , . . . , yn ) ∈
one component in Gdiag is faulty whereas the other On | Jφ[y1 /x1 ,...,yn /xn ] K = true}
is not. The system is then diagnosable iff such a S∞
sequence does not exist. • Jµx.φK = i=0 S i , with S 0 = ∅ and S i+1 =
Jφ[S i /x] K
T∞
4. µ-CALCUL FORMULATION OF • Jνx.φK = i=0 S i , with S 0 = O and S i+1 =
DIAGNOSABILITY Jφ[S i /x] K
The goal of our formulation is twofold: to establish The terms true and false are the basis B of the
a homogeneous formal logical framework to specify boolean algebra whose operators are the usual
the diagnosability problem, and to give a “decision boolean operators and, or and not; equals: O×O →
algorithm”, directly deduced from the µ-calculus B allows the comparison of two elements in O; OR is
semantics. the disjunction on a set of boolean terms and finally
∈ is the usual membership operator.
The logic that we use here is typically a predicate
calculation extended with two fix-point operators In Jµx.φK and Jνx.φK, φ must be monotone, i.e. each
which have been proposed first in Park (1976). occurence of x must be “covered” by an even number
of negations.
µ-calcul syntax
E ::= The fix-point operator is an infinite union. However
> | ⊥ | ¬E | E ∧ E | E ∨ E | (∃X)(E) | E = E | R0 (x1 , . . . , xn ) and according to the Knaster-Tarski theorem Tarski
(1955), since O is a complete lattice, we know that
R0 ::= V | λX n .E | µV.R0 | νV.R0
this fix-point will be reached upon a finite number of
iterations.
R ::= λX n .E | µV.R0 | νV.R0
4.1. Diagnosability
where V is the set of relational variables and X is a
set of variables. Writing V or X is a shortcut to mean: Let hQ, q0 , Σ, −
→i, with −
→: Q × Σ × Q, the LTS
”any element of these sets”. Moreover, n ∈ N, n ≥ 1 modeling the system for which we want to check
and finally V ∩ X = ∅. diagnosability. We do not want to handle any item
other than states and events, thus O = Q ∪ Σ. We
There are two entry points for this grammar: E and also assume the existence of sets Σf of faulty events
R. Each of these entry points defines a particular and Σo of observable events.
type of formula: E denotes boolean formulas, while
R defines relations. A relation is defined by the set Firstly, we will introduce diagnosability in the same
of elements respecting a given boolean formula, way as defined in Sampath (1995). Thus, several
therefore, E-expressions are necessary to define a relations will be defined. In these relations faulty
relation. Note, however, that in the sequel E will not states are those which are reached after a fault
be used as an entry point in our formulation. event has occurred (starting from the initial state).
Secondly, we show how this definition can be easily
Semantics extended.
Throughout the rest of the paper, we write φ[y/x] to
say that every occurrence of x in φ is substituted Informally speaking, a triplet (a, b, f ) is element of
by y. The semantics of µ-calculus expressions is the UOReach relation, means that there exists an
defined on the complete lattice hO, ⊆i, as follows: unobservable path between a and b. This path is
labeled with a boolean f which is true when at least
50
UOReach = µX.λ(s, t, f ).(∃s0 )(∃f 0 )(∃e)(∃r)(∃e0
) • Initially, s corresponds to the states issued from
e
s−
→ t ∧ s = q0 ∧ ¬Σo (e) ∧ f = Σf (e) ∨ an observable transition from which an unobservable
e e0 transition is possible, f indicates whether the
s− → t ∧ r −→ s ∧ Σo (e0 ) ∧ ¬Σo (e) ∧ f = Σf (e) ∨
event labelling the unobservable transition is faulty
e
X(s, s0 , f 0 ) ∧ s0 −
→t ∧ or not. Formally, this case can be written as:
0
f = (f ∨ Σf (e)) ∧ ¬Σo (e) e0
(∃r)(∃e0 )(∃e)(r −→ s ∧ Σo (e0 ) ∧ s −
e
→ t ∧ ¬Σo (e) ∧ f =
Σf (e))
Figure 3: Unobservable reachability + identification of
faulty/normal paths
• By default, the initial state is considered as to be
e
issued from an observable transition: (s − → t∧s =
one of the events of this path is a fault; conversely q0 ∧ ¬Σo (e) ∧ f = Σf (e))
f is false if there exists an unobservable normal
• The third case is the recursion operation: there
(without fault) path between a and b. In order to
exists a path between s and t if there is a triplet
reduce the size of this relation, only the states
(s, s0 , f 0 ) in UOReach such that an unobservable
destination of an observable event, or the initial state,
transition links s0 to t. The parameter f of the new
are considered as an origin of the unobservable
triplet (s, t, f ) is true if f 0 is true (a fault has already
paths. A graphical representation of this relation
occurred between s and s0 ), or when the transition
applied to the model of Figure 4 is given in Figure e
s0 −→ t is faulty (i.e. Σf (e)): therefore we propagate
5.
the information that a fault is possible between s and
In Figures 5, 7, 10, 11, 12, 13, 15, 16, 17 and 19, T
s0 to the new triplet. Formally, this case is expressed
tag stands for TRUE (faulty path) and F for FALSE e
as follows: (∃s0 )(∃f 0 )(∃e)(U OReach(s, s0 , f 0 ) ∧ s0 − →
(no fault).
t ∧ ¬Σo (e) ∧ f = f 0 ∨ Σf (e))
a Nextobs = µX.λ(s, e, t, f ).(∃s”)(∃e 0 0 0
0 3 )(∃f )(∃s )
e
f Σ (e) ∧ s = q0 ∧ s −
o
→ t ∧ ¬f ∨
a e
u Σo (e) ∧ X(s”, e0 , s, f 0 ) ∧ ¬f ∧ s −→t ∨
u 2 a
e
Σo (e) ∧ U OReach(s, s0 , f ) ∧ s0 −
→t
a
u
1 4 Figure 6: Observable reachability + detection of
faulty/normal paths
u
a, T
a, F
Figure 4: The considered example a, T
0
F a, F a, F a ,F
3 a, F 3
T F 0
4
F
2 F a, F
F
a, F
F
1 F 4 2
Figure 5: Graphical representation of UOReach relation
Figure 7: Graphical representation of Nextobs relation
In the U OReach formula, the µX fix-point operator
indicates that the definition is recursive and that X The second step consists in determining the
denotes the set of elements in the relation at the observable reachability of the LTS for which we
previous step of the recursion. Since the samllest examine dianosability. The observable reachability is
fix-point operator (µ) is used here, X is initially an an LTS which keeps only the observable events, and
empty set (∅). The next operator, λ(s, t, f ), expresses in which a transition links a state s to a state t iff it is
that the relation UOReach is a ternary relation. The possible to reach t from s through an unobservable
relation is defined by giving the valuation space sequence (may be ) followed by an observable
that the three parameters, here (s, t, f ) can have. event. Here, the origin state s has to be either the
UOReach is defined by three cases: initial state q0 , or a state destination of an observable
event.
51
To each triplet (s, e, t) involved in an element of in terms of observation; the goal being to examine
the observable reachability relation, we assign a ambiguity in the system behavior starting from such
boolean f denoting the existence of a faulty path pairs of states, as will be shown in the Amb relation.
(a path containing a fault) when f is true, and a Two cases are considered:
normal path (without any fault) when f is false. The
graphical representation of Nextobs relation is given • the first case holds when from the same “normal”
in Figure 7. As for UOReach, Nextobs relation is state s, one can reach two different states t
defined according to two cases: and t0 respectively by two unobservable normal
sequences, both followed by the same observable
e
• Either s −→ t (with e observable) already exists, then event e (cf. Figure 10). This case can be written as:
we add (s, e, t, f ) as is to Nextobs while putting f N ormal(s)∧N extobs(s, e, t, ⊥)∧N extobs(s, e, t0 , ⊥)∧
marker to false (since this is a faultless path from s ¬(t = t0 ).
e
to t). Formally, this can be written: s −
→ t∧Σo (e)∧¬f .
As for U OReach, the origin state must be either the • the second case corresponds to the recursion
initial state (s = q0 ), or a state destination of an and consists in propagating the trace equivalence.
observable event (X(s”, e0 , s, f 0 )), which has been Concretely from two indistinguishable states s and
already captured in the N extobs relation, here. s0 already in Sameobs (X(s, s0 )), one can reach
two different states t and t0 while generating the
• Or there exists an intermediary state s0 such that same observable event e and without generating
e
→ t where e is observable and s0 is reachable
s0 − any fault for both paths (cf. Figure 11). This case
from s through a sequence of unobservable events can be expressed as: X(s, s0 ) ∧ N extobs(s, e, t, ⊥) ∧
((s, s0 , f 0 ) ∈ U OReach). In this case, the fault N extobs(s0 , e, t0 , ⊥) ∧ ¬(t = t0 ).
marker f is a copy of f 0 : indeed only unobservable
sequences containing a fault can turn f into true. e, F
Formally, this case can be expressed as follows: s t = t'
e
U OReach(s, s0 , f ) ∧ s0 −
→ t ∧ Σo (e).
Normal(s) t Sameobs(t,t')
e, F
Normal
= µX.λ(t).(∃s)(∃e) t'
t = q0 ∨
(X(s) ∧ N extobs(s, e, t, ⊥)) Figure 10: First case
e, F
Figure 8: Normal States t = t'
Sameobs(s,s') s e, F t Sameobs(t,t')
Normal is a unary relation (λ(t)) containing the initial
s' t'
state q0 as well as all the states, destination of an
observable transition and reachable from q0 by at Figure 11: Second case: propagation
least one normal path (cf. N extobs). This relation
will be useful in the sequel as if a given state t is Proposition. Sameobs(t, t0 ) =⇒ ∃σ1 , σ2 ∈
reachable only through faulty paths, then the faults (Σ \ Σf )∗ .Σo such that σ1 6= σ2 ∧ PΣo (σ1 ) = PΣo (σ2 )
will propagate and all the subsequent reached states σ1
∧ q0 −→
σ2
t ∧ q0 −→ t0
will be consequently faulty (no anymore ambiguity).
One may easily note that from the implementation Proof. From the definition of Sameobs given in Figure
point of view, sets N extobs and N ormal can be 9, (s, s0 ) is in Sameobs iff:
computed simultaneously using the same procedure,
just by looking at the fault tagin N extobs. • either t and t0 come from the same N ormal
state s, by Sameobs through a same observ-
Sameobs
= µX.λ(t, t0 ).(∃s)(∃s0 )(∃e) able event e, and without generating any fault
N ormal(s) ∧ N extobs(s, e, t, ⊥) ∧
∨ (cf. Figure 12),
N extobs(s, e, t0 , ⊥) ∧ ¬(t = t0 )
0
X(s, s ) ∧ N extobs(s, e, t, ⊥) ∧
Normal Normal e, F t = t'
0 0 0
N extobs(s , e, t , ⊥) ∧ ¬(t = t ) Normal
s t Sameobs(t,t')
q0 e, F
Figure 9: Trace equivalence - Same observability
t'
This relation catches all the couples (t, t0 ) such Figure 12: Building (t, t0 ) in the first case
that states t and t0 are different states that could
be reached respectively by two normal (faultless)
paths P1 and P2 having the same projection on Σo . • or t and t0 come respectively from s and s0
Sameobs allows us to keep all the states equivalent by Sameobs through a same observable event
52
e and without generating any fault such that faulty and not is the second. This can happen
(s, s0 ) is also in Sameobs (cf. Figure 13). according to three cases:
Sameobs Sameobs
en-1,F
Sameobs
e,F
t = t'
• pairs (t, t0 ) such that t and t0 can be reached from
Normal Normal Normal
s1 sn-1 s=sn
e,F
t Sameobs(t,t') the same normal state s, respectively through an
q0 s en-1,F
s1' sn-1' s'=sn' t'
unobservable faulty path followed by an observable
event e in one hand, and on the other hand through
Figure 13: Building (t, t0 ) in the second case a normal unobservable path (may be ) followed
by the same observable event e. This case can be
expressed as:
In the first case and given the definition of N extobs, N ormal(s) ∧ N extobs(s, e, t, >) ∧ N extobs(s, e, t0 , ⊥)
∃s ∈ N ormal, ∃σ10 , σ20 ∈ (Σu \ Σf )∗ .Σo such that (cf. Figure 15).
σ0 σ0
σ10 6= σ20 , PΣo (σ10 ) = PΣo (σ20 ) = e ∧ s −→
1
t ∧ s −→
2
t0 . • when from two states s and s0 such that
Besides, given the definition of N ormal, it is easy to Sameobs(s, s0 ), one can reach t and t0 respectively
show (by induction) that ∃σ 0 ∈ (Σ \ Σf )∗ .Σo such that through two unobservable sequences, σ1 faulty and
σ0 σ0 σ0
q0 −→ s. Then we have q0 −→ s, s −→
1
t, σ10 6= σ20 σ2 normal, both followed by the same observable
σ0 event e (Sameobs(s, s0 ) ∧ N extobs(s, e, t, >) ∧
s −→
2
t0 . Hence, with σ1 = σ 0 .σ10 and σ2 = σ 0 .σ20 , we N extobs(s0 , e, t0 , ⊥)) as shown in Figure 16. This can
have σ1 , σ2 ∈ (Σ \ Σf )∗ .Σo ∧ σ1 6= σ2 ∧ PΣo (σ1 ) = be written:
σ1 σ2
PΣo (σ2 ) ∧ q0 −→ t ∧ q0 −→ t0 . Sameobs(s, s0 ) ∧ N extobs(s, e, t, >) ∧
N extobs(s0 , e, t0 , ⊥).
In the second case, let us take back the computation
of Sameobs as given in definition 9. Assume there • the third case is when the ambiguity is obtained
are n couples (si , s0i ) in Sameobs, i ∈ [1, n] preceding by “inheritence” from two ambiguous states s and
(t, t0 ) after having bifurcated from the same normal s0 repectively by a faulty unobservable sequence
state s, as shown in Figure 13. Then, according to (which may be either normal or faulty, and possibly
N extobs definition, ∃σn , σn0 ∈ (Σu \ Σf )∗ .Σo such empty) followed by an observable event e; and on
σn
that PΣo (σn ) = PΣo (σn0 ) = e ∧ (sn = s) −−→ t∧ the other hand by a normal unobservable sequence
(s0n = s0 ) −−→
n σ0
t0 . This is also true for each pair of followed by the same observable event e (X(s, s0 ) ∧
couples (si , s0i ), (si+1 , s0i+1 ) for i ∈ [1, n − 1]. That N extobs(s, e, t, f )∧N extobs(s0 , e, t0 , ⊥)). This case is
is ∀i ∈ [1,n-1], ∃σi , σi0 ∈ (Σ \ Σf )∗ .Σo such that depicted in Figure 17.
σ σ0
PΣo (σi ) = PΣo (σi0 ) ∧ si −→i
si+1 ∧ s0i −→ i
s0i+1 . e, T t
Then by concatenating respectively σi sequences
s
Normal(s) Amb(t,t')
and σi0 sequences, one can state that: ∃ρ1 , ρ2 ∈ e, F
(Σ \ Σf )∗ .Σo , ρ1 = σ1 . . . σn , ρ2 = σ10 . . . σn0 such that t'
ρ1 ρ2
PΣo (ρ1 ) = PΣo (ρ2 ) ∧ s1 −→ t ∧ s01 −→ t0 .
0 Figure 15: Primitive ambiguity
Moreover (s1 , s1 ) falls in the first case, then ∃τ1 , τ2 ∈
(Σ \ Σf )∗ , τ1 6= τ2 such that q0 −→
τ1 τ2
s1 ∧ q0 −→ s e, T t
τ1 τ2
s01 ∧ PΣo (τ1 ) = PΣo (τ2 ) ∧ q0 −→ s1 ∧ q0 −→ s01 . Sameobs(s,s') e, F Amb(t,t')
Finally, by taking σ1 = τ1 .ρ1 and σ2 = τ2 .ρ2 , we
obtain: σ1 , σ2 ∈ (Σ \ Σf )∗ .Σo , σ1 6= σ2 , PΣo (σ1 ) = s' t'
σ1 σ2
PΣo (σ2 ) ∧ q0 −→ t ∧ q0 −→ t0 .
Figure 16: Ambiguity from Sameobs states
Amb 0 0 s e, T or F t
= µX.λ(t, t ).(∃s)(∃s )(∃e)(∃f )
N ormal(s) ∧ N extobs(s, e, t, >) ∧ Amb(s,s') Amb(t,t')
0 ∨ e, F
N extobs(s, e,0t , ⊥)
Sameobs(s, s ) ∧ N extobs(s, e, t, >) ∧ s'
∨ t'
0 0
, e, t , ⊥)
N extobs(s
0
X(s, s ) ∧ N extobs(s, e, t, f ) ∧ Figure 17: Ambiguity by inheritance
0 0
N extobs(s , e, t , ⊥)
In order to examine diagnosability, one has to check
Figure 14: Local Ambiguity
whether there exists a cycle of ambiguous states.
Searching such a cycle is not simple if we use the
Amb relation is quite simple and consists in smallest fix-point operator µ. One possible way is to
identifying pairs of states t and t0 locally ambiguous, add, one by one, the elements that we are sure they
i.e t and t0 can be reached from q0 by two sequences do not make part of a cycle: if the obtained relation
generating the same observation, but the first is
53
(that we call Noteveramb) is equal to Amb, then a, T
there is no such a cycle. Conversely, the elements 0
of Amb which are not in Noteveramb form at least a, F
one ambiguous cycle.
a, F
However, the µ-calculus offers another operator a, T 2
which will be very useful here: the greatest fix-point a, F
operator ν. Thanks to this operator, we will start
from the maximal relation Q × Q, then at each step
we keep only the elements satisfying the equation a, F
until a fix-point is reached. Hence, defining Everamb
becomes simpler because only one case is possible
4
(cf. Figure 18): a couple (s, s0 ) is in Everamb iff s and
a, F
s0 are ambiguous (Amb(s, s0 )) and iff there is at least Figure 19: Cyclic ambiguity
one successor couple (t, t0 ) by N extobs which fulfills
both of the following conditions:
On one hand, Go of Huang (2004) is quite similar
• is also ambiguous: (N extobs(s, e, t, >) ∧ to N extobs. The major difference being that N extobs
N extobs(s0 , e, t0 , ⊥)), and holds fault information on transitions, while Go holds
• is in Everamb as well (recursivity): (X(t, t0 )) them in states. This mostly impacts the number of
states which would be more important in Go , while
Such a recursive definition implies that either of the N extobs may have more transitions.
following two cases holds: On the other hand, the computation of Sameobs
together with Amb is equivalent to the composition
1. the number of ambiguous couples in Everamb procedure Gd = (Go ||Go ). Actually, Sameobs
is infinite, or performs the composition between the normal paths
which have an observational equivalence (both
2. the ambiguous couples in Everamb form a generate the same observation), whereas Amb
cycle. performs the composition between a faulty path on
one hand and a normal path on the other hand, when
Hence, since we deal with a finite state system,
both paths have an observational equivalence.
only the second case is possible. Thereby, each
ambiguous couple (s, s0 ) in Everamb belongs to at Also, the definition of Everamb does not allow
least one cycle of ambiguous couples. multiple faults directly, but this does not break its
generality: if there is more than one type of faults,
Everamb = νX.λ(s, s0 ).(∃t)(∃t0 )(∃e)(∃f
) i.e. if the partition Πf contains more than one set, it
Amb(s, s0 ) ∧ N extobs(s, e, t, >) ∧
is sufficient to check the emptiness of Everamb for
N extobs(s0 , e, t0 , ⊥) ∧ X(t, t0 )
each of the sets individually, as stated in definition 8.
Figure 18: Cyclic ambiguity
In Gd , a couple (x, y) is ambiguous iff, for a given
fault f , x = (q, F ) and f ∈ F , while y = (q 0 , F 0 )
Figure 19 gives the Everamb relation for the
and f 6∈ F 0 . As (x, y) is in Gd , this means that q and
considered model. Everamb is equal to Amb here,
q 0 are reachable by the same observable sequence.
but for which we have shown in dotted line, some
This corresponds to our definition of ambiguity. The
cycles in N extobs that satisfy Amb.
couple of states (t, t0 ) is ambiguous if either of the
following conditions holds:
Definition 8 An LTS is diagnosable according to a
partition of faults Πf iff for each part Σf in Πf , • there exists a state s belonging to N ormal, i.e
Everamb is empty. there exists a normal sequence σ ∈ ((Σuo \ Σf )∗ Σo )∗
σ
such that q0 − → s, and there exists an observable
Theorem 1 The previous definition of diagnosability event e and two unobservable sequences σ 0 faulty
and those of Sampath (1995) and Huang (2004) are σ 0 .e σ 00 .e
equivalent. and σ 00 normal, such that s −−→ t and s −−−→ t0 .
This means we cannot decide, by only observing
Proof. PΣo (σ).e, whether a fault has occurred or not, hence
It is proved in Huang (2004) that an LTS is the ambiguity.
diagnosable in the sense of Sampath (1995) iff
• there exists a couple (s, s0 ) of states in Sameobs, i.e
the twin plant Gd = (Go ||Go ) does not have any
there exist two normal sequences having the same
ambiguous cycle.
54
projection on Σo , σ1 , σ2 ∈ ((Σuo \ Σf )∗ Σo )∗ such that yields a polynomial complexity (if it is not, finding an
σ1 σ2
q0 −→ s and q0 −→ s0 , and (s, s0 ) fulfills the following: efficient algorithm would have no sense!).
from s there can be an observable step (in N extObs)
s−
e
→ t generating a fault and from s0 there can be an To estimate the complexity of the whole diagnosabil-
observable step (in N extObs) s0 −
e
→ t0 with no fault. ity decision process, we will seek for an upper bound
Like previously, this means one cannot decide by on the complexity of each of the various formulas
only observing PΣo (σ).e whether a fault has occurred given in definitions 8 to 13.
or not, thus the ambiguity.
Let us recall that these formulas are all based on
0
• there exists a couple of states (s, s ) in Amb, which fixed point operators. Because of their recursive
means there exists a faulty sequence σ1 ∈ (Σuo ∗ nature and because the computation stops as soon
Σo )∗ such that q0 −→
σ1
s and a normal sequence as a new iteration does not change the result (the
∗ ∗ σ1 fixed point is reached), it is difficult to determine the
σ2 ∈ ((Σuo \ Σf ) Σo ) such that q0 −→ s0 while σ1
worst case in a general way. Indeed, it is possible
and σ2 have the same observable projection, and
to find a worst case for a given (part of) formula,
(s, s0 ) fulfills the following: there exist an observable
but it may very well be that this very worst case is
event e, two unobservable sequences σ either faulty
at the same time the best case of another one (or
or not (∈ Σ∗uo ), and σ 0 normal (∈ (Σuo \ Σf )∗ ) such
σ.e σ 0 .e
at least, not its worst case), and the worst case of
that s −−→ t and s0 −−→ t0 . Thereby, t can be both formulas, when combined, generally cannot be
reached from q0 through a faulty path σ1 σe, and the combination of the worst cases of each of the
t0 can be reached from q0 through a normal path formulas.
σ2 σ 0 e and both paths generate the same observation
(PΣo (σ1 σe) = PΣo (σ2 σ 0 e)). Like previously, this Here we will take the worst case for each of the
means we cannot decide based on the observed formulas for one single iteration and then, we will
events if a fault has actually occurred, hence the consider the maximum number of iterations leading
ambiguity. to the fix point. This way, we are sure to get an
upper bound of the complexity. Note that the result
For every sequence of events, once a state is faulty, we will get is necessarily an overestimate of the
every successor is faulty as well. If a cycle is found in real complexity. To picture that, let us consider the
Gd such that it contains at least one composite state calculation of U OReach (Definition 3). With the µ
of a “faulty” and a “normal” states (i.e. ambiguity), operator one starts with an empty set, and at the
then every state in that cycle is ambiguous too. first iteration the triples (s, t, f ) verifying the following
This is why instead of finding cycles containing at conditions are added:
least one ambiguous state as in Huang (2004), it
is equivalent to say that each element of a cycle • s is either the initial state, or the target
in Everamb must be ambiguous. As shown when state of an observable transition; to check
relation Everamb has been introduced earlier, each both conditions we must go through the
element in this set belongs to at least in one cycle of whole transition relation (which has a -highly
ambiguous pairs. improbable- maximum of |Q|.|Σ|.|Q| elements)
and check for each triple (s, e, t) whether
e is observable (|Σo | ≤ |Σ|). At the end,
5. COMPLEXITY these operations have the following complexity:
|Q|2 .|Σ|2 .
We want to insist on the fact that the purpose
of this article is not to propose a new algorithm. • for all the states s found in the previous item
Indeed, even if the semantics is operational and (at most |Q| states), (s, t, f ) is in U OReach
allows computation, a direct implementation of that at the first iteration if there exists (s, e, t)
semantics would be far from being optimized. in the transition relation, such that e is not
Nevertheless, we want to argue here that our observable (e ∈ Σu ). Like previously, we will
formulation may be a good source for some new consider Σ instead of Σu (|Σu | ≤ |Σ|), to
efficient algorithms. Indeed, where the other works ease factorization. We obtain the following
systematically operate a product of the system to be complexity: |Q|3 .|Σ|2 .
diagnosed with itself (or a non-faulty version of itself),
such a product is performed here according to some • f can be either true or false: the complexity of
finer conditions. But before exploring what such an the previous item is then multiplied by 2.
algorithm would look like, we wanted to explore the
complexity of our approach, to see whether it is of the This results in the following upper bound of the
same complexity order, i.e. whether our formulation overall complexity: |Q|2 .|Σ|2 + 2|Q|3 |Σ|2 for the first
iteration.
55
For the subsequent iterations, we start with the being studied.
existing set of triples (s, s0 , f ) (at most 2|Q|2 triples),
and for all the (target) states s0 of these triples,
we determine the states t directly accessible by an The approach was tested with the MEC/ARC tools,
unobservable transition e (complexity 2|Q|2 |Σ|2 ). So but a prototype was also implemented to tackle the
this gives the following upper bound of complexity: issue from the point of view of explicit exploration
2|Q|4 |Σ|2 . of the behavior (which is not allowed by MEC),
but also to have a better understanding of the
Regarding the number of iterations before reaching formulation complexity, and to explore optimization
the fixed point, the worst case corresponds to the possibilities. As a side note, the prototype was
situation in which at each iteration, a single new relatively easily implemented (using Standard ML),
triplet is added to U OReach: this means there are and we think that this is in large part because of
at most |Q|2 |Σ| iterations. the simplicity of the µ-calculus semantics. Besides
this direct implementation, we have also developed a
We then obtain that an upper bound on the second prototype based on a database management
complexity of the U OReach computation is |Q|6 .|Σ|3 . framework Ghazel (2012).
It is obvious that this bound is far from being optimal,
but it allows us to determine the complexity class of
our formulation. In the same way, we find that each of REFERENCES
the formulas, has a polynomial complexity. Thus, we
can say that analyzing the diagnosability on the basis A. Arnold, G. Point, A. Griffault and A. Rauzy (1999),
of our formulation is of a polynomial computational The altarica formalism for describing concurrent
complexity. systems, Fundam. Inf., 40(2-3):109-124.
F. Basile, P. Chiacchio and G. De Tommasi (2010),
6. CONCLUSION Petri nets via integer linear programming, Discrete
Event Dynamic Systems, 10(1):71-77.
This work offers a new way to formulate
M.P. Cabasino, A. Giua and C. Seatzu (2010), Fault
diagnosability of DES using µ-calculus logic
detection for discrete event systems using petri
that we advocate to be a good formalism for a
nets with unobservable transitions. Automatica,
single formal framework to deal with diagnosability.
46(9):1531-1539.
While it theoretically defines the logical perimeter
of the problem, it also allows the use of model C.G. Cassandras and S. Lafortune (2008), Introduc-
checking techniques. This means taking advantage tion to discrete event systems. Elsevier.
of already efficient tools and of mature techniques
to circumvent, the best it can, the problem of A. Cimatti, C. Pecheur and R. Cavada (2003), Formal
combinatorial explosion, which is a well-known verification of diagnosability via symbolic model
problem in model-checking, also called the state checking, In IJCAI’03, pages 363369.
space explosion problem. The developed formulation
M. Cabasino F. Basile and C. Seatzu (2013), Marking
is quite flexible and some extensions are being
estimation of time petri nets with unobservable
developed in order to tackle diagnosability issues
transitions, In 18th IEEE Int. Conf. on Emerging
under different contexts. Moreover, based on our
Technologies and Factory Automation.
logical formulation, we intend to develop diagnosers
for online monitoring. S. Genc and S. Lafortune (2007), Distributed diag-
nosis of place-bordered petri nets, IEEE Trans-
actions on Automation Science and Engineering,
From a technical point of view, developing an 4(2):206-219.
on-the-fly algorithm to implement our formulation
shall improve the efficiency of the computational M. Ghazel, A. Toguyéni and P. Yim (2009), State
complexity of the diagnosability analysis procedure observer for des under partial observation with
Liu (2014). This issue will be investigated in our time petri nets, Discrete Event Dynamic Systems,
future works. 19(2):137-165.
In addition, we believe that the flexibility of µ-
calculus can be efficiently used for some other M. Ghazel, F. Peres, A. Belhaj Alaya and A. Jemai
problems gravitating around diagnosability, as for (2012), A DBMS Framework for Diagnosability
fault specification of Jiang (2004), except that Analysis of Discrete Event Systems, The 42nd
µ-calculus would be used instead of LTL. Its An- nual IEEE/IFIP International Conference on
expressiveness, and the facilities it introduces are Dependable Systems and Networks (DSN’2012),
Boston, USA.
56
A. Grastien (2009), Symbolic testing of diagnos- T. Ushio, I. Onishi and K. Okuda (1998), Fault
ability, International Workshop on Principles of detection based on petri net models with
Diagnosis, pages 131-138. faulty behaviors, in Proceedings of the IEEE
International Conference on Systems, Man and
A. Griffault and A. Vincent (2004), The Mec 5 model-
Cybernetics, pages 113-118.
checker, in Rajeev Alur and Doron A. Peled,
editors, Computer Aided Verification, volume 3114 A. Vincent (2003), Conception et réalisation d’un
of LNCS, pages 248-251. vérificateur de modles AltaRica - PhD thesis,
Université des Sciences et Technologies -
Z Huang, S Bhattacharyya, V Chandra, S Jiang
Bordeaux I.
and R. Kumar (2004), Diagno- sis of discrete
event systems in rules-based model using first- T.S. Yoo and S. Lafortune (2002), Polynomial-time
order linear temporal logic, in Proceedings of the verification of diagnosability of partially observed
American Control Conference. discrete-event systems. IEEE Transactions on
T. Jéron, H. Marchand, S. Pinchinat and M-O. Automatic Control, 47(9):1491-1495.
Cordier (2006), Supervision patterns in discrete J. Zaytoon and S. Lafortune (2013), Overview of fault
event systems diagnosis, in 8th Workshop on diagnosis methods for discrete event systems.
Discrete Event Systems, WODES’06. Annual Reviews in Control, 37(2):308-320.
S. Jiang, Z. Huang, V. Chandra and R. Kumar (2001),
A polynomial algorithm for testing diagnosability of
discrete event systems, IEEE TAC, 46(8): 1318-
1321.
S. Jiang and R. Kumar (2004), Failure diagnosis of
discrete event systems with linear-time temporal
logic fault specifications. IEEE TAC, 49:6:934-945.
G. Jiroveanu and R. Boel (2006), A distributed
approach for fault detection and diagnosis based
on time petri nets, Mathematics and Computers in
Simulation, 70(5-6):287-313.
F. Lin (1994), Diagnosability of disrete event systems
and its applications. JDEDS, 4:197-212.
B. Liu, M. Ghazel and A. Toguyéni (2014), Toward
an efficient approach for diagnosability analysis
of des modeled by labeled petri nets, in The
13th European Control Conference (ECC14),
Strasbourg, France.
D. Park (1976), Finiteness is mu-ineffable. TCS,
3(2):173-181.
F. Peres, B. Berthomieu and F. Vernadat (2011), On
the composition of time petri nets, Discrete Event
Dynamic Systems, 21(3):395-424.
M. Sampath, R. Sengupta, S. Lafortune, K. Sin-
namohideen and D. Teneketzis (1995), Diagnos-
ability of discrete-event systems. 40:1555-1575.
A. Tarski (1955), A lattice-theoretical fixpoint
theorem and its applications, pa- cific journal
of mathematics, Pacific Journal of Mathematics,
5(2):285- 309.
S. Tripakis (2002), Fault diagnosis for timed
automata, in FTRTFT’02: Proceedings of the 7th
International Symposium on Formal Techniques in
Real-Time and Fault-Tolerant Systems, Springer-
Verlag, pages 205-224, London, UK.