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