2019/08/26 by Hao Lan, Yin Tong, Lan, Hao +5
Computer Science · #FOS: Electrical engineering #Formal Methods in Verification #Petri Nets in System Modeling #Real-Time Systems Scheduling #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1908.09604
openalex publication_date 2019/08/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Detectability describes the property of a system to uniquely determine, after a finite number of observations, the current and subsequent states. In this paper, to reduce the complexity of checking the detectability properties in the framework of bounded labeled Petri nets, we use a new tool, which is called detector, to verifying the strong detectability and periodically strong detectability. First, an approach, which is based on the reachable graph and its detector, is proposed. Then, we develop a novel approach which is based on the analysis of the detector of the basis reachability graph. Without computing the whole reachability space, and without building the observer, the proposed approaches are more efficient.