# Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Core SSM architectures for language, one of 10 directions in State-space sequence models (S4, Mamba).
- Builds on 19 of its 44 references that are in the map.
- First posted on arXiv 31 May 2024.

## Placed in

- State-space sequence models (S4, Mamba) / [Core SSM architectures for language](https://mlsanity.com/ssm/core-ssm-architectures-for-language/)

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Mamba: Linear-Time Sequence Modeling with Selective State Spaces](https://mlsanity.com/paper/2312.00752/) (2023)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Efficiently Modeling Long Sequences with Structured State Spaces](https://mlsanity.com/paper/2111.00396/) (2021)
- [Combining Recurrent, Convolutional, and Continuous-time Models with Linear State-Space Layers](https://mlsanity.com/paper/2110.13985/) (2021)
- [Deep Learning for Generic Object Detection: A Survey](https://mlsanity.com/paper/1809.02165/) (2018)
- [Video Mamba Suite: State Space Model as a Versatile Alternative for Video Understanding](https://mlsanity.com/paper/2403.09626/) (2024)
- [Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods](https://mlsanity.com/paper/2008.00097/) (2020)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [On Robustness Metrics for Learning STL Tasks](https://mlsanity.com/paper/2003.06041/) (2020)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [Multi-agent Motion Planning from Signal Temporal Logic Specifications](https://mlsanity.com/paper/2201.05247/) (2022)
- [The Complexity of Learning Linear Temporal Formulas from Examples](https://mlsanity.com/paper/2102.00876/) (2021)
- [Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach](https://mlsanity.com/paper/2104.15083/) (2021)
- [Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic](https://mlsanity.com/paper/2110.06726/) (2021)
- [Mining Environment Assumptions for Cyber-Physical System Models](https://mlsanity.com/paper/2005.08435/) (2020)
- [Automatic Failure Explanation in CPS Models](https://mlsanity.com/paper/1903.12468/) (2019)

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

- [Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers](https://mlsanity.com/paper/2507.07808/) (2025)

## Abstract (arXiv)

Temporal logic is a framework for representing and reasoning about propositions that evolve over time. It is commonly used for specifying requirements in various domains, including hardware and software systems, as well as robotics. Specification mining or formula generation involves extracting temporal logic formulae from system traces and has numerous applications, such as detecting bugs and improving interpretability. Although there has been a surge of deep learning-based methods for temporal logic satisfiability checking in recent years, the specification mining literature has been lagging behind in adopting deep learning methods despite their many advantages, such as scalability. In this paper, we introduce autoregressive models that can generate linear temporal logic formulae from traces, towards addressing the specification mining problem. We propose multiple architectures for this task: transformer encoder-decoder, decoder-only transformer, and Mamba, which is an emerging alternative to transformer models. Additionally, we devise a metric for quantifying the distinctiveness of the generated formulae and a straightforward algorithm to enforce the syntax constraints. Our experiments show that the proposed architectures yield promising results, generating correct and distinct formulae at a fraction of the compute cost needed for the combinatorial baseline.