Controller synthesis for linear system with reach-avoid specifications

Chuchu Fan, Zengyi Qin, Umang Mathur, Qiang Ning, Sayan Mitra, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review


We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Our solution decomposes the overall synthesis problem into two smaller, and more tractable problems: one synthesis problem for an open-loop controller which can produce a reference trajectory, and a second for synthesizing a tracking controller, which can enforce the other trajectories to follow the reference trajectory. As a key building-block result, we show that these two controllers can be synthesized independently. Moreover, we are able to reduce the problem of synthesizing open-loop controllers to satisfiability problems over quantifier-free linear real arithmetic, with the number of constraints linear to the number of hyperplanes as the surfaces of the polytopic obstacles and goal sets. The overall synthesis algorithm computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We implement this synthesis algorithm in a tool and show promising results on several benchmarks with up to 20

Original languageEnglish (US)
JournalIEEE Transactions on Automatic Control
StateAccepted/In press - 2021


  • Benchmark testing
  • Computational modeling
  • Control systems
  • Controller syntheis
  • disturbance
  • Ellipsoids
  • Encoding
  • linear system
  • Linear systems
  • reach-avoid specification
  • Trajectory

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Computer Science Applications
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Controller synthesis for linear system with reach-avoid specifications'. Together they form a unique fingerprint.

Cite this