Synthesis of Universal Safety Controllers

TL;DR

This paper introduces a scalable, adaptable universal safety controller synthesis method based on prophecies, enabling control strategies to be generated from logical specifications without modeling the entire plant.

Contribution

It proposes a novel synthesis approach that constructs a universal controller using prophecies, improving scalability, adaptability, and explainability over traditional methods.

Findings

Enhanced scalability demonstrated in experiments

Controller adapts to different plants effectively

Prototype tool UNICON shows promising results

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.