Reliable Analysis And Verification Of Hybrid Systems Based On Symbolic-Numeric Computation

As a common mathematical model for cyber-physical systems, hybrid systems are dynamical systems that are governed by interacting discrete and continuous dynamics. Complex behaviors of hybrid systems make the analysis and verification of hybrid sys-tems both critical and challenging. Taking advantage of the efficiency of numerical com-putation and the error-free property of symbolic computation, hybrid symbolic-numeric method aims to extend the domain of efficiently solvable problems. In this thesis, we present hybrid symbolic-numeric methods to tackle reliable safety verification, stability analysis and domain of attraction estimation of hybrid systems. The main work is carried out as follows:●We address the problem of reliable safety verification of polynomial hybrid systems and then illustrate that invariant generation can be used to guarantee the safety verification of hybrid systems. A hybrid symbolic-numeric method, based on SOS relaxation, modified Gauss-Newton iteration refinement and reliable verification, is presented to compute exact invariants for safety verification of polynomial hybrid systems.●We consider the problem of reliable safety verification of uncertain polynomial hy-brid systems. For ease of presentation, two different representations of uncertainty are proposed, that is, parametric hybrid systems and interval hybrid systems. Then we transform the problem of safety verification to the problem of robust invariant generation, and present two different reliable verification algorithms to generate ex-act robust invariants for safety verification of parametric polynomial hybrid systems and interval polynomial hybrid systems.●We discuss the problem of reliable safety verification of non-polynomial hybrid sys-tems. We first transform the problem of safety verification to the problem of invari-ant generation. Given non-polynomail hybrid systems, polynomial interpolation or Chebyshev-Pade approximation method is applicable to obtain their associated uncertain polynomail hybrid systems or uncertain rational hybrid systems, which include the orginal non-polynomial ones. Similarly, the above hybrid symbolic-numeric method can be empolyed to generate exact invariants for safety verifica-tion.●We extend the presented symbolic-numeric method to stability analysis and domain of attraction estimation of nonlinear hybrid systems. We first give the notions of equilibrium, stability and domain of attraction of hybrid systems. Then we reduce the problems of stability analysis and domain of attraction estimation to the problem of constructing Lyapunov functions, and apply the suggested method, such as SOS relaxation, modified Gauss-Newton iteration refinement, interval certification and function approximation, to compute exact Lyapunov functions for stability analysis and domain of attraction estimation.●We develop an automated verification tool HSProver. It has friendly interface for consumers, easy to operate, and can be used for safety verification of polynomial hybrid systems and uncertain polynomial hybrid systems.