EDBT 2026 Demo / reviewers in the wild / expert
Kuize Zhang
dblp:12/7347
· DBLP profile ↗
11ranked-venue papers
6as first author
5since 2021 · last 2025
0000-0001-9547-103XORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Applied, interdisciplinary, general and emerging computing · 6 · 3 first-author · 1 since 2021Theory of computation · 3 · 3 first-author · 3 since 2021Artificial intelligence and machine learning · 1Software engineering, systems software and programming languages · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | A Unified Method to Efficiently Verify Opacity of Discrete-Timed Automata
Julian Klein 0001, Kuize Zhang, Sabine Glesner |
ICFEM | 2 |
| 2025 | Human-Simulated Intelligent Walking Control for Biped RobotsabstractBiped robots have received increasing attention due to their human-like mechanical structure and good environmental adaptability. In this paper, a new Human-Simulated Intelligent Walking Control (HIWC) scheme is proposed to solve the stability problem of the most popular proportional differential (PD) control under model inaccuracy and disturbance, and further improve its control performance. Specifically, based on Human-Simulated Intelligent Control (HSIC), HIWC is a hierarchical control structure composed of a foot placement compensation (FPC) strategy at the high-level planning layer, and a multi-mode compensation controller (MCC) at the low-level (execution) layer. In FPC, a foot placement compensation algorithm is proposed to plan and correct the swing foots trajectory in real time. MCC consists of a PD and two adaptive compensation algorithms. MCC under bounded uncertainty is proven to be stable in this paper using the Lyapunov theorem. HIWC was tested and compared with PD and model predictive control (MPC) in three experiments on a physical robot platform for planar walking, push-pull, and uneven-ground walking. Experimental results show that the proposed HIWC is more flexible and accurate in controlling the robot’s movement.Note to Practitioners—This paper builds on the fact that PD controllers cannot be easily proven to be stable and do not provide accurate control for the biped robot walking problem. To address these issues, this paper proposes a novel control scheme namely Human-Simulated Intelligent Walking Control (HIWC) and belonging to the family of Human-Simulated Intelligent Control (HSIC) schemes. The proposed HIWC system has been compared against the model predictive control (MPC) and a proportional differential (PD) controller. The proposed HIWC, unlike PD controllers, is rigorously proven to be stable in the presence of model inaccuracy and disturbance. Furthermore, the experiments carried out on a real-world biped robot demonstrate the superiority of HIWC over PD and MPC in terms of control performance. Xingyang Liu, Haina Rong, Ferrante Neri, Kuize Zhang, Zhangguo Yu, Gexiang Zhang |
IEEE Trans Autom. Sci. Eng. | 4 |
| 2024 | State-based opacity of labeled real-time automata
Kuize Zhang |
Theor. Comput. Sci. | 1 |
| 2024 | Diagnosability of labeled Dp-automataabstractIn this paper, we formulate a notion of diagnosability for labeled weighted automata over a class of dioids which admit both positive and negative numbers as well as vectors. The weights can represent diverse physical meanings such as time elapsing and position deviations. We also develop an original tool called concurrent composition to verify diagnosability for such automata. These results are fundamentally new compared with the existing ones in the literature. In a little more detail, diagnosability is characterized for a labeled weighted automaton A D p over a special dioid D p called progressive , which can represent diverse physical meanings such as time elapsing and position deviations. In a progressive dioid, the canonical order is total, there is at least one eventually dominant element, there is no zero divisor, and the cancellative law is satisfied, where the functionality of an eventually dominant element t is to make every nonzero element a arbitrarily large by multiplying a by t for sufficiently many times. A notion of diagnosability is formulated for A D p . By developing a notion of concurrent composition , a necessary and sufficient condition is given for diagnosability of automaton A D p . It is proven that the problem of computing the concurrent composition for an automaton A Q _ is NP -complete, then the problem of verifying diagnosability of A Q _ is proven to be coNP -complete, where the NP -hardness and coNP -hardness results even hold for deterministic, deadlock-free, and divergence-free automaton A N _ , where Q _ and N _ are the max-plus dioids having elements in Q ∪ { − ∞ } and N ∪ { − ∞ } , respectively. Several extensions of the main results have also been obtained. Kuize Zhang, Jörg Raisch |
Theor. Comput. Sci. | 1 |
| 2021 | A Unified Method to Decentralized State Detection and Fault Diagnosis/prediction of Discrete-event SystemsabstractThe state detection problem and fault diagnosis/prediction problem are fundamental topics in many areas. In this paper, we consider discrete-event systems (DESs) modeled by finite-state automata (FSAs). There exist plenty of results on decentralized versions of the latter problem but there is almost no result for a decentralized version of the former problem. In this paper, we propose a decentralized version of strong detectability called co-detectability which means that if a system satisfies this property, for each generated infinite-length event sequence, in at least one location the current and subsequent states can be determined by observations in the location after a common observation time delay. We prove that the problem of verifying co-detectability of deterministic FSAs is coNP-hard. Moreover, we use a unified concurrent-composition method to give PSPACE verification algorithms for co-detectability, co-diagnosability, and co-predictability of FSAs, without any assumption on or modification of the FSAs under consideration, where co-diagnosability is first studied by [Debouk & Lafortune & Teneketzis 2000], co-predictability is first studied by [Kumar & Takai 2010]. By our proposed unified method, one can see that in order to verify co-detectability, more technical difficulties will be met compared with verifying the other two properties, because in co-detectability, generated outputs are counted, but in the latter two properties, only occurrences of events are counted. For example, when one output was generated, any number of unobservable events could have occurred. PSPACE-hardness of verifying co-diagnosability is already known in the literature. In this paper, we prove PSPACE-hardness of verifying co-predictability. Kuize Zhang |
Fundam. Informaticae | 1 |
| 2020 | Dynamics and control of evolutionary congestion games
Xiaoye Gao, Jinhuan Wang, Kuize Zhang |
Sci. China Inf. Sci. | 3 |
| 2020 | Basis for the quotient space of matrices under equivalence
Kuize Zhang |
Sci. China Inf. Sci. | 1 |
| 2017 | An Application of Invertibility of Boolean Control Networks to the Control of the Mammalian Cell CycleabstractIn Fauré et al. (2006), the dynamics of the core network regulating the mammalian cell cycle is formulated as a Boolean control network (BCN) model consisting of nine proteins as state nodes and a tenth protein (protein CycD) as the control input node. In this model, one of the state nodes, protein Cdc20, plays a central role in the separation of sister chromatids. Hence, if any Cdc20 sequence can be obtained, fully controlling the mammalian cell cycle is feasible. Motivated by this fact, we study whether any Cdc20 sequence can be obtained theoretically. We formulate the foregoing problem as the invertibility of BCNs, that is, whether one can obtain any Cdc20 sequence by designing input (i.e., protein CycD) sequences. We give an algorithm to verify the invertibility of any BCN, and find that the BCN model for the core network regulating the mammalian cell cycle is not invertible, that is, one cannot obtain any Cdc20 sequence. We further present another algorithm to test whether a finite Cdc20 sequence can be generated by the BCN model, which leads to a series of periodic infinite Cdc20 sequences with alternately active and inactive Cdc20 segments. States of these sequences are alternated between the two attractors in the proposed model, which reproduces correctly how a cell exits the cell cycle to enter the quiescent state, or the opposite. Kuize Zhang, Lijun Zhang 0004, Shaoshuai Mou |
IEEE ACM Trans. Comput. Biol. Bioinform. | 1 |
| 2016 | Controllability of probabilistic Boolean control networks with time-variant delays in states
Kuize Zhang, Lijun Zhang 0004 |
Sci. China Inf. Sci. | 1 |
| 2013 | Controllability of time-variant Boolean control networks and its application to Boolean control networks with finite memories
Lijun Zhang 0004, Kuize Zhang |
Sci. China Inf. Sci. | 2 |
| 2013 | Controllability and Observability of Boolean Control Networks With Time-Variant Delays in StatesabstractThis brief investigates the controllability and observability of Boolean control networks with (not necessarily bounded) time-variant delays in states. After a brief introduction to converting a Boolean control network to an equivalent discrete-time bilinear dynamical system via the semi-tensor product of matrices, the system is split into a finite number of subsystems (constructed forest) with no time delays by using the idea of splitting time that is proposed in this brief. Then, the controllability and observability of the system are investigated by verifying any so-called controllability constructed path and any so-called observability constructed paths in the above forest, respectively, which generalize some recent relevant results. Matrix test criteria for the controllability and observability are given. The corresponding control design algorithms based on the controllability theorems are given. We also show that the computing complexity of our algorithm is much less than that of the existing algorithms. Lijun Zhang 0004, Kuize Zhang |
IEEE Trans. Neural Networks Learn. Syst. | 2 |