Dr Kuize Zhang
Academic and research departments
Nature Inspired Computing and Engineering Research Group, Department of Computer Science.About
Biography
I obtained my PhD degree at Harbin Engineering University, China, 2014. I was an Alexander von Humboldt fellow at Control Systems Group, Technical University of Berlin, Germany from 2020 to 2022, did postdocs at KTH Royal Institute of Technology, Sweden, from 2017 to 2020 as well as at Technical University of Munich, Germany, from 2016 to 2017.
Affiliations and memberships
ResearchResearch interests
Decidability and complexity of fundamental properties (e.g., controllability, observability, invertibility, detectability, diagnosability, opacity) in Boolean control networks and diverse labeled (i.e., partially-observed) discrete-event and hybrid systems, including finite automata, Petri nets, timed automata, real-time automata, weighed automata over monoids, etc., with applications to systems biology and cyber security/privacy, etc.
The observability verification method (called weighted pair graph, later renamed observability graph) in Boolean control networks proposed by me has been widely used since 2015 in the corresponding area.
I recently proposed an open-loop property enforcement framework, which particularly can be implemented in polynomial time in labeled finite automata, remarkably differing from the classical supervisory control framework proposed by Ramadge and Wonham, used over 30 years in a closed-loop manner, which can be realized in finite automata in at least exponential time. Compared with the supervisory control framework, the open-loop framework has better scalability and can be implemented in more systems.
An original technique was developed to compute the basic tool -- observer (i.e., powerset construction) of a labeled real-time automaton, which will extend plenty of results in labeled finite automata obtained in the past 3 decades to labeled real-time automata.
I recently proposed a new model called labeled weighed automata oner monoids, and developed original techniques to compute two basic tools -- concurrent composition and observer (i.e., powerset construction) therein, which will also extend plenty of results in labeled finite automata obtained in the past 3 decades to this new model. Welcome more and more researchers to join in this new research direction.
The powerset construction of finite automata (computable in exponential time) was given by Rabin and Scott in 1959, has become a part of standard computation textbooks for many years. The observers (computable in doubly exponential time) in labeled weighted automata over monoids and labeled real-time automata are direct generalizations of the powerset construction of finite automata, thus, many results based on the powerset construction of finite automata, e.g., verification and synthesis in finite automata, verification and synthesis in hybrid systems (cyber-physical systems) under the framework of formal methods might be extended by changing the core part of finite automata to labeled weighted automata over monoids and labeled real-time automata.
Research interests
Decidability and complexity of fundamental properties (e.g., controllability, observability, invertibility, detectability, diagnosability, opacity) in Boolean control networks and diverse labeled (i.e., partially-observed) discrete-event and hybrid systems, including finite automata, Petri nets, timed automata, real-time automata, weighed automata over monoids, etc., with applications to systems biology and cyber security/privacy, etc.
The observability verification method (called weighted pair graph, later renamed observability graph) in Boolean control networks proposed by me has been widely used since 2015 in the corresponding area.
I recently proposed an open-loop property enforcement framework, which particularly can be implemented in polynomial time in labeled finite automata, remarkably differing from the classical supervisory control framework proposed by Ramadge and Wonham, used over 30 years in a closed-loop manner, which can be realized in finite automata in at least exponential time. Compared with the supervisory control framework, the open-loop framework has better scalability and can be implemented in more systems.
An original technique was developed to compute the basic tool -- observer (i.e., powerset construction) of a labeled real-time automaton, which will extend plenty of results in labeled finite automata obtained in the past 3 decades to labeled real-time automata.
I recently proposed a new model called labeled weighed automata oner monoids, and developed original techniques to compute two basic tools -- concurrent composition and observer (i.e., powerset construction) therein, which will also extend plenty of results in labeled finite automata obtained in the past 3 decades to this new model. Welcome more and more researchers to join in this new research direction.
The powerset construction of finite automata (computable in exponential time) was given by Rabin and Scott in 1959, has become a part of standard computation textbooks for many years. The observers (computable in doubly exponential time) in labeled weighted automata over monoids and labeled real-time automata are direct generalizations of the powerset construction of finite automata, thus, many results based on the powerset construction of finite automata, e.g., verification and synthesis in finite automata, verification and synthesis in hybrid systems (cyber-physical systems) under the framework of formal methods might be extended by changing the core part of finite automata to labeled weighted automata over monoids and labeled real-time automata.
Supervision
Postgraduate research supervision
I am looking for a PhD student. The topic is on verification of fundamental properties in real-time automata and weighted automata (over monoids), with applications to cyber-security. Basic knowledge in theoretical computer science and control theory is required.
Teaching
Mathematics Bootcamp (2022)
Foundations of Computing II (2022/3)
Publications
Highlights
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: an open-loop control theory (OCT) 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 OCT 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 OCT 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 OCT 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 OCT 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) 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 OCT framework has just been finished, and the study in LWAMs has just started.