Verification of $k$-Step and Definite Critical Observability in Discrete-Event Systems

In this paper, 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 (i) the $k$-step critical observability that requires that the critical states can be distinguished from non-critical ones after a loss of consecutive $k$ events, and (ii) the definite critical observability that is a generalization of $k$-step critical observability for all nonnegative integers $k$. Then a structure called $k$-extended detector is proposed. Necessary and sufficient conditions for $k$-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 $(\frac{1}{2}(|Q|^{2}+|Q|))$-step critical observability, where $Q$ 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 $k_{max}$ (if it exists) such that the plant is $k_{max}$-step critically observable.