Diagnosability of event patterns in safe labeled time Petri nets: a model-checking approach

International audienceChecking the diagnosability of a time discrete event system usually consists in determining whether a single fault event can always be identified with certainty after a finite amount of time. The aim of this paper is to extend this type of analysis to more complex behaviors, called event patterns, and to propose an effective method to check diagnosability with the use of modelchecking techniques. To do so, we propose to convert the pattern diagnosability problem into checking a linear-time property over a specific time Petri net. Note to Practitioners-This paper is motivated by the problem of improving the monitoring and the supervision of systems like automated and robotised manufacturing systems. Based on a model of the system, the paper proposes a method to assert with certainty whether the available set of sensors will always provide enough information to ensure that a complex and unexpected behavior has not happened in the system. The proposed method uses a publicly available model-checking tool to perform this analysis