OF-PENDA: A Software Tool for Fault Diagnosis of Discrete Event Systems Modeled by Labeled Petri Nets Baisi Liu1,2,3 , Mohamed Ghazel1,2 , and Armand Toguyéni1,3 1 Univ. Lille Nord de France, F-59000, Lille, France 2 IFSTTAR, Cosys/Estas, F-59666, Villeneuve d’Ascq, France 3 École Centrale de Lille, LAGIS, F-59651, Villeneuve d’Ascq, France {baisi.liu, mohamed.ghazel}@ifsttar.fr, armand.toguyeni@ec-lille.fr Abstract. In this paper, a software tool to deal with diagnosis of dis- crete event systems (DESs) is presented. This tool called On-the-Fly PEtri-Net-based Diagnosability Analyzer (OF-PENDA) implements the techniques developed in [13] for the diagnosis of DESs modeled by la- beled Petri nets (LPNs). This technique aims to cope with the state explosion problem which is a major issue when dealing with diagnosis of DESs. In particular, OF-PENDA implements an incremental and on- the-fly algorithm which makes it possible to analyze (K-)diagnosability without necessarily generating the whole state space of the model. Three aspects for OF-PENDA are discussed in this paper: an overview on the implemented technique is given; some features of the tool are discussed; then two illustrative case studies are processed to show the efficiency in terms of time and memory compared with some existing approaches. Keywords: fault diagnosis, discrete event system, labeled Petri net, on- the-fly analysis, incremental search, C++. 1 Introduction Diagnosability analysis and online diagnosis are two crucial issues in safety crit- ical systems. Most of such systems can be modeled as DESs [5] in a sufficiently high abstraction level. For technical and/or economical reasons, it is generally inconceivable to sense all the behavioral variations in a complex dynamic system. Thereby, very often, monitoring activities in such systems have to be carried out under partial observability. In particular, DES diagnosis is often explained as the task which consists in deducing and identifying the occurrence of faulty unob- servable events, based on the occurrence of observable events; and diagnosability is the ability to diagnose any fault in a finite delay after its occurrence. In the past two decades, diagnosability analysis has been studied using tech- niques such as diagnoser automata [15], verifier automata [7, 17], integer linear programming [1] and verifier Petri nets [3]. Software tools, such as the UMDES library [9] can analyze diagnosability. A major issue that these works have to 2 B. Liu, M. Ghazel and A. Toguyéni deal with is the computation complexity. In particular, the state explosion phe- nomenon constitutes a major obstacle especially for the approaches based on building and/or investigation of the state space. In [11], we have developed a new technique which aims to cope (even partially) with this problem, by adapt- ing an incremental and on-the-fly building of the state space in parallel with (K-)diagnosability analysis. OF-PENDA is a software tool developed in C++ for the diagnosability anal- ysis and the online diagnoser generation for DESs modeled by LPNs. It is the implementation of various algorithms developed in [11]. Diagnosability verdict is emitted and when the system is diagnosable, an online diagnoser is generated in a straightforward way. In addition, for diagnosable systems, Kmin , the mini- mum number of steps (observable events) after the occurrence of fault to ensure diagnosability, is also given to help describe diagnosability in a finer way. The reminder of this paper is organized as follows. Section 2 briefly introduces some notations pertaining to LPN and (K)-diagnosability. Section 3 discusses the on-the-fly and incremental techniques implementated in OF-PENDA. In Sec- tion 4, we present the features of OF-PENDA. Then, two cases WODES and level crossing (LC) benchmarks are used to show the efficiency of OF-PENDA in Section 5 and 6, respectively. Finally, some concluding remarks are given in Section 7. 2 Preliminaries 2.1 Labeled Petri Nets A Petri net (PN) is a tuple N = (P, T, P re, P ost), where P is a finite set of places; T is a finite set of transitions; P re and P ost are the pre- and post- incidence mappings. C = P ost − P re is the incidence matrix. A marking is a vector M ∈ N |P | that assigns a non-negative integer to each place. A marked PN (N, M0 ) is a PN N with given initial marking M0 . For short, a marked PN will be called PN afterward. A transition ti is enabled at marking M if M ≥ P re(·, ti ), denoted by M [ ti >. A PN (N, M0 ) is bounded if the number of tokens in each place does not exceed a finite number m ∈ N for any marking reachable from M0 . A PN is live if, no matter what marking has been reached from M0 , it is possible to ultimately fire any transition of the net by progressing through some further firing sequence. An LPN is a tuple NL = (N, M0 , Σ, ϕ), where (N, M0 ) is a marked PN; Σ is a finite set of events and ϕ : T → Σ is the transition labeling function. ϕ is also extended to sequences of transitions, ϕ : T ∗ → Σ ∗ . The language generated by NL is L(NL ) = {ϕ(σ) ∈ Σ ∗ | σ ∈ T ∗ , M0 [ σ >}. For short, we write L instead of L(NL ). We denote by s = s1 s2 . . . sn the concatenation of s1 , s2 , . . . , sn , where s1 , s2 , . . . , sn ∈ Σ ∗ . Lecture Notes in Computer Science: Authors’ Instructions 3 2.2 K-diagnosability In event-based diagnosis of DESs, event set Σ is partitioned into two disjoint sets, Σ = Σo ] Σu , where Σo is a finite set of observable events and Σu is a finite set of unobservable events. Fault events are unobservable, thus the set of fault events Σf ⊆ Σu . Likewise, the set of transitions T is partitioned into sets of observable and unobservable transitions: T = To ] Tu . Moreover, the faulty transitions are unobservable (T Ufm ⊆ Tu ). Also, the set of fault events can be partitioned into m sets, Σf = i=1 ΣFi , where ΣFi denotes one class of faults. Let Po : Σ ∗ → Σo∗ be the projection which “erases” the unobservable events in a sequence s ∈ Σ ∗ . The inverse projection operator Po−1 is defined as Po−1 (r) = {s ∈ L | Po (s) = r} for r ∈ Σo∗ . Given a live and prefix-closed language L ⊆ Σ ∗ and a string s ∈ L, the post-language of L after s denoted by L/s is L/s = {s0 ∈ Σ ∗ | ss0 ∈ L}. We denote the length of string s by |s|, and the ith event of sequence s by si . For a ∈ Σ and s ∈ Σ ∗ , we write a ∈ s if i exists such that si = a. Definition 1. Given an LPN NL and K ∈ N , e ∈ Σf is K-diagnosable if ∀u ∈ L, u|u| ∈ Σf and ∀v ∈ L/u such that |Po (v)| ≥ K, then r ∈ Po−1 (Po (uv)) ⇒ e ∈ r For a K-diagnosable system S, it is obvious that S is K 0 -diagnosable for any 0 K ≥ K. Besides, Kmin exists such that S is Kmin -diagnosable, and S is not K 0 -diagnosable for all K 0 < Kmin . 3 Techniques Applied in OF-PENDA 3.1 On-the-fly Analysis For most existing approaches, diagnosability analysis is composed of two stages. First, advanced models are developed for extracting the necessary information for diagnosability analysis from the original model, e.g., diagnoser automata [15], verifier automata [17], verifier Petri nets [3], and linear inequalities [1]. Secondly, diagnosability analysis is tackled based on the structure analysis of the plant (or by solving mathematical models), e.g., through checking the existence of certain specific states or cycles, and verifying the existence of linear inequalities solu- tions. Traditionally, the two stages are proceeded independently and sequentially. The analysis of advanced models is performed after their state spaces have been completely generated. This presents the state explosion problem when dealing with large systems. In OF-PENDA, we tackle this problem by using on-the-fly techniques [16], since such techniques have the following advantages: On-the-fly techniques can save memory resources. Generally, on-the-fly tech- niques permit us to generate and investigate only a part of the state space to find solutions, unlike the classic enumerative approaches which have to build the whole state space a priori. On-the-fly exploration techniques do not reduce 4 B. Liu, M. Ghazel and A. Toguyéni the complexity of the original algorithms, but they do save memory resources in general, depending on the system structure and on the searching strategy. On-the-fly techniques can save computing time. On the one hand, on-the- fly exploration terminates as soon as some specific features are found, which requires less time than investigating the whole state space. On the other hand, for two-stage analysis, such as our approaches that will be given in this paper, the advanced models can be derived and analyzed step by step as the on-the-fly building of the basic models, rather than being analyzed after building the whole basic models, which can save time from both analysis stages. On-the-fly techniques can deal with some unbounded systems, since they re- turn a verdict as soon as some specific features are found, instead of investigating the whole infinite state space, as will be shown in Section 5. 3.2 Incremental Search Technique The incremental method [8] is a search technique that reuses the information from previous searches when some parameters change. Generally, it is faster than performing the search for each changed parameter from scratch. The analysis of the k th step is based on the search result of the (k − 1)th step. Different from other speeding up searches, it can guarantee finding the shortest paths. As in [13], the classic diagnosability can be analyzed based on incrementally investigating K-diagnosability with increasing the value of K, and the Kmin value which ensures the diagnosability will be eventually found (for diagnosable systems). Note that some approaches based on integer programming [1] have to rebuild and solve the equation system (or inequalities) when seeking out Kmin , without using the previous search results. The incremental technique is a skillful technique to speed up the search pro- cedure. It should be used for bounded systems so that the search can terminate well. In particular, it can be used for unbounded systems when some conditions for terminating the search exist. Incremental techniques can be used with on-the-fly analysis to perform an efficient analysis. Both techniques do not change the computation complexity. However, they improve the searching efficiency when dealing with real systems. 4 Features of OF-PENDA In [13], we deal with diagnosability of LPN models using on-the-fly and incremental techniques. Classic diagnosability is transformed into a series of K-diagnosability, where K increases progressively. Unlike several existing approaches [7,15,17], we do not enumerate the state space. Instead, the state space is often partially gen- erated as necessary, and the investigation is stopped as soon as some special criteria are met. This can potentially offer efficiency in terms of time and mem- ory, compared with the aforementioned approaches. OF-PENDA is the implementation of various algorithms elaborated in [13] for the diagnosis of DESs modeled by LPNs. It is a command-line software tool developed in C++. Lecture Notes in Computer Science: Authors’ Instructions 5 OF-PENDA takes the mathematical model of an LPN as input, i.e., the matrices P re, P ost, M0 , the event-mapping matrix [13] and the fault partitions. While analyzing (K-)diagnosability, the generated model for the K th step are used for (K + 1)th step. If the system is diagnosable, the minimum value Kmin ensuring K-diagnosability is given, and the on-line diagnoser is generated. In order to show the efficiency of on-the-fly and incremental techniques in diagnosability analysis, the WODES benchmark [6] and the LC diagnosis bench- mark are used in the comparative simulation using OF-PENDA and the UMDES library [9], with the help of TINA tool [2], as will be presented in Section 5 and 6. Based on the simulation results, we will point out the similarities and differences between our approach and some existing diagnosis approaches. 5 Application to the WODES Diagnosis Benchmark 5.1 WODES Benchmark The WODES diagnosis benchmark [6] is shown in Figure 1 and describes a manufacturing system characterized by three parameters: n, m and k, where: – n is the number of production lines; – m is the number of units of the final product that can be simultaneously produced. Each unit of product is composed of n parts; – k is the number of operations that each part must undergo in each line. The observable transitions are indicated by white boxes, and the unobservable transitions by black boxes. 5.2 Comparative Results We now analyze the diagnosability upon the fault class ΣF 1 = {f1 , . . . , fn−1 }. In other terms, only one class of faults is considered here. In order to per- form a comparative simulation with OF-PENDA and the UMDES library, some preparations are necessary. The UMDES library deals with automata models by importing a .fsm file. Thus, we first generate the reachability graph of the consid- ered PN with the help of TINA yielding to a .aut file, which is then transformed into a .fsm file by a script integrated in OF-PENDA that we have developed. This ensures that the comparative simulation is performed with the same input. The simulation has been performed on a PC Intel with a clock of 2.26 GHz and the results are shown in Table 1. – The first 3 columns entitled “m”, “n” and “k” are the basic structural pa- rameters of the WODES diagnosis benchmark. – The 4th column entitled “|R|” is the number of nodes in the marking graph computed by TINA, which is equal to the number of states of the automaton for building the diagnoser by the UMDES library. – The 5th column entitled “|N |” is the number of the FM-graph nodes. 6 B. Liu, M. Ghazel and A. Toguyéni Fig. 1. The WODES diagnosis benchmark – The 6th column entitled “|Diag|” is the number of the diagnoser automaton states generated by UMDES. – The 7th column entitled “|Xv |” is the number of the fault marking set tree (FM-set tree) nodes. – The 8th (resp. 9th ) column entitled “DD ” (resp. DO ) is the diagnosability verdict returned by UMDES (resp. OF-PENDA), where “Yes” indicates that the system is diagnosable and “No” indicates undiagnosable. – The 10th column is the stopping value of K in the incremental search. Note that for a diagnosable case (cf. Column 9), this “K ” value is equal to “Kmin ”. All the results are obtained under a simulation time of less than 6 hours. “o.t.” (out of time) means the result cannot be computed within 6 hours. 5.3 Discussions A Finer Version of Diagnosability Both the OF-PENDA and the UMDES library allow us to check diagnosability for bounded DESs. In particular, thanks to our incremental investigation of diagnosability, our tool also gives Kmin for diagnosable systems, while the UMDES library [9] does not. It is worth recalling that the K-diagnosability is a finer version of diagnosability with the following two main features: Online, the value of Kmin gives us a valuable piece of information indicat- ing the minimum number of steps necessary to detect and identify faults for a Lecture Notes in Computer Science: Authors’ Instructions 7 Table 1. Comparative results obtained by UMDES and OF-PENDA m n k |R| |N | |Diag| |Xv | DD DO K m n k |R| |N | |Diag| |Xv | DD DO K 1 2 1 15 8 4 3 Yes Yes 2 1 5 1 3,295 2,607 o.t. 66 o.t. Yes 5 1 2 2 24 10 4 3 Yes Yes 2 1 5 2 9,691 o.t. o.t. o.t. o.t. o.t. o.t. 1 2 3 35 12 4 3 Yes Yes 2 2 2 1 96 68 20 9 No No 8 1 2 4 48 14 4 3 Yes Yes 2 2 2 2 237 137 o.t. 9 o.t. No 8 1 3 1 80 52 10 6 Yes Yes 3 2 3 1 1,484 801 20 12 No No 11 1 3 2 159 90 10 6 Yes Yes 3 2 3 2 5,949 2,746 o.t. 12 o.t. No 11 1 3 3 274 138 10 6 Yes Yes 3 2 4 1 28,203 8,795 o.t. 15 o.t. No 14 1 3 4 431 196 10 6 Yes Yes 3 2 4 2 180,918 o.t. o.t. o.t. o.t. o.t. o.t. 1 4 1 495 367 29 17 Yes Yes 4 3 2 1 377 290 66 12 No No 11 1 4 2 1,200 822 29 17 Yes Yes 4 3 3 1 12,048 5,165 o.t. 16 o.t. No 15 1 4 3 2,415 1,533 o.t. 17 o.t. Yes 4 3 4 1 484,841 o.t. o.t. o.t. o.t. o.t. o.t. 1 4 4 4,320 2,554 o.t. 17 o.t. Yes 4 diagnosable system. Note that in [1], K is the number of both observable and unobservable transitions after a faulty transition. While here, as well as in [3] K is the value relative to only observable events. Modifying our algorithm to compute both observable and unobservable transitions can be done easily. Secondly, K-diagnosability allows a meticulous description of the diagnosabil- ity for multiple faults. It is advisable to discuss the traditional diagnosability as a series of K-diagnosability problems for each class of faults ΣF i ⊆ Σf . Fur- ther analysis on K could help to enhance the diagnosability. In order to solve K-diagnosability for each ΣF i , it is sufficient to perform our algorithm for each class of faults ΣF i iteratively. Thus, the computational complexity will be linear with the number of fault classes. An On-the-fly and Incremental Method The UMDES library deals with diagnosability of systems modeled by automata based on the construction of an observer and a diagnoser automaton, which requires an exhaustive enumeration of the state space. However, we solve the classic diagnosability by handling a series of K-diagnosability problems, where K increases progressively. In other words, we reuse the state space generated while analyzing K-diagnosability to deal with (K + 1)-diagnosability. This is totally different from the approach in [1], since for each value of K a new system of equations is generated in their technique based on linear programming. Additionally, by progressively increasing K, it is certain to find Kmin if the system is diagnosable. Thanks to the on-the-fly investigation of diagnosability, building the whole FM-set tree is not necessary. Actually, for undiagnosable systems, the FM-set tree building as well as its exploration are stopped as soon as an indeterminate cycle is found. Moreover, for diagnosable systems, while generating a branch in the FM-set tree, we stop as soon as an F -certain or an existing node is obtained. This is a notable advantage compared with the existing approaches [4, 8 B. Liu, M. Ghazel and A. Toguyéni 15] which first build an exhaustive diagnoser or a reachability graph. The test result using the WODES diagnosis benchmark has shown this point since we were able to investigate diagnosability on models which are not tractable using UMDES library. Relation between Diagnosability and Boundedness of PNs The UMDES library solves the diagnosability problem based on exhaustive enumeration of the state space. Therefore, it can only deal with bounded systems modeled by finite state automata. It is worth noting that there exist two PN-based approaches for the diagnos- ability analysis of unbounded models. In [3], the authors check the diagnosability of unbounded PN models by analyzing the structure of the generated verifier net reachability graph. This approach requires an exhaustive enumeration of the reachability set of the verifier net, which may be larger than the reachability set of the original PN. In [1], the proposed approach is based on linear programming technique. System behavior is represented by a series of linear equations. The diagnosability of the unbounded PN models can be verified only if the faulty behavior can be described by a finite number of equations. With the help of the on-the-fly computation, our algorithm can determine undiagnosability as soon as an Fi -indeterminate cycle is detected. Hence, this approach can be applied to some unbounded PNs with an Fi -indeterminate cycle. Although an unbounded PN has infinite fault markings, which may result in an infinite number of fault marking sets (FM-sets), the construction of an FM-set tree terminates once an Fi -indeterminate cycle is detected and a negative diagnosability verdict is emitted. From a practical point of view, some thresholds need to be used if our algorithm is used to deal with unbounded LPNs. Case of Unlive PNs Note that we have extended our algorithm to also deal with unlive systems, while considering the definition of diagnosability relative to unlive DES, given in [14]. Besides, the WODES diagnosis benchmark we dealt with is unlive when n ≥ 2, which is against the assumption of liveness in [15]. Concretely, as the computation of the FM-set tree is performed on the fly, we have added an additional stopping condition: when some F -uncertain FM-set containing a deadlock state is obtained. Indeed, in this case, the system may stay indefinitely in this uncertain state, and no diagnosis verdict can be emitted. Limitations It is shown that some limitations of the WODES benchmark exist when testing diagnosability analysis approaches: – The benchmark is only live when k = 1. – The benchmark is only diagnosable when m = 1. In order to overcome these limitations, we develop the bounded and live n-line LC benchmark [12], which integrates both diagnosable and undiagnosable faults for any parameter n, as will be introduced in the following section. Lecture Notes in Computer Science: Authors’ Instructions 9 6 Application to the LC benchmark In this section, OF-PENDA is applied to a case study pertinent to railway safety. We study the fault diagnosis problems on an LC system. Our purpose here is two- fold: first, we show that OF-PENDA can deal with complex systems; secondly, the analysis results obtained on a quite complex example can show the efficiency of on-the-fly and incremental techniques in terms of time and memory compared with other existing approaches. Here, the complex model, namely the n-line LC will be modeled by an LPN with a great number of reachable markings. 6.1 n-line LC Benchmark The n-line LC benchmark, as shown in Figure 2, describes an n-line LC system composed of railway traffic, LC controller and barriers subsystems. The n-line LC benchmark can be obtained from the single-line LC model [10] while fulfilling the following controlling rules under a nominal situation: – The LC must be closed if any approaching train is detected in any line; – The LC can be reopened if there is no train in the “within” or “before” sections in any line. In other terms, the above rules eliminate all the possibilities that the collision between railway and road traffic may take place. In this global model, all the transitions are observable, but the faulty transi- tions, i.e., To = T \Tu and Tu = Tf = {t6 } ∪ (∪i {ti,5 }). The n-line LPN model can be rather big when n takes great values. The state space of the corresponding LPN models for the various values of n can be calculated by the TINA tool [2], as will be shown in Table 2. Recall here that not the whole state space will be generated while using our on-the-fly technique. However, the reachability graphs are generated in order to transform them into the input file (language equivalent automata) for UMDES. As shown in Table 2, the size of the reachability graph grows very quickly as n increases, since places p2 and p6 can hold as many as n tokens, due to which so many markings exist. 6.2 Diagnosability Analysis In this section, we will analyze the diagnosability of the LC model while consid- ering various values of n. Here, we will consider two fault classes: – For TF 1 = ∪ni=1 {ti,5 }, we consider all the faults ti,5 in each track as belonging to the same class. Recall that such faults express the fact that trains can enter the crossing zone while the barriers are not ensured to be down. – For TF 2 = {t6 }, this fault class depicts an early lowering of the barriers, i.e., before all the trains are ensured to have left the LC. 10 B. Liu, M. Ghazel and A. Toguyéni railway traffic tn,4 , aw4 tn,5 , ig pn,1 tn,1 , apn pn,2 tn,2 ,inn pn,3 tn,3 , lvn pn,4 t4 ··· ··· ··· t1,5 , ig ··· ··· ··· p1,1 t1,1 , ap1 p1,2 t1,2 , in1 p1,3 t1,3 , lv1 p1,4 LC controller p1 p2 n p3 p4 t1 , cr p9 t2 , or p5 n p6 barriers p7 , up n n t3 , kd t4 , lw t6 , bf t5 , rs p8 , down Fig. 2. n-line LC benchmark A comparative simulation with UMDES library is performed on an Intel PC (CPU: 2.50 GHz, RAM: 3.16 GB) and the results are given in Table 2, Figure 4 and Figure 3, where: – n is the number of railway tracks; – ΣF i is the considered fault class (ΣF 1 or ΣF 2 ); – |P | and |T | are the number of places and transitions of the LPN model respectively; – |A| and |R|, which are the number of the arcs and the nodes of the reachabil- ity graph respectively, give the scale of the LPN reachability graph computed by TINA and which serves as the input automaton states for UMDES; Table 2. Comparative simulation results based on n-line LC benchmark n ΣF i |P | |T | |A| |R| |N | |Diag| |Xv | DD DV DO K TT TD TV TO 1 13 11 28 24 24 26 15 YES YES YES 3 <1s <1s <1s <1ms 2 17 16 540 216 116 262 18 a.q. NO NO 11 <1s 11s <1s 15ms 3 21 21 6,256 1,632 173 1,924 18 a.q. NO NO 11 <1s 12s 7s 46ms 4 25 26 56,704 11,008 230 12,504 18 a.q. NO NO 11 <1s 32s 21m22s 62ms 5 29 31 442,880 68,608 287 75,722 18 a.q. o.t. NO 11 2s 28m34s o.t. 78ms 6 33 36 3,126,272 403,456 344 a.q. 18 o.t. o.t. NO 11 11s 1h36m o.t. 125ms ΣF 1 7 37 41 20,500,480 2,269,184 401 o.t. 18 o.t. o.t. NO 11 140s o.t. o.t. 156ms 8 41 46 127,074,304 12,320,768 458 o.t. 18 o.t. o.t. NO 11 29m o.t. o.t. 203ms 9 45 51 o.m. o.m. 515 - 18 - - NO 11 o.m. - - 249ms 10 49 56 o.m. o.m. 572 - 18 - - NO 11 o.m. - - 296ms 20 89 106 o.m. o.m. 1,142 - 18 - - NO 11 o.m. - - 1,467ms 40 169 206 o.m. o.m. 2,282 - 18 - - NO 11 o.m. - - 5,460ms 1 13 11 28 24 29 26 15 YES YES YES 7 <1s <1s <1s <1ms 2 17 16 540 216 277 262 207 YES YES YES 10 <1s <1s <1s 453ms 3 21 21 6,256 1,632 2,109 1,924 1842 YES YES YES 17 <1s <1s 5s 109s 4 25 26 56,704 11,008 13,353 12,504 5670 YES YES a.q. 18 <1s 20s 16m19s 2h4m 5 ΣF 2 29 31 442,880 68,608 o.t. 75,722 o.t. YES o.t. o.t. o.t. 2s 27m12s o.t. o.t. 6 33 36 3,126,272 403,456 o.t. o.t. o.t. o.t. o.t. o.t. o.t. 11s o.t. o.t. o.t. 7 37 41 20,500,480 2,269,184 o.t. o.t. o.t. o.t. o.t. o.t. o.t. 140s o.t. o.t. o.t. 8 41 46 127,074,304 12,320,768 o.t. o.t. o.t. o.t. o.t. o.t. o.t. 29m o.t. o.t. o.t. 9 45 51 o.m. o.m. o.t. - o.t. - - o.t. o.t. o.m. - - o.t. Note: o.m. = out of memory o.t. = out of time (¿ 6h) a.q.= accidental quit  results obtained by TINA  results obtained by diag UR.exe and dcycle.exe of UMDES Lecture Notes in Computer Science: Authors’ Instructions  results obtained by verifier dia.exe of UMDES  results obtained by OF-PENDA 11 12 B. Liu, M. Ghazel and A. Toguyéni Fig. 3. Time cost for the diagnosability analysis on ΣF 2 Fig. 4. Time cost for the diagnosability analysis on ΣF 1 – |N | is the number of (on-the-fly) generated fault markings by OF-PENDA when the diagnosability verdict is issued; – |Diag| is the number of diagnoser states generated by UMDES (the diagnoser approach) which were needed to give the diagnosability verdict; – |Xv | is the number of (on-the-fly) generated FM-sets by OF-PENDA when the diagnosability verdict is issued, and corresponds also to the number of nodes of the diagnoser derived from this FM-set tree when the model is diagnosable; – DD , DV and DO are the diagnosability verdicts obtained by diagnoser ap- proach, verifier approach of UMDES and OF-PENDA respectively, where “Yes” indicates that the system is diagnosable and “No” indicates undiag- nosable; – K is the minimum value ensuring diagnosability computed by OF-PENDA, if the system is diagnosable; otherwise, it is the last value under which K- diagnosability is investigated before concluding that the system is undiag- nosable; Lecture Notes in Computer Science: Authors’ Instructions 13 – TT is the time needed to generate the LPN reachability graph computed by TINA, i.e., the time used for preparing the input automaton needed for UMDES; – TD , TV and TO are the times needed to obtain the diagnosability verdict by dcycle.exe (diagnoser approach), verifer dia.exe (verifier approach) of UMDES and OF-PENDA (on-the-fly approach), respectively. 6.3 Discussions For the comparative simulation results, the following remarks can be made: 1. The UMDES library has been integrated in the DESUMA framework which also integrates GIDDES for graphical facilities. Here, we directly use the com- mand lines in UMDES library rather than the interface framework (DESUMA), since the DESUMA takes so much time to load large automaton models. 2. The scale of the PN reachability graph grows quickly (cf. the columns enti- tled with |A| and |R| in Table 2) as n increases. The capability of TINA to calculate the reachability graph considerably depends on the memory of the computer, since TINA needs to refer to the already built part of the reacha- bility graph all along the computation. One can observe that the generated .aut files become considerable starting from n = 7. For instance, the size of the .aut files for 1, 2, 3, 4, 5, 6, 7-line LC benchmark is 655b, 11KB, 128KB, 1.2MB, 9.9MB, 74.8MB, 518.6MB, respectively. A Mac with a RAM of 16GB cannot store the .aut file for 8-line benchmark even if it can be calculated eventually. For the case of n = 9, the calculation stops with an “out of mem- ory” error. Thus, the analysis of the cases with n ≥ 9 cannot be performed using UMDES. 3. The simulation using UMDES and OF-PENDA is performed on a Windows PC. For ΣF 1 , some “accidental quits” happen during the running of dcy- cle.exe (diagnoser approach in UMDES) for some cases. However, the diag- nosability verdict can be obtained by using the verifier technique (command verifier dia.exe) in UMDES library. Note that the relative results given by OF-PENDA when an accidental quit happens are the last outputs before the program’s exit. We do not know exactly the reason for this problem. The improvement of the source code and using other operation systems may eliminate the problems. 4. In order to compare the efficiency in terms of time, we make a record of the computing time for each case. The time indicated in the columns entitled with To , TD and TV are obtained by an external timer, since TINA and UMDES do not output this information. Thus, there is an error margin of ±1s. For the OF-PENDA, an automatic timer has been integrated with an error margin of less than 1ms. 5. Besides the diagnosability verdict, OF-PENDA also gives the minimum value of K to ensure diagnosability, which cannot be obtained by UMDES. 6. In these cases, the number of FM-sets generated by OF-PENDA is lower than the number of diagnoser states given by UMDES. This shows the advantage 14 B. Liu, M. Ghazel and A. Toguyéni offered by our on-the-fly technique in terms of memory consumption in terms of memory consumption. Besides, it is worthwhile to mention that the FM- sets can be far fewer than the diagnoser states when an indeterminate cycle exists, i.e., if the model is undiagnosable, and is detected early. 7. It is worthwhile to notice that the FM-set tree is generated by OF-PENDA directly from the LPN, while the UMDES takes an automaton as an input which is equivalent to the reachability graph of the LPN. In other words, the inputs for UMDES and OF-PENDA are not the same and we had to compute the LPN reachability graph a priori before performing analysis via UMDES, whereas, on the contrary, the reachable markings are computed on the fly while investigating diagnosability by OF-PENDA. 8. The results (cf. column TD and TV ) show that the diagnoser approach is more efficient than the verifier approach while dealing with the n-line LC benchmark. This does not violate the claim that the verifier approach is more efficient in terms of time complexity (polynomial for the verifier approach vs. exponential for the diagnoser approach), since the theoretical complexity is always computed while considering the worst case. More importantly, compared with the diagnoser and verifier approaches, our on-the-fly approach can deal with some quite complex models that UMDES cannot deal with (e.g., for the cases ΣF 1 when n ≥ 7), especially for some undiagnosable systems, and shows better efficiency in terms of time and memory. For example, the diagnosability analysis for the LC model is performed in less than 6 seconds, for even when n = 40, whereas UMDES (diagnoser and verifier techniques) do not issue a verdict within 6 hours for n > 4. However, for the diagnosable cases (ΣF 2 ), we spend less memory but more time than UMDES, although the obtained results remain comparable: OF-PENDA and UMDES- verifier block from n = 4, whereas UMDES-diagnoser blocks at n = 5. This gap in terms of efficiency depending on whether the model is diagnosable or not can be explained as follows: For the undiagnosable models, the analysis by OF-PENDA is completed as soon as an indeterminate cycle is found which can occur quickly, hence avoiding the generation and analysis of an important part of the state space. However, for diagnosable models, it is likely that a bigger part of the state space is generated/analyzed since, in this case, the only stopping condition which allows us to avoid building/investigating the whole state space is when a faulty node is generated. Indeed, since we deal with permanent faults, it is useless to continue investigating the following nodes since they are faulty as well. 7 Conclusion OF-PENDA is a software tool for the diagnosis of DESs modeled by LPNs, on the basis of the techniques developed in [11]. For diagnosable bounded systems, the minimum value Kmin ensuring K-diagnosability is given. Besides, thanks to the incremental search it implements, OF-PENDA can also issue diagnosis verdict for some unlive and/or unbounded LPN models under some conditions. Lecture Notes in Computer Science: Authors’ Instructions 15 Two benchmarks have been used in this paper for illustrating the efficiency of OF-PENDA while a comparison discussion is carried out w.r.t some existing techniques. As future works, we intend to improve the source code of our tool and to integrate some heuristics to guide the depth-first search technique adopted here, while defining some priority rules as regards the branches to be investigated first. Acknowledgement The present research work has been partially supported by the International Cam- pus on Safety and Intermodality in Transportation, the Nord-Pas-de-Calais Region, the European Community, the Regional Delegation for Research and Technology, the Ministry of Higher Education and Research, and the National Center for Scientific Research. The authors gratefully acknowledge the support of these institutions. References 1. F. Basile, P. Chiacchio, and G. De Tommasi. On K-diagnosability of Petri nets via integer linear programming. Automatica, 48(9):2047–2058, Sept. 2012. 2. B. Berthomieu, P.-O. Ribet, and F. Vernadat. The tool TINA - Construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research, 42(14):2741–2756, July 2004. 3. M. P. Cabasino, A. Giua, S. Lafortune, and C. Seatzu. A new approach for diagnos- ability analysis of Petri nets using verifier nets. IEEE Transactions on Automatic Control, 57(12):3104–3117, Dec. 2012. 4. M. P. Cabasino, A. Giua, and C. Seatzu. Fault detection for discrete event systems using Petri nets with unobservable transitions. Automatica, 46(9):1531–1539, Sept. 2010. 5. C. G. Cassandras and S. Lafortune. Introduction to discrete event systems. Springer, 2 edition, 2007. 6. A. Giua. A benchmark for diagnosis. http://www.diee.unica.it/giua/WODES/ WODES08/media/benchmark diagnosis.pdf, 2007. 7. S. Jiang, Z. Huang, V. Chandra, and R. Kumar. A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Transactions on Automatic Control, 46(8):1318–1321, 2001. 8. S. Koenig, M. Likhachev, Y. Liu, and D. Furcy. Incremental heuristic search in AI. AI Magazine, 25(2):99–112, 2004. 9. S. Lafortune. UMDES-Lib software library. http://www.eecs.umich.edu/ umdes/toolboxes.html, 2000. 10. N. G. Leveson and J. Stolzy. Analyzing safety and fault tolerance using time petri nets. Formal Methods and Software Development, 186, 1985. 11. B. Liu. An efficient approach for diagnosability and diagnosis of DES based on labeled Petri nets - untimed and timed contexts. PhD thesis, Univ. Lille Nord de France, 2014. 12. B. Liu. N-track level crossing benchmark. http://6814.is- programmer.com/posts/45619.html, 2014. 13. B. Liu, M. Ghazel, and A. Toguyéni. Toward an efficient approach for diagnosabil- ity analysis of DES modeled by labeled Petri nets. In The 13th European Control Conference (ECC’14), 2014. 16 B. Liu, M. Ghazel and A. Toguyéni 14. M. Sampath, S. Lafortune, and D. Teneketzis. Active diagnosis of discrete-event systems. IEEE Transactions on Automatic Control, 43(7):908–929, July 1998. 15. M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Di- agnosability of discrete-event systems. IEEE Transactions on Automatic Control, 40(9):1555–1575, 1995. 16. S. Schwoon and J. Esparza. A note on on-the-fly verification algorithms. Springer, 2005. 17. T.-S. Yoo and S. Lafortune. Polynomial-time verification of diagnosability of par- tially observed discrete-event systems. IEEE Transactions on Automatic Control, 47(9):1491–1495, Sept. 2002.