@inproceedings{14530af2ebd94c19aafc794644234da0,
title = "Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm",
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 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.",
keywords = "Control systems, Encoding, Feedback control, Linear systems, Robustness, Safety, Search problems",
author = "Zhenqi Huang and Yu Wang and Sayan Mitra and Dullerud, {Geir E.} and Swarat Chaudhuri",
note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 54th IEEE Conference on Decision and Control, CDC 2015 ; Conference date: 15-12-2015 Through 18-12-2015",
year = "2015",
month = feb,
day = "8",
doi = "10.1109/CDC.2015.7403394",
language = "English (US)",
series = "Proceedings of the IEEE Conference on Decision and Control",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "7434--7439",
booktitle = "54rd IEEE Conference on Decision and Control,CDC 2015",
address = "United States",
}