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

TL;DR

This paper introduces deep learning models, including transformers and Mamba, to generate linear temporal logic formulas from system traces, enhancing specification mining with scalable and efficient methods.

Contribution

It presents novel autoregressive architectures for temporal logic formula generation and a new metric for assessing formula distinctiveness, advancing deep learning applications in specification mining.

Findings

Transformers and Mamba effectively generate correct temporal logic formulas.

Proposed models outperform baselines in computational efficiency.

Generated formulas are both accurate and diverse.

Abstract

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.