Feedback Refinement Relations for the Synthesis of Symbolic Controllers

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 pa...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on automatic control 2017-04, Vol.62 (4), p.1781-1796
Main Authors: Reissig, Gunther, Weber, Alexander, Rungger, Matthias
Format: Article
Language:English
Subjects:
Automated synthesis
Complexity theory
Concrete
Context
Control systems
discrete abstraction
nonlinear system
robust synthesis
Robustness
symbolic control
symbolic model
Uncertainty
Vehicle dynamics
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0018-9286
1558-2523
DOI:10.1109/TAC.2016.2593947