# Learning Finite Linear Temporal Logic Specifications with a Specialized Neural Operator

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 21 references that are in the map.
- First posted on arXiv 7 Nov 2021.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [Environment-Independent Task Specifications via GLTL](https://mlsanity.com/paper/1704.04341/) (2017)
- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Interpretable Apprenticeship Learning with Temporal Logic Specifications](https://mlsanity.com/paper/1710.10532/) (2017)
- [Temporal and Object Quantification Networks](https://mlsanity.com/paper/2106.05891/) (2021)

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

- [DeepDFA: Automata Learning through Neural Probabilistic Relaxations](https://mlsanity.com/paper/2408.08622/) (2024)
- [Neural Reward Machines](https://mlsanity.com/paper/2408.08677/) (2024)
- [A Neuro-Symbolic Framework for Sequence Classification with Relational and Temporal Knowledge](https://mlsanity.com/paper/2505.05106/) (2025)
- [RNN Generalization to Omega-Regular Languages](https://mlsanity.com/paper/2509.02491/) (2025)
- [Learning Representations Through Contrastive Neural Model Checking](https://mlsanity.com/paper/2510.01853/) (2025)

## Abstract (arXiv)

Finite linear temporal logic (mathsfLTLf) is a powerful formal representation for modeling temporal sequences. We address the problem of learning a compact mathsfLTLf formula from labeled traces of system behavior. We propose a novel neural network operator and evaluate the resulting architecture, NeuralmathsfLTLf. Our approach includes a specialized recurrent filter, designed to subsume mathsfLTLf temporal operators, to learn a highly accurate classifier for traces. Then, it discretizes the activations and extracts the truth table represented by the learned weights. This truth table is converted to symbolic form and returned as the learned formula. Experiments on randomly generated mathsfLTLf formulas show NeuralmathsfLTLf scales to larger formula sizes than existing approaches and maintains high accuracy even in the presence of noise.