Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant  

作　　者：Hui Kong Fei He Xiaoyu Song Ming Gu Hongyan Tan Jiaguang Sun 

机构地区：[1]the School of Software,Tsinghua University [2]the Department of ECE,Portland State University [3]the Institute of Acoustics,Chinese Academy of Sciences

出　　处：《Tsinghua Science and Technology》2014年第2期211-222,共12页清华大学学报（自然科学版（英文版）

基　　金：supported by the National Key Basic Research and Development (973) Program of China (No. 2010CB328003);the National Natural Science Foundation of China (Nos. 61272001,60903030,and 91218302);the National Key Technology Research and Development Program (No. SQ2012BAJY4052);the Tsinghua University Initiative Scientific Research Program

摘　　要：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.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.

关 键 词：inductive invariant semi-algebraic dynamical system safety verification hybrid system nonlinearsystem 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]