New methods for verifying strong periodic detectability and strong periodic D-detectability of discrete-event systems

2021/09/18 by Kuize Zhang, Zhang, Kuize
Computer Science · #Distributed systems and fault tolerance #FOS: Mathematics #Formal Methods in Verification #Optimization and Control (math.OC) #Petri Nets in System Modeling

paper · pdf · doi:10.48550/arxiv.2109.08854

openalex publication_date 2021/09/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

In this paper, in discrete-event systems modeled by finite-state automata (FSAs), we show new thinking on the tools of detector and concurrent composition and derive two new algorithms for verifying strong periodic detectability (SPD) without any assumption that run in NL; we also reconsider the tool of observer and derive a new algorithm for verifying strong periodic D- detectability (SPDD) without any assumption that runs in PSPACE. These results strengthen the NL upper bound on verifying SPD and the PSPACE upper bound on verifying SPDD for deadlock-free and divergence-free FSAs in the literature.

Related

• On Verification of D-Detectability for Discrete Event Systems
• Complexity of Deciding Detectability in Discrete Event Systems
• Revisiting delayed strong detectability of discrete-event systems
• A unified method to decentralized state inference and fault diagnosis/prediction of discrete-event systems
• Verification of Strong K-Step Opacity for Discrete-Event Systems