Skip to Main content Skip to Navigation
Journal articles

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

Abstract : Checking 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.
Complete list of metadata
Contributor : Yannick Pencolé <>
Submitted on : Friday, February 12, 2021 - 12:43:26 PM
Last modification on : Thursday, June 10, 2021 - 3:48:20 AM
Long-term archiving on: : Thursday, May 13, 2021 - 6:58:34 PM


Files produced by the author(s)



Yannick Pencolé, Audine Subias. Diagnosability of event patterns in safe labeled time Petri nets: a model-checking approach. IEEE Transactions on Automation Science and Engineering, Institute of Electrical and Electronics Engineers, inPress, ⟨10.1109/TASE.2020.3045565⟩. ⟨hal-03139863⟩



Record views


Files downloads