Dr Kuize Zhang

Observability is a fundamental property of a partially-observed dynamical system, which means whether one can use an input sequence and the corresponding output sequence to determine the initial state. Observability provides bases for many related problems such as state estimation, identification, disturbance decoupling, controller synthesis, etc. Until now, fundamental improvement has been obtained in observability of Boolean control networks mainly based on two methods — Edward F. Moore’s partition and our observability graph (or their equivalent representations found later based on the semitensor product (STP) of matrices (where the STP was proposed by Daizhan Cheng)), including necessary and sufficient conditions for different types of observability, extensions to probabilistic Boolean networks (PBNs) and singular BCNs, even to nondeterministic finite-transition systems (NFTSs); and the development (with the help of the STP of matrices) in related topics such as computation of smallest invariant dual subspaces of BNs containing a set of Boolean functions, multiple-experiment observability verification/decomposition in BCNs, disturbance decoupling in BCNs, etc. This paper provides a thorough survey for these topics. The contents of the paper are guided by the above two methods. First, we show that Moore’s partition-based method closely relates the following problems: computation of smallest invariant dual subspaces of BNs, multiple-experiment observability verification/decomposition in BCNs, and disturbance decoupling in BCNs. However, this method does not apply to other types of observability or nondeterministic systems. Second, we show that based on our observability graph, four different types of observability have been verified in BCNs, verification results have also been extended to PBNs, singular BCNs, and NFTSs. In addition, Moore’s partition also shows similarities between BCNs and linear time-invariant (LTI) control systems, e.g., smallest invariant dual subspaces of BNs containing a set of Boolean functions in BCNs vs unobservable subspaces of LTI control systems, the forms of quotient systems based on observability decomposition in both types of systems. However, there are essential differences between the two types of systems, e.g., “all plausible definitions of observability in LTI control systems turn out to be equivalent” (by Walter M. Wonham 1985), but there exist nonequivalent definitions of observability in BCNs; the quotient system based on observability decomposition always exists in an LTI control system, while a quotient system based on multiple-experiment observability decomposition does not always exist in a BCN.

Discrete-event systems (DESs) usually consist of discrete states and transitions between them caused by spontaneous occurrences of labeled events. In this review article, we study DESs modeled by labeled (nondeterministic) finite-state automata (LFSAs). Due to the partially-observed feature of DESs, fundamental properties therein can be classified into two categories: state/event-inference-based properties (e.g., strong detectability, diagnosability, and predictability) and state-concealment-based properties (e.g., opacity). Intuitively, the former category describe whether one can use observed output sequences to infer the current and subsequent states, past occurrences of faulty events, or future certain occurrences of faulty events; while the latter describe whether one cannot use observed output sequences to infer whether secret states have been visited (that is, whether the DES can conceal the status that its secret states have been visited). Over the past two decades these properties were studied separately using different methods, and particularly, in most works inference-based properties were verified based on two fundamental assumptions of deadlock-freeness and divergence-freeness, where the former implies that an automaton will always run, the latter implies that an automaton has no reachable unobservable cycle, hence the running of such an automaton will always be eventually observed. In this article, for LFSAs, a unified concurrent-composition method is shown to verify all above inference-based and concealment-based properties, resulting in a unified mathematical framework for the two categories of properties. In addition, compared with the previous methods in the literature, the concurrent-composition method does not depend on assumptions and is currently the most efficient. Finally, based on concurrent composition, we represent the negations of the above inference-based properties as linear temporal logic (LTL) formulae; by combining the concurrent composition and an additional tool called observer (i.e., the classical powerset construction for LFSAs), we also represent the above concealment-based properties as LTL formulae. Although LTL formulae model checking algorithms do not provide more efficient verification for these inference-based and concealment-based properties, the obtained LTL formulae show common similarities among these properties.

Observers are formulated for labeled real-time automata, algorithms are also designed to compute observers for such automata.  The observers of labeled real-time automata provide a natural and nontrivial generalization of Rabin and Scott's powerset consturction of nondeterministic finite automata. Extend the decidability results on all kinds of state-based opacity in labeled finite automata to labeled real-time automata. Will extend plenty of decidable results obtained in the past 30 years in labeled finite automata as discrte-event systems to labeled real-time automata based on the computability results of observers proven in the paper.