Fault detection based on Petri net models with faulty behaviors

We consider Petri net models of discrete event systems with faulty behaviors which are triggered by the firing of failure transitions. We extend a necessary and sufficient condition for diagnosability shown by Sampath et al. (1994, 1995) to unbounded Petri nets. But it is algorithmically impossible to check the condition in general. We introduce methods for modification of coverability trees in order to detect failure transitions. By using such approximated sets, we propose two kinds of diagnosers called a difference marking ω-diagnoser and an ω-refined diagnoser. For observable places whose token numbers are replaced by ω in the coverability trees, the former diagnoser calculates difference between token numbers before and after partially observed markings change, and detects failures. In the latter diagnoser, we refine the symbol ω, and modify the coverability tree in order to distinguish markings reachable by normal behaviors from those reachable by faulty behaviors.