Controller Synthesis with Inductive Proofs for Piecewise Linear Systems: an SMT-based Algorithm

TL;DR

This paper introduces an SMT-based algorithm for synthesizing controllers for piecewise linear systems that guarantees safety and progress through inductive proofs, with completeness under certain robustness assumptions.

Contribution

It presents a novel SMT-based approach that synthesizes feedback controllers with inductive safety proofs for reach-avoid problems in piecewise linear systems.

Findings

Algorithm successfully synthesizes controllers with proofs of correctness.

Under robustness assumptions, the method is complete, either finding a controller or proving none exists.

Preliminary experiments demonstrate the approach's feasibility.

Abstract

We present a controller synthesis algorithm for reach-avoid problems for piecewise linear discrete-time systems. Our algorithm relies on SMT solvers and in this paper we focus on piecewise constant control strategies. Our algorithm generates feedback control laws together with inductive proofs of unbounded time safety and progress properties with respect to the reach-avoid sets. Under a reasonable robustness assump- tion, the algorithm is shown to be complete. That is, it either generates a controller of the above type along with a proof of correctness, or it establishes the impossibility of the existence of such controllers. To achieve this, the algorithm iteratively attempts to solve a weakened and strengthened versions of the SMT encoding of the reach-avoid problem. We present preliminary experimental results on applying this algorithm based on a prototype implementation.