English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a controller synthesis algorithm for reach-avoid problems forpiecewise linear discrete-time systems. Our algorithm relies on SMT solvers andin this paper we focus on piecewise constant control strategies. Our algorithmgenerates feedback control laws together with inductive proofs of unboundedtime safety and progress properties with respect to the reach-avoid sets. Undera 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 proofof correctness, or it establishes the impossibility of the existence of suchcontrollers. To achieve this, the algorithm iteratively attempts to solve aweakened and strengthened versions of the SMT encoding of the reach-avoidproblem. We present preliminary experimental results on applying this algorithmbased on a prototype implementation.

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