Feedback Refinement Relations for the Synthesis of Symbolic Controllers

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.

This work has been accepted for publication in the IEEE Trans. Automatic Control. v3: Definition VIII.2 corrected; plus minor modifications; accepted version

Cited by in corpus (22)

• Compositional abstraction and safety synthesis using overlapping symbolic models
• TIRA: Toolbox for Interval Reachability Analysis
• Symbolic Optimal Control
• Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems
• Over-approximating reachable tubes of linear time-varying systems
• Optimized State Space Grids for Abstractions
• Robustly Complete Synthesis of Memoryless Controllers for Nonlinear Systems with Reach-and-Stay Specifications
• Context-triggered Abstraction-based Control Design
• Continuous and discrete abstractions for planning, applied to ship docking
• Synthesizing Safety Controllers for Uncertain Linear Systems: A Direct Data-driven Approach
• Compositional abstraction refinement for control synthesis
• Sparsity-Sensitive Finite Abstraction
• A Specification-Guided Framework for Temporal Logic Control of Nonlinear Systems
• Symbolic Abstractions for Nonlinear Control Systems via Feedback Refinement Relation
• Explainable Reactive Synthesis
• The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
• Finite Horizon Discrete Models for Multi-Agent Control Systems with Coupled Dynamics
• Logarithmic Quantization based Symbolic Abstractions for Nonlinear Control Systems
• Interval Reachability Analysis using Second-Order Sensitivity
• SENSE: Abstraction-Based Synthesis of Networked Control Systems
• Approximately Optimal Controllers for Quantitative Two-Phase Reach-Avoid Problems on Nonlinear Systems
• Automatic Generation of Communication Requirements for Enforcing Multi-Agent Safety