Analysis of strong and strong periodic detectability of bounded labeled Petri nets

Detectability describes the property of a system to uniquely determine, after a finite number of observations, the current and the subsequent states. Different notions of detectability have been proposed in the literature. In this paper, we formalize and analyze strong detectability and strong periodic detectability for systems that are modeled as labeled Petri nets with partial observation on their transitions. We provide three new approaches for the verification of such detectability properties using three different structures. The computational complexity of the proposed approaches is analyzed and the three methods are compared. The main feature of all the three approaches is that they do not require the calculation of the entire reachability space or the construction of an observer. As a result, they have lower computational complexity than other methods in the literature.