Universal Safety Controllers with Learned Prophecies

Conference: AAAI 2026 arXiv: 2511.11390 Code: UCLearn (uclearn tool) Area: Interpretability Keywords: Universal Safety Controllers, Temporal Logic, CTL Learning, Reactive Synthesis, Prophecy Approximation

TL;DR

This paper proposes UCLearn, which learns CTL (Computation Tree Logic) formulas as approximate representations of prophecies from a small number of representative plant models, replacing exact but computationally expensive tree automata to achieve efficient, scalable, and interpretable universal safety controller synthesis.

Background & Motivation

1. Background: Reactive synthesis and supervisory control aim to automatically construct correct-by-design controllers from temporal logic specifications. Traditional approaches require composing specification automata with concrete plant models, suffering from severe state-space explosion.
2. Limitations of Prior Work: Although the previously proposed Universal Safety Controller (USC) framework enables synthesis independent of the plant, its core component—the prophecy—is represented using tree automata, which incurs prohibitively high computational and verification costs and is difficult to interpret.
3. Key Challenge: USCs must precisely characterize "under what plant behaviors a given control output is correct," yet the exact representation (tree automata) is impractical, while simpler representations may forfeit correctness guarantees.
4. Goal: To find a computationally efficient and human-readable prophecy representation while preserving correctness guarantees.
5. Key Insight: CTL formulas are used in place of tree automata as the representation of prophecies; a learning algorithm infers CTL formulas from a small set of representative plants that can separate correct from incorrect control outputs.
6. Core Idea: Rather than precisely characterizing all possible plant behaviors, it suffices to learn a CTL formula from a small number of samples that adequately separates correct and incorrect control decisions.

Method

Overall Architecture

UCLearn consists of three iterative phases: (1) Initialization—converting the safety LTL specification into a safety automaton and establishing initial approximations (under-approximation = empty set, over-approximation = all plants); (2) Refinement Loop—for each new nominal plant, the current controller is first applied; if incorrect, a correct controller is synthesized, positive/negative samples are updated, and a new CTL formula is learned; (3) Composition—the learned prophecy controller is composed with the concrete plant, the prophecy is verified via CTL model checking, and an explicit controller is extracted.

Key Designs

1. Approximation Framework:

   • Function: Maintains upper and lower approximations of prophecies to ensure correctness and maximal permissiveness.
   • Mechanism: Defines the triple \(\mathcal{W}=(\mathcal{A}, \underline{\kappa}, \overline{\kappa})\), where \(\underline{\kappa}(q,\alpha) \subseteq \kappa(q,\alpha) \subseteq \overline{\kappa}(q,\alpha)\). The under-approximation \(\underline{\kappa}\) guarantees correctness (conservative strategy), while the over-approximation \(\overline{\kappa}\) guarantees maximal permissiveness (no correct plant is excluded).
   • Design Motivation: Exact prophecy computation (\(\kappa\)) is too costly; maintaining upper and lower bounds enables incremental refinement, and the under-approximation is always safe to deploy.

2. Refinement via Game Solving:

   • Function: Updates the upper and lower approximations for each new plant.
   • Mechanism: The specification automaton is composed with the plant into a game graph \(G\), and the winning region \(Win\) is computed. For each state \(q\) and output \(\alpha\): if the sub-plant guarantees entry into a winning state, it is added to \(\underline{\kappa}\); otherwise, it is removed from \(\overline{\kappa}\) (Algorithm 1). Refinement is monotone—only increasing the under-approximation and decreasing the over-approximation.
   • Design Motivation: Interaction with concrete plants yields positive and negative samples, progressively narrowing the uncertainty range of the prophecy.

3. CTL Learning for Prophecies:

   • Function: Converts sets of upper and lower bound samples into concise CTL formulas.
   • Mechanism: Plants in \(\underline{\kappa}\) serve as positive samples and plants in \(\mathbb{P} \setminus \overline{\kappa}\) as negative samples; the learnCTL algorithm is invoked to learn a CTL formula \(\phi\) separating the two classes (Algorithm 2). The resulting \(\phi\) is used as the prophecy annotation: \(\kappa(q,\alpha) = \mathcal{L}(\phi)\).
   • Design Motivation: CTL formulas are concise, human-readable, and efficiently verifiable (polynomial-time model checking), and are expressive enough to capture plant behavior conditions in most practical scenarios.

Loss & Training

