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 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 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 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 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.