Feedback Refinement Relations for the Synthesis of Symbolic Controllers

DOI10.1109/TAC.2016.2593947zbMATH Open1366.93363arXiv1503.03715OpenAlexW3104168345MaRDI QIDQ5282424FDOQ5282424

Authors: Gunther Reißig, A. Weber, Matthias Rungger 

Publication date: 27 July 2017

Published in: IEEE Transactions on Automatic Control (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1503.03715

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Dynamical systems in control (37N35) Discrete event control/observation systems (93C65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (38)

• Data-driven abstraction-based control synthesis
• Finite-step alternating approximately bi-similar symbolic model for Markov jump systems
• Learning-based symbolic abstractions for nonlinear control systems
• Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability
• The refinement calculus of reactive systems
• Robust stutter bisimulation for abstraction and controller synthesis with disturbance
• Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
• 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
• Lazy Abstraction-Based Controller Synthesis
• 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
• Nonlinear model predictive control based on \(K\)-step control invariant sets
• Compositional abstraction refinement for control synthesis
• 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
• 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)