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.