Source-linked AI summary
Controller Synthesis for Safety and Reachability via Approximate Bisimulation
Antoine Girard
TL;DR
Safety synthesis seeks permissive controllers that keep outputs safe, while reachability synthesis seeks controllers that reach a target safely in minimum time. This paper synthesizes controllers on approximately bisimilar abstractions and concretizes them for the original system, providing performance estimates and demonstrating the approach on a switched system.
Problem
Safety and reachability controller synthesis must address safe behavior and, for reachability, time to target; the paper focuses on these problems using approximately bisimilar abstractions.
Source: §1 · p. 1Method
The paper synthesizes controllers for approximately bisimilar abstractions and uses problem-specific concretization to obtain controllers for the concrete system.
Source: §1 · pp. 1–2Results
The concretized controllers are correct by design, with estimated distance to maximal safety or time-optimal reachability controllers; the approach is illustrated on switched-system synthesis.
Source: §1 · p. 2, §6 · p. 11Takeaways & Limitations
The techniques apply to any approximately bisimilar abstraction, and the paper demonstrates them for switched-system controller synthesis.
Source: §6 · p. 11The safety-controller comparison is conditioned on a robustness assumption.
Source: §3.2 · p. 6
Abstract
from arXiv · showhide
In this paper, we consider the problem of controller design using approximately bisimilar abstractions with an emphasis on safety and reachability specifications. We propose abstraction-based approaches to solve both classes of problems. We start by synthesizing a controller for an approximately bisimilar abstraction. Then, using a concretization procedure, we obtain a controller for our initial system that is proved "correct by design". We provide guarantees of performance by giving estimates of the distance of the synthesized controller to the maximal (i.e the most permissive) safety controller or to the time-optimal reachability controller. Finally, we use the presented techniques combined with discrete approximately bisimilar abstractions of switched systems developed recently, for switching controller synthesis.
1. Introduction
The paper uses approximately bisimilar abstractions to synthesize safety and reachability controllers, then concretizes them for the original system with performance estimates. It situates this approach against prior abstraction-based controller work and illustrates it for switched systems.
1. Introduction
- Strict equality of observed behaviors can be too restrictive for continuous or hybrid systems, while approximate bisimulation has extended the class admitting discrete abstractions.Discrete abstractions can support synthesis using supervisory-control or algorithmic-game-theory techniques, and formal behavioral relations reduce the need for verification.Source: §1 · p. 1
- The approach synthesizes controllers on an approximately bisimilar abstraction, then concretizes them for the original system with correct-by-design guarantees and estimates of distance to maximal safety or time-optimal reachability controllers.The paper also applies the techniques to switching controller synthesis using discrete approximately bisimilar abstractions of switched systems.Source: §1 · pp. 1–2
- Unlike prior fixed-bounded-horizon work, this paper considers variable-horizon time-optimal reachability; it also presents a specific approximately bisimilar-abstraction approach for safety.The authors identify their safety approach as the first specific one using approximately bisimilar abstractions.Source: §1 · p. 2
2. Preliminaries
The preliminaries establish transition systems as a common framework for discrete, continuous, and hybrid systems, and define the approximate-bisimulation relationship used for abstraction-based synthesis. They also motivate specific controller concretization procedures by identifying drawbacks of a general procedure.
2. Preliminaries
- A transition system comprises states, actions, transitions, observations, and an output map; it is discrete when its states and actions are finite or countable, and metric when observations carry a metric.The framework is introduced for discrete, continuous, and hybrid systems.Source: §2 · p. 2
- A trajectory is a sequence of states and actions following enabled transitions, and its associated observed behavior is the sequence of state outputs.A state with no enabled actions is blocking; a system is non-blocking when every state is non-blocking.Source: §2 · p. 2
- Controllers are static state-feedback maps from states to enabled actions; the controlled system retains only transitions permitted by the controller.A state is blocking in the controlled system when the controller permits no actions.Source: §2 · pp. 2–3
- Approximate bisimulation relates systems with the same actions and metrically close observations while matching transitions in both directions; an abstraction is a simpler system approximately bisimilar to the controlled system.The paper assumes matching transitions share the same input, noting that this can be relaxed using alternating approximate bisimulation.Source: §2 · p. 3
- A general concretization procedure can produce dynamic state-feedback controllers, require encoding abstraction dynamics, and provide essentially no feedback for deterministic abstractions.The paper presents specific safety and reachability concretization procedures intended to avoid these drawbacks.Source: §2 · p. 3
3. Controller Synthesis for Safety Specifications
Safety synthesis seeks to keep outputs in a specified safe set while preserving nonblocking evolution. The paper synthesizes on an approximately bisimilar abstraction, concretizes the controller for the original system, and estimates its distance from maximality.
3.1. Problem Formulation.
- A safety controller keeps outputs in the safe set and trajectories nonblocking; maximality favors enabling as many actions as possible.A fixed-point algorithm computes the maximal controller and is guaranteed to terminate when the safe-state set is finite; abstraction-based synthesis can help when termination is not guaranteed.Source: §3.1 · p. 4
3.2. Abstraction-based Controller Synthesis.
- Synthesis first computes a controller for abstraction T2 under the ε-contracted safe set, then concretizes it to obtain a well-defined safety controller for concrete system T1.Theorem 3.6 establishes that the resulting controller is safe for the original specification.Source: §3.2 · p. 5
- The concretized controller S1 is bounded between safety controllers derived from contracted and expanded specifications, and computing S1 and S1,E2ε gives a certified upper bound on its distance to the maximal safety controller.If the problem is robust, the synthesized controller approaches the maximal one as ε decreases.Source: §3.2 · pp. 5–6
4. Controller Synthesis for Reachability Specifications
The section formulates safe, time-optimal reachability and synthesizes concrete-system controllers from approximately bisimilar abstractions. Concretization yields performance bounds, including estimates of distance to time optimality.
4.1. Problem Formulation.
- Reachability synthesis seeks to reach the target while remaining safe, minimizing time; entry time is the worst-case number of steps needed to reach the target safely.A time-optimal controller minimizes entry time across controllers and states.Source: §4.1 · pp. 6–7
- Dynamic programming computes a time-optimal controller and terminates in finitely many steps when the safe-state set is finite, but termination is not guaranteed otherwise.An abstraction-based approach may instead produce a suboptimal controller with an estimate of its distance to optimality.Source: §4.1 · p. 7
4.2. Abstraction-based Controller Synthesis.
- For each concrete state, the method selects an approximately bisimilar abstract state with minimum entry time, then uses its abstract controller actions to define the concrete controller.The abstraction uses contracted safe and target sets; the resulting controller is well-defined and satisfies the entry-time bound.Source: §4.2 · pp. 7, 9
- The concrete controller's entry time is bounded by the abstract controller's value, while paired controllers bound performance relative to the concrete system's time-optimal value.For robust reachability problems, the distance to optimality can be approximated arbitrarily closely.Source: §4.2 · pp. 8–9
5. Application to Switching Controller Design
The paper applies its abstraction-based synthesis to a switched system, using approximately bisimilar discrete abstractions to construct safety and reachability controllers. The examples verify the specifications and report bounds and synthesis iterations.
Application to Switching Controller Design
- The switched-system model samples trajectories every τ and admits arbitrary-precision approximately bisimilar discrete abstractions under incremental stability.The approximate bisimulation relation can be characterized by a Lyapunov function proving incremental stability.Source: §5 · p. 10
- The approach applies only to incrementally stable systems; the reachability example uses safe set [0.65, 1.65] × [4.95, 5.95] and target set [1.1, 1.6] × [5.4, 5.9].For that example, the sampling parameter is τ = 0.5.Source: §5 · p. 10
- 2 iterations produced a safety controller for the converter that met the specification, and 4 iterations produced a controller that upper-bounds the maximal safety controller.The safety abstraction used precision ε = 0.05 and τ = 1.Source: §5 · p. 10
- For the switched system, dynamic programming terminated after 94 iterations, yielding a suboptimal controller that meets the reachability specification; its entry time upper-bounds the time-optimal value, while another controller gives a lower bound.The fixed-point algorithm for computing the maximal safety controller terminated in 66 iterations.Source: §5 · p. 11
6. Conclusion
The paper closes with an abstraction-based methodology for safety and reachability controller synthesis, performance guarantees, and a switched-system demonstration. The approach is stated to apply to any approximately bisimilar abstraction.
6. Conclusion
- The methodology computes safety and reachability controllers from approximately bisimilar discrete abstractions and estimates their distance from maximal-safety or time-optimal controllers.Source: §6 · p. 11
- The methodology is demonstrated by synthesizing controllers for a switched system.Figure 2 shows the suboptimal controller and trajectories of the controlled switched system.Source: §6 · p. 11, Figure 2 · p. 12
- The techniques are independent of abstraction type when it is approximately bisimilar; richer specifications and other optimal-control problems are future work.Source: §6 · p. 11
- For the switched-system reachability example, the plotted entry-time functions bound the time-optimal value between the synthesized controller's lower- and upper-bound values.Source: §6 · p. 11, Figure 3 · p. 12