Feedback Refinement Relations for the Synthesis of Symbolic Controllers
From MaRDI portal
Publication:5282424
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.
Cited in
(38)- Learning-based symbolic abstractions for nonlinear control systems
- Data-driven abstraction-based control synthesis
- Finite-step alternating approximately bi-similar symbolic model for Markov jump systems
- Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability
- The refinement calculus of reactive systems
- Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
- Robust stutter bisimulation for abstraction and controller synthesis with disturbance
- Compositional construction of abstractions for infinite networks of discrete-time switched systems
- Robustly complete synthesis of sampled-data control for continuous-time nonlinear systems with reach-and-stay objectives
- On distributed symbolic control of interconnected systems under persistency specifications
- Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
- Convergent under-approximations of reachable sets and tubes: a piecewise constant approach
- An improved algorithm for the control synthesis of nonlinear sampled switched systems
- Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions
- Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications
- Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications
- Formal controller synthesis from specifications given by discrete-time hybrid automata
- Symbolic control design of incrementally stable nonlinear systems with dynamic regular language specifications
- Abstraction-based control synthesis using partial information
- Switching controller synthesis for delay hybrid systems under perturbations
- Symbolic abstractions for nonlinear control systems via feedback refinement relation
- Lazy controller synthesis for monotone transition systems and directed safety specifications
- Compositional abstraction refinement for control synthesis
- Nonlinear model predictive control based on \(K\)-step control invariant sets
- Abstraction and control by interconnection of linear systems: a geometric approach
- Towards scalable synthesis of stochastic control systems
- Robust approximate symbolic models for a class of continuous-time uncertain nonlinear systems via a control interface
- Approximately bisimilar symbolic model for switched systems with unstable subsystems
- Refinements of behavioural abstractions for the supervisory control of hybrid systems
- Finite horizon discrete models for multi-agent control systems with coupled dynamics
- Finite abstraction of mixed monotone systems with discrete and continuous inputs
- Lazy abstraction-based controller synthesis
- ABS: A formally correct software tool for space-efficient symbolic synthesis
- BOCoSy: Small but Powerful Symbolic Output-Feedback Control
- OmegaThreads
- Symbolic control for stochastic systems via finite parity games
- Synthesis of event-triggered controllers for SIRS epidemic models
- Optimal multirate sampling in symbolic models for incrementally stable switched systems
This page was built for publication: Feedback Refinement Relations for the Synthesis of Symbolic Controllers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5282424)
