Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant

• Published in: Tsinghua science and technology 2014-04, Vol.19 (2), p.211-222
• Main Authors: Kong, Hui, He, Fei, Song, Xiaoyu, Gu, Ming, Tan, Hongyan, Sun, Jiaguang
• Format: Article
• Language: English
• Subjects: 半代数; 安全性; 安全验证; 感应; 计算复杂性; 诱导条件; 量词消去; 非线性动力系统
• ISSN: 1007-0214; 1878-7606; 1007-0214
• DOI: 10.1109/TST.2014.6787375

To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.