CMACS Researchers Developed a New Framework for Verifying Hybrid Systems

The main difficulty with formal verification of hybrid systems, besides that they are already undecidable for unrealistically simple hybrid systems, is that the standard formal verification approaches that have been successful in other domains (such as hardware and software) are hard to apply in this domain. The reason is that almost all scalable modern verification techniques rely on the use of logic solvers (SAT and SMT solvers), while for hybrid systems one needs to reason about logic formulas over the real numbers with nonlinear functions -- such problems are of very high complexity and often undecidable.

In the work of CMACS researchers Sicun Gao, Jeremy Avigad, and Edmund Clarke, from Carnegie Mellon University, a new solution for the core decision problems has been given. To circumvent the theoretically difficult decision problem for logic formulas over the reals, they defined the so-called "delta-decision problems": instead of asking whether a formula is true or false, the delta-decision problem asks whether "a formula is true", or "some delta-variant of it is false". Here, delta is a positive rational number, and a delta-variant of a formula is obtained by perturbing the numerical terms in it with delta-bounded errors. They proved that the delta-decision problem for bounded formulas for very general nonlinear functions (any Type 2 computable function, as studied in Computable Analysis) are decidable, with reasonable complexity bounds. This stands in sharp contrast to the undecidability results. Moreover, delta-decisions can be obtained by numerically-driven decision procedures, in which scalable numerical algorithms can be utilized to their full power. They then apply delta-decidability to formal verification problems for hybrid systems. Using bounded model checking, one can encode bounded reachability of hybrid systems using first-order formulas, such that the delta-decision problem of the formulas correspond to strong correctness guarantees: either a system is absolutely safe up to certain bounds, or that it is unsafe when some numerical perturbation (bounded by delta) is applied to the system. Given that practical systems always need to tolerate numerical errors, such as in measuring input signals, a system that is unsafe under delta-bounded perturbations should indeed be regarded unsafe as long as delta is small enough. Such bounded "delta-reachability" problems are also decidable with reasonable complexity. In all, switching to delta-decisions and delta-reachability leads to a new and positive outlook hybrid systems.

Guided by the new theory, the CMACS group has also implemented numerically-driven decision procedures in their tool dReal, and the hybrid system verification tool dReach (available soon), solving many challenging benchmarks. Further descriptions of this new framework can be found in papers "Delta-Decidability over the Reals", "Delta-Complete Decision Procedures for Satisfiability over the Reals", and Sicun Gao's PhD thesis titled "Computable Analysis, Decision Procedures, and Hybrid Automata: A New Framework for the Formal Verification of Cyber-Physical Systems".