Synthesizing switching logic using constraint solving

Abstract

A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we extend that work to automatic synthesis of safe hybrid systems. Starting with a multi-modal dynamical system and a safety property, we present a sound technique for synthesizing a switching logic for changing modes so as to preserve the safety property. By construction, the synthesized hybrid system is well-formed and is guaranteed safe. Our approach is based on synthesizing a controlled invariant that is sufficient to prove safety. The generation of the controlled invariant is cast as a constraint solving problem. When the system, the safety property, and the controlled invariant are all expressed only using polynomials, the generated constraint is an ∃∀ formula in the theory of reals, which we solve using SMT solvers. The generated controlled invariant is then used to arrive at the maximally liberal switching logic. © 2009 Springer Berlin Heidelberg.