Sciweavers

Share
CDC
2015
IEEE

Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm

4 years 9 months ago
Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm
— 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 assumption, 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.
Zhenqi Huang, Yu Wang, Sayan Mitra, Geir E. Duller
Added 18 Apr 2016
Updated 18 Apr 2016
Type Journal
Year 2015
Where CDC
Authors Zhenqi Huang, Yu Wang, Sayan Mitra, Geir E. Dullerud, Swarat Chaudhuri
Comments (0)
books