Synthesis of Universal Safety Controllers

TL;DR

This paper tackles the scalability of reactive controller synthesis when the plant model is large or changes over time. It introduces a universal controller framework in which each controller output is annotated with a prophecy about the plant's behavior, enabling correct-by-construction synthesis from a given temporal specification without enumerating all plant states. Prophecies are captured by tree automata, and safe-prophecy construction yields a universal controller that is correct and most permissive for safety specifications. An on-the-fly composition procedure specializing the universal controller to a particular plant allows scalable adaptation, and experiments with the unicontool prototype demonstrate favorable scalability and practical impact on benchmark scenarios and maze-like robotics tasks.

Abstract

The goal of logical controller synthesis is to automatically compute a control strategy that regulates the discrete, event-driven behavior of a given plant s.t. a temporal logic specification holds over all remaining traces. Standard approaches to this problem construct a two-player game by composing a given complete plant model and the logical specification and applying standard algorithmic techniques to extract a control strategy. However, due to the often enormous state space of a complete plant model, this process can become computationally infeasible. In this paper, we introduce a novel synthesis approach that constructs a universal controller derived solely from the game obtained by the standard translation of the logical specification. The universal controller's moves are annotated with prophecies - predictions about the plant's behavior that ensure the move is safe. By evaluating these prophecies, the universal controller can be adapted to any plant over which the synthesis problem is realizable. This approach offers several key benefits, including enhanced scalability with respect to the plant's size, adaptability to changes in the plant, and improved explainability of the resulting control strategy. We also present encouraging experimental results obtained with our prototype tool, UNICON.