**Date: **
15:00,
Wednesday, September 18, 2013

**Speaker: **
Sicun Gao

**Venue: **TU Wien

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.