# Learning Linear Temporal Specifications from Demonstrations with Uncertainty

arXiv: https://arxiv.org/abs/2607.10918 · HTML: https://mlsanity.com/paper/2607.10918/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 24 references that are in the map.
- First posted on arXiv 12 Jul 2026.

## Builds on (most cited first, 9 of 9)

- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Learning from Demonstrations using Signal Temporal Logic](https://mlsanity.com/paper/2102.07730/) (2021)
- [Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis](https://mlsanity.com/paper/2107.07116/) (2021)
- [Optimization Modulo Theories with Linear Rational Costs](https://mlsanity.com/paper/1410.6039/) (2014)
- [Constrained LTL Specification Learning from Examples](https://mlsanity.com/paper/2412.02905/) (2024)
- [Learning Temporal Logic Properties: an Overview of Two Recent Methods](https://mlsanity.com/paper/2212.00916/) (2022)
- [Learning Temporal Properties is NP-hard](https://mlsanity.com/paper/2312.11403/) (2023)
- [A Direct Translation from LTL with Past to Deterministic Rabin Automata](https://mlsanity.com/paper/2405.01178/) (2024)
- [The Complexity of Learning Temporal Properties](https://mlsanity.com/paper/2408.04486/) (2024)

## Abstract (arXiv)

Learning temporal logic specifications from system demonstrations is essential for tasks such as formal verification and controller synthesis, especially in safety-critical domains. Existing approaches typically assume demonstrations are correct or only affected by misclassification errors. In practice, however, system traces are often uncertain or incomplete due to sensor faults, measurement errors, or data loss. We present a framework for learning minimal Linear Temporal Logic (LTL) formulas from demonstrations with uncertainty. Our approach models uncertainty via Hamming distance to generate possible estimates around each observed trace, which are grouped with constraints requiring that at least one trace per group is consistent with the learned formula. Our problem is then reduced to an equivalent Pseudo-Boolean Optimization. We evaluate our method against state-of-the-art LTL learning approaches and show that it recovers specifications that more closely align with ground-truth formulas under uncertainty.