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

摘要

There is a need for controller design methodologies that enable early detection and elimination of unsafe designs. This thesis is about 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; this work is concerned with ways of overcoming the scalability issue. In particular, three techniques for improving scalability are addressed.;Firstly, a specification-guided abstraction-refinement technique with two novel inventions is presented. As opposed to traditional uniform abstractions, this technique creates non-uniform abstractions that are iteratively refined in ''promising'' areas of the state space to create a parsimonious abstraction. The abstraction is also augmented with additional information in the form of progress groups that can encode transience properties of the underlying concrete system. Examples demonstrate that both these novelties can reduce the computational burden significantly.;Secondly, ways to decompose large problems into smaller ones while preserving correctness guarantees are considered. Since synthesis techniques typically scale exponentially with system dimension, decomposition can render otherwise intractable problems tractable. Two techniques for computation of separable invariant sets are presented; one for joint computation via LMIs, and one for iterative localized computation for systems with nonlinear interconnections.;The final part of the thesis presents a way to leverage problem structure in order to provide mathematical correctness guarantees on aggregate behavior for very large collections of systems. In particular, counting problems are introduced, which due to their symmetry admit a novel form of abstraction whose size is a fraction of that of a traditional naive abstraction. The counting problem on the abstraction is solved via ILP optimization.