Feedback Refinement Relations for the Synthesis of Symbolic Controllers
- 22 July 2016
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Automatic Control
- Vol. 62 (4), 1781-1796
- https://doi.org/10.1109/tac.2016.2593947
Abstract
We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation of the designed controllers and, as we prove, are characterized by the existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept introduced in this paper. Our work builds on a general notion of system with set-valued dynamics and possibly non-deterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce the specification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a well-defined sense, and provide a method to efficiently compute canonical abstractions. We demonstrate the practicality of our approach on two examples.Keywords
Other Versions
Funding Information
- German Research Foundation (RE 1249/3-2, RE 1249/4-1)
This publication has 43 references indexed in Scilit:
- Synthesis of Reactive(1) designsJournal of Computer and System Sciences, 2012
- A Theory of Synchronous Relational InterfacesACM Transactions on Programming Languages and Systems, 2011
- Temporal logic motion planning for dynamic robotsAutomatica, 2009
- Reachability and Control Synthesis for Piecewise-Affine Hybrid Systems on SimplicesIEEE Transactions on Automatic Control, 2006
- The Linear Time - Branching Time Spectrum I. The Semantics of Concrete, Sequential ProcessesPublished by Elsevier BV ,2001
- Validated solutions of initial value problems for ordinary differential equationsApplied Mathematics and Computation, 1999
- Hierarchical hybrid control systems: a lattice theoretic formulationIEEE Transactions on Automatic Control, 1998
- Numerical nonlinear regulator designIEEE Transactions on Automatic Control, 1994
- Directed hypergraphs and applicationsDiscrete Applied Mathematics, 1993
- Using branching time temporal logic to synthesize synchronization skeletonsScience of Computer Programming, 1982