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

TL;DR

This paper introduces new algorithms for verifying strong periodic detectability and strong periodic D-detectability in finite-state automata, improving computational bounds and removing previous assumptions.

Contribution

It presents novel algorithms for verifying SPD and SPDD in FSAs, strengthening theoretical bounds and eliminating prior assumptions.

Findings

Verifies SPD in NL complexity class

Verifies SPDD in PSPACE complexity class

Strengthens existing bounds on detectability verification

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.