Design of Online Supervisors for Enforcing Diagnosability in Petri Nets With Unknown Initial Markings

This article formalizes and solves the problem of diagnosability verification and enforcement of discrete event systems (DESs) that are modeled by Petri nets with unknown initial markings, i.e., the number of tokens in part or all of the places is unknown or uncertain at an initial marking. A revised topology of the original net with a certain initial marking, called an acceptable initial-model (AIM), is constructed to verify the diagnosability of such a system without testing diagnosability for each possible initial marking. The process applies a diagnosability verification agent, called an extended verifier that is obtained from the proposed AIM. We prove that a Petri net with unknown initial markings is diagnosable if and only if there does not exist any uncertain fault path in the verifier. The result also provides sufficient and necessary conditions for enforcing diagnosability by developing an online supervisor. Examples are presented to demonstrate the proposed method.