arXiv · 1903.07827
Verification of C-detectability Using Petri Nets
Abstract
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 relax detectability to C-detectability that only requires a given set of crucial states can be distinguished from other states. Four types of C-detectability: strong C-detectability, weak C-detectability, periodically strong C-detectability, and periodically weak C-detectability are defined in the framework of 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 C-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.
Explore related subjects
Keep this discovery
Hao Lan, Yin Tong, Jin Guo, Carla Seatzu. 2019-03-19. Verification of C-detectability Using Petri Nets. https://doi.org/10.1016/j.ins.2020.04.024
Cite the original work for its findings. Save a collection to share your selection of sources.