# Learning Probabilistic Temporal Logic Specifications for Stochastic Systems

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 44 references that are in the map.
- First posted on arXiv 17 May 2025.

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

- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Reinforcement learning](https://mlsanity.com/paper/2405.10369/) (2024)
- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Generation of Policy-Level Explanations for Reinforcement Learning](https://mlsanity.com/paper/1905.12044/) (2019)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [Interpretable Classification of Time-Series Data using Efficient Enumerative Techniques](https://mlsanity.com/paper/1907.10265/) (2019)
- [Sample Efficient Model-free Reinforcement Learning from LTL Specifications with Optimality Guarantees](https://mlsanity.com/paper/2305.01381/) (2023)
- [Re-understanding Finite-State Representations of Recurrent Policy Networks](https://mlsanity.com/paper/2006.03745/) (2020)
- [Learning Interpretable Temporal Properties from Positive Examples Only](https://mlsanity.com/paper/2209.02650/) (2022)
- [A Robust Genetic Algorithm for Learning Temporal Specifications from Data](https://mlsanity.com/paper/1711.06202/) (2017)
- [Learning Interpretable Models in the Property Specification Language](https://mlsanity.com/paper/2002.03668/) (2020)
- [Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic](https://mlsanity.com/paper/2110.06726/) (2021)
- [Explainable Multi-Agent Reinforcement Learning for Temporal Queries](https://mlsanity.com/paper/2305.10378/) (2023)
- [LTL learning on GPUs](https://mlsanity.com/paper/2402.12373/) (2024)
- [Differentiable Inference of Temporal Logic Formulas](https://mlsanity.com/paper/2208.05440/) (2022)
- [SAT-based Learning of Computation Tree Logic](https://mlsanity.com/paper/2402.06366/) (2024)
- [Learning Branching-Time Properties in CTL and ATL via Constraint Solving](https://mlsanity.com/paper/2406.19890/) (2024)

## Built on by (most cited first, 2 of 2)

- [LTLf Learning Meets Boolean Set Cover](https://mlsanity.com/paper/2509.24616/) (2025)
- [SpecRLBench: A Benchmark for Generalization in Specification-Guided Reinforcement Learning](https://mlsanity.com/paper/2604.24729/) (2026)

## Abstract (arXiv)

There has been substantial progress in the inference of formal behavioural specifications from sample trajectories, for example, using Linear Temporal Logic (LTL). However, these techniques cannot handle specifications that correctly characterise systems with stochastic behaviour, which occur commonly in reinforcement learning and formal verification. We consider the passive learning problem of inferring a Boolean combination of probabilistic LTL (PLTL) formulas from a set of Markov chains, classified as either positive or negative. We propose a novel learning algorithm that infers concise PLTL specifications, leveraging grammar-based enumeration, search heuristics, probabilistic model checking and Boolean set-cover procedures. We demonstrate the effectiveness of our algorithm in two use cases: learning from policies induced by RL algorithms and learning from variants of a probabilistic model. In both cases, our method automatically and efficiently extracts PLTL specifications that succinctly characterise the temporal differences between the policies or model variants.