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