On-the-fly diagnosability analysis of LPN using verifier nets

In this paper, the on-the-fly diagnosability analysis using Verifier Nets (VN) is developed. The objective is to improve the VN approach by using on-the-fly diagnosability analysis technique. The diagnosability is analyzed in the framework of bounded and unbounded labeled Petri nets (LPN) with no deadlock after firing any fault transition. The VN and its reachability graph (for bounded LPN)/ coverability graph (for unbounded LPN) are built on-the-fly and in parallel for diagnosability analysis. Stop conditions are proposed to stop the construction as soon as a diagnosability decision is established. This approach achieves a compromise between computation efficiency and combinatorial explosion limitation.