This paper does not involve deep learning. The core algorithmic pipeline is as follows: - Initialization: Safety LTL → Deterministic Safety Automaton (LTLtoDSA) - Refinement: Game solving → Winning region → Update upper/lower bounds → CTL learning - Verification: On-the-fly composition (Algorithm 3) + model checking for correctness - Safety Net: The synthesize procedure in Algorithm 4 includes a verification step—if the learned prophecy is insufficient, automatic refinement and re-learning are triggered.

Key Experimental Results

Main Results

Benchmark	Metric	UCLearn	unicon (Exact)	Standard Synthesis	Gain
Grid World (n×n)	Computation time ratio	1x	10–100x	10–100x	>10x speedup
Lily Benchmark	Computation time ratio	1x	~8x	~8x	Up to 8x speedup
SYNTCOMP Safety Benchmark	Adaptability	Very fast	Slower	N/A	Significantly faster adaptation

Ablation Study

Configuration	Key Metric	Description
Learning from a single 2×2 grid	CTL formula size ≤ 2	Generalizes from a minimal plant to larger grids
Composition time comparison	UCLearn << unicon	CTL model checking is much faster than tree automata
Increasing Lily parameters	Linear vs. exponential growth	UCLearn scales significantly better than exact methods

Key Findings

• A CTL formula learned from a single small-scale plant (grid size 2) generalizes to larger grids (formula size ≤ 2), demonstrating strong generalization capability.
• CTL prophecy formulas are concise and human-readable (e.g., the load balancer prophecy: \(\forall \bigcirc (overload \Rightarrow asgn_i)\)).
• On SYNTCOMP benchmarks, UCLearn adapts far more quickly than unicon and standard synthesis, as the cost of reusing CTL formulas is minimal.

Highlights & Insights

• Trading Precision for Efficiency: CTL formulas are less precise than tree automata, but are sufficient in practice—formulas learned from a small number of plants generalize well—while substantially reducing computational cost.
• Interpretable Controllers: CTL prophecies are human-readable temporal logic formulas, enabling users to understand why the controller makes a particular decision.
• Incremental Correctness Guarantees: The under-approximation is always correct; when an uncovered plant is encountered, the system automatically refines and relearns—an elegant anytime algorithm.
• Cross-Plant Generalization: The controller is not tailored to a specific plant but is conditioned via prophecies; adapting to a new plant requires only verifying the CTL formula.

Limitations & Future Work

• CTL is less expressive than tree automata and may fail to find an effective separating formula for some complex plant behaviors.
• Learning quality depends on the representativeness of nominal plants—if the initial plant set is insufficiently diverse, the learned prophecy may not generalize well.
• The framework currently supports only safety LTL specifications; liveness and other temporal properties are not addressed.
• The scalability of the CTL learning algorithm itself remains a potential bottleneck.

Related Work & Insights

• vs. unicon (Exact USC Synthesis): unicon uses tree automata to precisely represent prophecies, which is computationally expensive and uninterpretable; UCLearn approximates with CTL formulas, achieving orders-of-magnitude speedup and interpretability.
• vs. Standard Reactive Synthesis: Standard methods solve each plant independently without reuse; the USC framework enables cross-plant reuse through prophecy conditioning.
• vs. Temporal Logic Learning (Neider et al.): Prior work learns LTL specifications, but applying learned formulas as prophecies within controller synthesis is a novel contribution.

Rating

• Novelty: ⭐⭐⭐⭐⭐ First to introduce learning methods into USC prophecy synthesis; using CTL as a prophecy representation is a genuine innovation.
• Experimental Thoroughness: ⭐⭐⭐⭐ Multiple benchmarks covering scalability and adaptability, though real-world application scenarios are limited.
• Writing Quality: ⭐⭐⭐⭐ Formal definitions are clear, algorithmic pseudocode is complete, and running examples are woven throughout.
• Value: ⭐⭐⭐⭐ Significant theoretical and practical value in the formal methods and controller synthesis communities.

Related Papers

• [ICLR 2026] Universal Properties of Activation Sparsity in Modern Large Language Models
• [ICLR 2026] GAVEL: Towards Rule-Based Safety through Activation Monitoring
• [ICLR 2026] Beyond Linear Probes: Dynamic Safety Monitoring for Language Models
• [CVPR 2026] SafeDrive: Fine-Grained Safety Reasoning for End-to-End Driving in a Sparse World
• [NeurIPS 2025] How Intrinsic Motivation Shapes Learned Representations in Decision Transformers: A Cognitive Interpretability Analysis