Controller Synthesis for Safety and Reachability via Approximate Bisimulation

TL;DR

This paper introduces an abstraction-based method for synthesizing controllers that ensure safety and reachability in systems, providing performance guarantees and applying to switched systems.

Contribution

It presents a novel approach using approximate bisimulation for controller synthesis with correctness guarantees and extends to switched systems.

Findings

Controllers synthesized are close to optimal safety and reachability controllers.

Guarantees provided on the performance of the synthesized controllers.

Method successfully applied to switched systems with recent abstractions.

Abstract

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.