Verification of [Formula Omitted]-Step and Definite Critical Observability in Discrete-Event Systems

• Published in: IEEE transactions on automatic control 2023-01, Vol.68 (7), p.4305
• Main Authors: Yin, Tong, Ma, Ziyue
• Format: Article
• Language: English
• Subjects: Algorithms; Discrete event systems; Polynomials; Verification
• ISSN: 0018-9286; 1558-2523
• DOI: 10.1109/TAC.2022.3202983

In this article, we study the verification of critical observability in discrete-event systems in which a plant and its observer are connected via an unreliable communication channel. We consider a communication protocol in which each packet sent from the plant consists of an event and the sequence number of the packet. We define two novel notions of critical observability called first, the [Formula Omitted]-step critical observability that requires that the critical states can be distinguished from noncritical ones after a loss of consecutive [Formula Omitted] events, and second, the definite critical observability that is a generalization of [Formula Omitted]-step critical observability for all nonnegative integers [Formula Omitted]. Then, a structure called [Formula Omitted]-extended detector is proposed. Necessary and sufficient conditions for [Formula Omitted]-step critical observability are derived, which can be verified with polynomial complexity. Moreover, we prove that the definite critical observability can be verified by checking the [Formula Omitted]-step critical observability, where [Formula Omitted] is the set of states of a plant. For a plant that is not definitely critically observable, a polynomial algorithm has been proposed to obtain a maximal nonnegative integer [Formula Omitted] (if it exists) such that the plant is [Formula Omitted]-step critically observable.