Sicun (Sean) Gao

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.

Posted in RiSE Seminar