Correct-by-Construction Control Synthesis for High-Dimensional Systems

Abstract:

There is a need for controller design methodologies that enable early detection and elimination of unsafe designs. In this talk I will present work on correct-by-construction synthesis methods—a collection of techniques that provide mathematical guarantees on correct behavior with respect to a formal specification. While these methods have attractive theoretical properties, there are fundamental scalability limitations that inhibit wide adoption; my work is concerned with ways of overcoming the scalability issue.

In the first part of the talk I consider problem decomposition via computation of separable invariant sets. Since synthesis techniques typically scale exponentially with system dimension, decomposition can render otherwise intractable problems tractable. Two techniques for computation of separable invariant sets will be presented; one for joint computation via LMIs, and one for iterative localized computation for systems with nonlinear interconnections. I will present an application of the decomposition technique to autonomous driving.

In the second part I introduce the concept of "counting problems'. This is a novel class of problems that due to symmetry admit a novel form of compact abstraction. A solution to a 20.000-dimensional counting problem from the power systems domain will be presented.