Universal Safety Controllers with Learned Prophecies
Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak, Anne-Kathrin Schmuck
TL;DR
The paper addresses scalability in temporal-safety controller synthesis by introducing Universal Safety Controllers (USCs) that leverage prophecies conditioned on plant behavior. It replaces costly tree-automata prophecies with compact, learnable CTL formulas to form approximate USCs, enabling learning from a small set of nominal plants and verification on unseen plants. The approach uses under- and over-approximations of prophecies and a refinement loop driven by plant observations, with on-the-fly composition and CTL-based learning (learnCTL) to produce correct controllers efficiently. Experimental results on grid-world and lily benchmarks show that learned CTL prophecies are compact, human-readable, and can substantially outperform automata-based USC methods in scalability and adaptability, while maintaining safety guarantees. Overall, the method delivers scalable, interpretable universal control for safety specifications by combining learning, formal verification, and refinement.
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.