Quantifier-free encoding of invariants for hybrid systems

Hybrid systems are a clean modeling framework for embedded systems, which feature integrated discrete and continuous dynamics. A well-known source of complexity comes from the time invariants, which represent an implicit quan- tication of a constraint over all time points of a continuous transition. Emerging techniques based on Satisability Modulo Theory (SMT) have been found promising for the verication and validation of hybrid systems because they combine discrete reasoning with solvers for rst-order theories. However, these techniques are ecient for quantier-free theories and the current approaches have so far either ignored time invariants or have been limited to hybrid systems with linear constraints. In this paper, we propose a new method that encodes a class of hybrid systems into transition systems with quantier-free formulas. The method does not rely on expensive quantier elimination procedures. Rather, it exploits the sequential nature of the transition system to split the continuous evolution enforcing the invariants on the discrete time points. This way, we can encode all hybrid systems whose invariants can be expressed in terms of polynomial constraints. This pushes the application of SMT-based techniques beyond the standard linear case.