Non-linear Invariants for Control-Command Systems

Control theorists know for long that quadratic invariants, that is ellipsoids, are a good solution to bound the behavior of linear controllers, which constitute the heart of most control-command systems. They designed methods to synthesize such invariants using some convex optimization techniques, namely semidefinite programming solvers. The first part of this talk will briefly introduce those methods.

In practice, these techniques heavily rely on numerical computations performed using floating-point arithmetic, raising stringent soundness questions about their results. We will thus investigate solutions to formally validate such results and see that this is feasible with only a small overhead.

Finally, we present a simple implementation in the Alt-Ergo SMT solver and comparison with other state-of-the-art SMT solvers on non-linear real arithmetic benchmarks. We also introduce an implementation in the Coq proof assistant with a reflexive tactic enabling to automatically discharge polynomial inequalities proofs. Benchmarks indicate that we are able to formally address problems that would otherwise be untractable with other state-of-the-art methods.

[Slides]

Series:
Microsoft Research Talks
Date:
Speakers:
Pierre Roux
Affiliation:
ONERA

Series: Microsoft Research Talks