Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant

Authors

• Hui Kong, Tsinghua University, Beijing
• Fei He, Tsinghua University, Beijing
• Xiaoyu Song, Portland State UniversityFollow
• Ming Gu, Tsinghua University
• Hongyan Tan, Chinese Academy of Sciences, Beijing
• Jiaguang Sun, Tsinghua University, Beijing

Sponsor

This work was 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), and the Tsinghua University Initiative Scientific Research Program.

Published In

Tsinghua Science and Technology

Document Type

Article

Publication Date

6-30-2014

Subjects

Inductive invariant, Semi-algebraic, dynamical system; safety verification; hybrid systemnonlinear system

Abstract

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.

Rights

Copyright (c) 2026 The Authors

This work is licensed under a Creative Commons Attribution 4.0 International License.

Locate the Document

10.1109/TST.2014.6787375

DOI

10.1109/TST.2014.6787375

Persistent Identifier

https://archives.pdx.edu/ds/psu/44942

Citation Details

Kong, H., He, F., Song, X., Gu, M., Tan, H., & Sun, J. (2014). Safety verification of semi-algebraic dynamical systems via inductive invariant. Tsinghua Science and Technology, 19(2), 211–222. https://doi.org/10.1109/tst.2014.6787375