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

Zhenqi Huang, Yu Wang, Sayan Mitra, Geir E. Dullerud, Swarat Chaudhuri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication54rd IEEE Conference on Decision and Control,CDC 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages7434-7439
Number of pages6
ISBN (Electronic)9781479978861
DOIs
StatePublished - Feb 8 2015
Event54th IEEE Conference on Decision and Control, CDC 2015 - Osaka, Japan
Duration: Dec 15 2015Dec 18 2015

Publication series

NameProceedings of the IEEE Conference on Decision and Control
Volume54rd IEEE Conference on Decision and Control,CDC 2015
ISSN (Print)0743-1546

Other

Other54th IEEE Conference on Decision and Control, CDC 2015
CountryJapan
CityOsaka
Period12/15/1512/18/15

Keywords

  • Control systems
  • Encoding
  • Feedback control
  • Linear systems
  • Robustness
  • Safety
  • Search problems

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Modeling and Simulation
  • Control and Optimization

Fingerprint Dive into the research topics of 'Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm'. Together they form a unique fingerprint.

Cite this