Synthesizing Switching Logic using Constraint Solving
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, which is solved
using SMT solvers. The generated controlled invariant
is then used to arrive at the maximally liberal switching