Synthesizing Switching Logic Using ConstraintSolving

摘要

A new approach based on constraint solving techniques wasrecently proposed for verification of hybrid systems. This approach worksby searching for inductive invariants of a given form. In this paper, weextend that work to automatic synthesis of safe hybrid systems. Startingwith a multi-modal dynamical system and a safety property, we presenta sound technique for synthesizing a switching logic for changing modesso as to preserve the safety property. By construction, the synthesizedhybrid system is well-formed and is guaranteed safe. Our approach isbased on synthesizing a controlled invariant that is sufficient to provesafety. The generation of the controlled invariant is cast as a constraintsolving problem. When the system, the safety property, and the con-trolled invariant are all expressed only using polynomials, the generatedconstraint is an 3V formula in the theory of reals, which we solve usingSMT solvers. The generated controlled invariant is then used to arriveat the maximally liberal switching logic.