Polynomial-Time Verification and Enforcement of Delayed Strong Detectability for Discrete-Event Systems

Detectability is a fundamental property in partially observed dynamical systems. It describes whether one can use observed output sequences to determine the current and subsequent states. Delayed detectability generalizes detectability in the sense that when doing state estimation at a time instant, some outputs after the instant are also considered, making the estimation more accurate. In this article, we use a novel concurrent-composition method to give polynomial-time algorithms for verifying several delayed versions of strong detectability of discrete-event systems modeled by finite-state automata in the contexts of formal languages and $\omega$-languages without any assumption, which strengthen the polynomial-time verification algorithms in the literature based on two fundamental assumptions of liveness (aka deadlock-freeness) and divergence-freeness (the former implies an automaton will never halt and the latter implies the running of an automaton will always be eventually observed). In addition, based on our verification algorithms, we obtain polynomial-time algorithms for enforcing these notions of delayed strong detectability in an open-loop manner, which work in a different way compared with the existing exponential-time enforcement algorithms under the supervisory control framework in a closed-loop manner. Moreover, by using our methods, polynomial-time enforcement algorithms can be designed for many polynomially verifiable inference-based properties such as diagnosability and predictability.