Delta-Decisions over the Reals

VCLA will be hosting a talk by Sicun Gao on September 18th, 2013.

ABSTRACT

Formal reasoning about continuous and hybrid dynamical systems requires solving decision problems for first-order formulas over the real numbers with various nonlinear real functions. Such decision problems are known to be very hard for real arithmetic already, and undecidable when trigonometric functions are also involved. I present positive results for a rich signature with arbitrary Type 2 computable functions instead. The key is to define a notion of numerical errors (delta-perturbations) on logic formulas and consider what we call the "delta-decision problem": decide if a sentence is false, or a delta-perturbation of it is true. We show that under such relaxations, bounded formulas in this rich signature (allowing transcendental functions, differential equations, etc) are delta-decidable within reasonable complexity classes. The results lead to a new framework for the control and analysis of dynamical systems, as well as practical decision procedures that combine the power of numerical and symbolic algorithms. I will demo our solver dReal (http://dreal.cs.cmu.edu) on large benchmarks.