Verification of Detectability in Labeled Petri Nets
Yin Tong, Hao Lan, Jin Guo · 2019
Detectability describes the property of an system whose current and the subsequent states can be uniquely determined after a finite number of observations. In this paper, we extend four types of detectability: strong detectability, weak detectability, periodically strong detectability, and periodically weak detectability, from finite automata to labeled Petri nets, which have larger modeling power than finite automata. Moreover, based on the notion of basis markings, the approaches are developed to verify the four detectability of a bounded labeled Petri net system. Without computing the whole reachability space and without enumerating all the markings consistent with an observation, the proposed approaches are more efficient.