Affiliations and memberships

IEEE / Senior Member


Research interests




1. My monograph entitled A New Framework for Discrete-Event Systems has been published in Foundations and Trends® in Systems and Control (https://www.nowpublishers.com/article/Details/SYS-028)

The monograph mainly contains two contributions: a new theory (NEWT) framework for verifying and enforcing properties in discrete-event systems (DESs) and a new class of automata - labeled weighted automata over monoids (LWAMs).

Real-world problems are often formulated as diverse properties of different types of dynamical systems, so property verification and synthesis/enforcement are long-standing research interests in different areas. 

Ramadge and Wonham's closed-loop supervisory control theory (SCT) framework (1987) for enforcing properties in DESs led the development of DESs in the past 3 decades. Compared with the SCT, my NEWT has better scalability and wider implementability. Therefore, the theoretical framework and applied areas of DESs will must be largely extended. The SCT cannot be implemented in polynomial time, because its implementation is EXPTIME-hard, while my NEWT can be implemented in polynomial time for polynomially verifiable properties. Hence my framework has better scalability. Currently it is known that the SCT can only be fully implemented on finite automata, while my NEWT can be fully implemented on decidable properties of partially-observed systems with finitely many events, e.g., labeled Petri nets and labeled timed automata. Hence my NEWT can be implemented in much more systems.

The LWAMs provide a natural generalization of finite automata in the sense that each transition carries a weight from a monoid, and the weight of a run is the product of the weights of its transitions. Weights have diverse physical meanings such as time consumptions and position deviations, so the LWAMs have much more applications compared with finite automata. Furthermore, by developing original computing techniques, I proved that two basic tools -- concurrent composition and observer (a nontrivial extension of Rabin and Scott's powerset construction for nondeterministic finite automata, 1959, 1976 Turing Award) are computable for labeled weighted automata over the monoid of rational vectors with + operator, thus, plenty of results obtained in finite automata in the past 3 decades can be extended to this new class of automata. 

The NEW framework has just been finished, and the study in LWAMs has just started. 

2. We are organizing a pre-conference workshop entitled "Semi-Tensor Product of Matrices and Its Applications" at the 62nd IEEE Conference on Decision and Control, Dec. 13-15, 2023, Singapore. Please refer to https://cdc2023.ieeecss.org/workshops/ and register our workshop if being interested. 

K. Zhang and J. Raisch (2021) Diagnosability of labeled weighted automata over the monoid $(\mathbb{Q}_{\ge0},+,0)$. In the 60th IEEE Conference on Decision and Control, Austin, Texas, USA, December 13-15 2021.
L. Zhang and K. Zhang (2013) Controllability and observability of Boolean control networks with time-variant delays in states. IEEE Transactions on Neural Networks and Learning Systems, 24(9), 1478-1484, 2013.
K. Zhang (2022) How attacks affect detectability in discrete-event systems? 2022 American Control Conference, July 8-10, 2022, Atlanta, USA, accepted.
W. Dong, X. Yin, K. Zhang, S. Li (2022) On the verification of detectability for timed systems. 2022 American Control Conference, July 8-10, 2022, Atlanta, USA, accepted.
X. Han, K. Zhang, Z. Li. (2022) Verification of strong K-step opacity for discrete-event systems, accepted, the 61st IEEE Conference on Decision and Control, December 6–9, 2022, in Cancún, Mexico.
K. Zhang (2023) A survey on observability of Boolean control networks, accepted, Control Theory and Technology, 33 pages

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.

K. Zhang (2023) A unified concurrent-composition method to state/event inference and concealment in labeled finite-state automata as discrete-event systems

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.

K. Zhang (2024) State-based opacity of labeled real-time automata, accepted, Theoretical Computer Science

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.