In this paper, a software tool to deal with diagnosis of discrete 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 labeled 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 onthe- y 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 e ciency in terms of time and memory compared with some existing approaches.
Diagnosability analysis and online diagnosis are two crucial issues in safety
critical systems. Most of such systems can be modeled as DESs [
In the past two decades, diagnosability analysis has been studied using
techniques such as diagnoser automata [
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 [
The reminder of this paper is organized as follows. Section 2 brie y introduces some notations pertaining to LPN and (K)-diagnosability. Section 3 discusses the on-the- y 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 e ciency of OF-PENDA in Section 5 and 6, respectively. Finally, some concluding remarks are given in Section 7. 2
2.1
Labeled Petri Nets A Petri net (PN) is a tuple N = (P; T; P re; P ost), where P is a nite set of places; T is a nite 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 2 N jP j 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 nite number m 2 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 re any transition of the net by progressing through some further ring sequence.
An LPN is a tuple NL = (N; M0; ; '), where (N; M0) is a marked PN; is a nite 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) = f'( ) 2 j 2 T ; M0 [ >g. For short, we write L instead of L(NL). We denote by s = s1s2 : : : sn the concatenation of s1; s2; : : : ; sn, where s1; s2; : : : ; sn 2 .
K-diagnosability In event-based diagnosis of DESs, event set is partitioned into two disjoint sets, = o ] u, where o is a nite set of observable events and u is a nite 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 (Tf Tu). Also, the set of fault events can be partitioned into m sets, f = Uim=1 Fi , where Fi denotes one class of faults.
Let Po : ! o be the projection which \erases" the unobservable events in a sequence s 2 . The inverse projection operator Po 1 is de ned as Po 1(r) = fs 2 L j Po(s) = rg for r 2 o . Given a live and pre x-closed language L and a string s 2 L, the post-language of L after s denoted by L=s is L=s = fs0 2 j ss0 2 Lg. We denote the length of string s by jsj, and the ith event of sequence s by si. For a 2 and s 2 , we write a 2 s if i exists such that si = a.
De nition 1. Given an LPN NL and K 2 N , e 2 f is K-diagnosable if 8u 2 L; ujuj 2 f and 8v 2 L=u such that jPo(v)j K, then
r 2 Po 1(Po(uv)) ) e 2 r
For a K-diagnosable system S, it is obvious that S is K 0-diagnosable for any K 0 K. Besides, Kmin exists such that S is Kmin-diagnosable, and S is not K 0-diagnosable for all K 0 < Kmin. 3 3.1
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 [
On-the- y techniques can save memory resources. Generally, on-the- y techniques permit us to generate and investigate only a part of the state space to nd solutions, unlike the classic enumerative approaches which have to build the whole state space a priori. On-the- y 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- y techniques can save computing time. On the one hand, on-they exploration terminates as soon as some speci c 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- y 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- y techniques can deal with some unbounded systems, since they return a verdict as soon as some speci c features are found, instead of investigating the whole in nite state space, as will be shown in Section 5. 3.2
Incremental Search Technique
The incremental method [
As in [
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- y analysis to perform an e cient analysis. Both techniques do not change the computation complexity. However, they improve the searching e ciency when dealing with real systems. 4
In [
OF-PENDA is the implementation of various algorithms elaborated in [
OF-PENDA takes the mathematical model of an LPN as input, i.e., the
matrices P re, P ost, M0, the event-mapping matrix [
In order to show the e ciency of on-the- y and incremental techniques in
diagnosability analysis, the WODES benchmark [
The WODES diagnosis benchmark [
Comparative Results We now analyze the diagnosability upon the fault class F 1 = ff1; : : : ; fn 1g. 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 le. Thus, we rst generate the reachability graph of the considered PN with the help of TINA yielding to a .aut le, which is then transformed into a .fsm le 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 rst 3 columns entitled \m", \n" and \k" are the basic structural parameters of the WODES diagnosis benchmark. { The 4th column entitled \jRj" 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 \jN j" is the number of the FM-graph nodes. { The 6th column entitled \jDiagj" is the number of the diagnoser automaton states generated by UMDES. { The 7th column entitled \jXvj" 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 [
Online, the value of Kmin gives us a valuable piece of information
indicating the minimum number of steps necessary to detect and identify faults for a
m n k jRj jN j jDiagj jXvj DD DO K m n k jRj jN j jDiagj jXvj 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 [
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 su cient 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- y 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 di erent from the approach
in [
Thanks to the on-the- y 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 [
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 nite state automata.
It is worth noting that there exist two PN-based approaches for the
diagnosability analysis of unbounded models. In [
With the help of the on-the- y 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 in nite fault markings, which may result
in an in nite 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 de nition of diagnosability relative to
unlive DES, given in [
{ The benchmark is only diagnosable when m = 1.
In order to overcome these limitations, we develop the bounded and live n-line
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 twofold: rst, we show that OF-PENDA can deal with complex systems; secondly, the analysis results obtained on a quite complex example can show the e ciency of on-the- y 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 tra c, LC controller and barriers subsystems. The n-line
LC benchmark can be obtained from the single-line LC model [
In other terms, the above rules eliminate all the possibilities that the collision between railway and road tra c may take place.
In this global model, all the transitions are observable, but the faulty transitions, i.e., To = T nTu and Tu = Tf = ft6g [ ([ifti;5g).
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 [
Recall here that not the whole state space will be generated while using our on-the- y technique. However, the reachability graphs are generated in order to transform them into the input le (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 considering various values of n. Here, we will consider two fault classes: n { For TF 1 = [i=1fti;5g, 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 = ft6g, this fault class depicts an early lowering of the barriers, i.e., before all the trains are ensured to have left the LC. railway tra c tn;4, aw4 tn;5, ig tn;2,inn pn;1 tn;1, apn pn;2 pn;3 tn;3, lvn pn;4 p1;1 t1;1, ap1 p1;2 p1;3 t1;3, lv1
p1;4 t4 t1;5, ig t1;2, in1 p9 p3
p4 t2, or n p6 p7, upn
n t6, bf
t5, rs p8, down LC controller p1
p2 n t1, cr
p5 barriers t3, kd t4, lw
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); { jP j and jT j are the number of places and transitions of the LPN model respectively; { jAj and jRj, which are the number of the arcs and the nodes of the reachability graph respectively, give the scale of the LPN reachability graph computed by TINA and which serves as the input automaton states for UMDES; k r a h c n e b L e n i l n n o d e s a b s t l u s e r n o i t e v i t a r a p m o C
O T j R j i F
Lecture Notes in Computer Science: Authors' Instructions 11 s s s s s s s s s s s s s s s m ..t ..t ..t ..t ..t S m m m m m m m m m m m m m m 09 4 o o o o o E 1 5 6 2 8 5 6 3 9 6 7 0 1 3 1 h D < 1 4 6 7 2 5 0 4 9 6 6 < 45 2 1 1 2 2 2 ,4 ,4 M 1 5 U f o e x e . e l c y c d t a i e x e . a i d r e i IN re T v m V < <
T C T
D < 1 1 3 3 6 o o
3 m h 8 1 2
< <
< < < 2 1 o o o b b D Y N N N N N N N N N N N Y Y Y a o o o o o ) o o V S O O O ..t ..t ..t ..t - - - - S S S S .t ..t ..t ..t - 6h lts lts D E N N N o o o o
E E E E .o o o o > u u
Y Y Y Y ( s s Y
. . . - - - - S S S S S .t ..t ..t - e re re D SE ..q ..q ..q ..q .t .t .t D a a a a o o o
E E E E E .o o o im
Y Y Y Y Y t Y . . . . f j 5 8 8 8 8 8 8 8 8 8 8 8 5 7 2 0 .t .t .t .t .t o v 1 1 1 1 1 1 1 1 1 1 1 1 1 0 4 7 . S
2 8 6 o o o o o t X u E j 1 5 m 7 2 n U E e P d g i . cc ida FO
4 6 3 0 7 4 1 8 5 2 2 2 9 7 9 3 .t ..t ..t ..t ..t j 2 1 7 3 8 4 0 5 1 7 4 8 2 7 0 5 .
1 1 2 2 3 4 4 5 5 ,1 ,2 2 ,1 ,3 o o o o o N j 1 2 2 3
1 2 1 3 0 0 5 8 6 m .m .m .m 2 1 3 0 0 5 8 6 m
2 ,6 ,0 ,6 ,4 ,1 ,7 .o o o o 2 ,6 ,0 ,6 ,4 ,1 ,7 .o A j 1 6 1 6 1 6 1 6 1 6 6 6 1 6 1 6 1 6 1 6 1 u u T 1 1 2 2 3 3 4 4 5 5 0 0 1 1 2 2 3 3 4 4 5 = se se j 1 2 . r r 2 2
1 3 0 7 2 2
1 j b a Aj T 8 0 6 4 0 2 0 4 . . . . 8 0 6 4 0 2 0 4 . ro b b 2 54 ,256 ,7065 ,88244 ,,27621 ,,48005 ,,30470 .om .om .om .om 2 54 ,265 ,7605 ,82844 ,,26721 ,,40805 ,,34070 .om feomm iteandb iteandb o o 1 1 8 3 9 0 1 6 0 6 2 4 ,2 ,
3 2 2
1 y y y 3 0 7 2 2 t 1 ou lts lt s { jN j is the number of (on-the- y) generated fault markings by OF-PENDA when the diagnosability verdict is issued; { jDiagj is the number of diagnoser states generated by UMDES (the diagnoser approach) which were needed to give the diagnosability verdict; { jXvj is the number of (on-the- y) 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 approach, veri er 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; { 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 (veri er approach) of UMDES and OF-PENDA (on-the- y approach), respectively. 6.3 For the comparative simulation results, the following remarks can be made: o ered by our on-the- y 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 y while investigating diagnosability by OF-PENDA. 8. The results (cf. column TD and TV ) show that the diagnoser approach is more e cient than the veri er approach while dealing with the n-line LC benchmark. This does not violate the claim that the veri er approach is more e cient in terms of time complexity (polynomial for the veri er 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 veri er approaches, our on-the- y 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 e ciency 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 veri er 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 UMDESveri er block from n = 4, whereas UMDES-diagnoser blocks at n = 5. This gap in terms of e ciency 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
OF-PENDA is a software tool for the diagnosis of DESs modeled by LPNs, on
the basis of the techniques developed in [
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 Scienti c Research. The authors gratefully acknowledge the support of these institutions.