2011/12/11 by Wang Lin, Lin Wang, Lin, Wang +6 · 1 citation
Computer Science · Decision Sciences · Mathematics · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Optimization and Control (math.OC) #Probabilistic and Robust Engineering Design #Risk and Safety Analysis #Software Engineering (cs.SE) #cs.SE #math.OC
paper · pdf · doi:10.48550/arxiv.1112.2328
arxiv created 2011/12/11 · openalex publication_date 2011/12/11 · arxiv updated 2015/03/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is deployed to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.