Diagnosability analysis and online diagnosis are two crucial issues in safety critical 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 unobservable 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 techniques 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 deal with is the computation complexity. In particular, the state explosion phenomenon 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 adapting 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 analysis 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, K min , the minimum 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 Section 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.
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 postincidence 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, M 0 ) is a PN N with given initial marking M 0 . For short, a marked PN will be called PN afterward. A transition t i is enabled at marking M if M ≥ P re(•, t i ), denoted by M [ t i >.
A PN (N, M 0 ) is bounded if the number of tokens in each place does not exceed a finite number m ∈ N for any marking reachable from M 0 . A PN is live if, no matter what marking has been reached from M 0 , it is possible to ultimately fire any transition of the net by progressing through some further firing sequence.
An LPN is a tuple N L = (N, M 0 , Σ, ϕ), where (N, M 0 ) 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
For short, we write L instead of L(N L ). We denote by s = s 1 s 2 . . . s n the concatenation of s 1 , s 2 , . . . , s n , where s 1 , s 2 , . . . , s n ∈ Σ * .
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 = T o T u . Moreover, the faulty transitions are unobservable (T f ⊆ T u ). Also, the set of fault events can be partitioned into m sets, Σ f = m i=1 Σ Fi , where Σ Fi denotes one class of faults. Let P o : Σ * → Σ * o be the projection which "erases" the unobservable events in a sequence s ∈ Σ * . The inverse projection operator P −1 o is defined as
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 = {s ∈ Σ * | ss ∈ L}. We denote the length of string s by |s|, and the i th event of sequence s by s i . For a ∈ Σ and s ∈ Σ * , we write a ∈ s if i exists such that s i = a.
For a K-diagnosable system S, it is obvious that S is K -diagnosable for any K ≥ K. Besides, K min exists such that S is K min -diagnosable, and S is not K -diagnosable for all K < K min .
3 Techniques Applied in OF-PENDA
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 solutions. 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 techniques 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 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-thefly 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 return 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.
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 K min 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 K min , without using the previous search results.
The incremental technique is a skillful technique to speed up the search procedure. 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.
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 generated 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 memory, 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++.
OF-PENDA takes the mathematical model of an LPN as input, i.e., the matrices P re, P ost, M 0 , 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 K min 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 benchmark 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.
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.
We now analyze the diagnosability upon the fault class Σ F 1 = {f 1 , . . . , f n−1 }. In other terms, only one class of faults is considered here. In order to perform 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 considered 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 parameters of the WODES diagnosis benchmark. -The 4 th 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 5 th column entitled "|N |" is the number of the FM-graph nodes. -The 8 th (resp. 9 th ) column entitled "D D " (resp. D O ) is the diagnosability verdict returned by UMDES (resp. OF-PENDA), where "Yes" indicates that the system is diagnosable and "No" indicates undiagnosable. -The 10 th 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 "K min ".
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.
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 K min 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 K min gives us a valuable piece of information indicating the minimum number of steps necessary to detect and identify faults for a 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 diagnosability 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 . Further 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 K min 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,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.
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 diagnosability 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 F i -indeterminate cycle is detected. Hence, this approach can be applied to some unbounded PNs with an F i -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 F i -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.
-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.
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 twofold: 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.
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 transitions, i.e., T o = T \T u and
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 p 2 and p 6 can hold as many as n tokens, due to which so many markings exist.
In this section, we will analyze the diagnosability of the LC model while considering various values of n. Here, we will consider two fault classes:
-For T F 1 = ∪ n i=1 {t i,5 }, we consider all the faults t i,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 T F 2 = {t 6 }, this fault class depicts an early lowering of the barriers, i.e., before all the trains are ensured to have left the LC.
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; - -|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; -|X v | 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; -D D , D V and D O are the diagnosability verdicts obtained by diagnoser approach, verifier approach of UMDES and OF-PENDA respectively, where "Yes" indicates that the system is diagnosable and "No" indicates undiagnosable; -K is the minimum value ensuring diagnosability computed by OF-PENDA, if the system is diagnosable; otherwise, it is the last value under which Kdiagnosability is investigated before concluding that the system is undiagnosable; -T T 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; -T D , T V and T O 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.
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 command 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 entitled 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 reachability 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 memory" 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 dcycle.exe (diagnoser approach in UMDES) for some cases. However, the diagnosability 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 T o , T D and T V 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 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 FMsets 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 T D and T V ) 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 UMDESverifier 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.
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 K min 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. 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.
The present research work has been partially supported by the International Campus 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.