Universal Safety Controllers with Learned Prophecies

TL;DR

This paper introduces an approximation-based learning approach for Universal Safety Controllers that uses inferred CTL formulas as prophecies, enhancing scalability, interpretability, and generalization to unseen plants.

Contribution

It proposes a novel learning algorithm that approximates prophecies with CTL formulas, improving efficiency and human interpretability over exact automata-based methods.

Findings

Learned prophecies are more compact and interpretable.

The approach generalizes well to unseen plants.

Experimental results confirm improved efficiency and scalability.

Abstract

\emph{Universal Safety Controllers (USCs)} are a promising logical control framework that guarantees the satisfaction of a given temporal safety specification when applied to any realizable plant model. Unlike traditional methods, which synthesize one logical controller over a given detailed plant model, USC synthesis constructs a \emph{generic controller} whose outputs are conditioned by plant behavior, called \emph{prophecies}. Thereby, USCs offer strong generalization and scalability benefits over classical logical controllers. However, the exact computation and verification of prophecies remain computationally challenging. In this paper, we introduce an approximation algorithm for USC synthesis that addresses these limitations via learning. Instead of computing exact prophecies, which reason about sets of trees via automata, we only compute under- and over-approximations from (small) example plants and infer computation tree logic (CTL) formulas as representations of prophecies. The resulting USC generalizes to unseen plants via a verification step and offers improved efficiency and explainability through small and concise CTL prophecies, which remain human-readable and interpretable. Experimental results demonstrate that our learned prophecies remain generalizable, yet are significantly more compact and interpretable than their exact tree automata representations.