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

TL;DR

The paper tackles the problem of mining linear temporal logic ($LTL$) formulae from symbolic traces, a task known to be $NP$-hard, by reframing it as an autoregressive trace-to-$LTL$ generation problem. It investigates three neural architectures—Transformer encoder-decoder, decoder-only Mamba, and a Llama-based decoder—to produce semantically correct, syntactically valid, and distinctive $LTL$ formulas, aided by a hand-crafted Polish notation tokenizer and a syntax-enforcing mechanism. A distinctiveness metric is introduced to discourage trivial formulas and quantify how uniquely a predicted formula describes a given trace. Empirical results on an adapted $DeepLTL$ dataset show that the proposed models, particularly Mamba, achieve high semantic accuracy with substantially lower compute time than combinatorial baselines, while maintaining high distinctiveness, highlighting the practical potential for scalable specification mining and improved interpretability of system traces.

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.

Figures (15)

• Figure 1: The overview of the problem. The table on the left denotes the input trace and shows how propositions evolve over time. On the right, a possible output is shown, which is a linear temporal logic (LTL) formula satisfied by the input trace. In this example, the formula dictates that the motor will start in the next time step, and the cargo will be carried until reaching the destination.
• Figure 2: The visual summary of the proposed method. The input symbolic trace is converted into the prefix notation and then tokenized (Top). The model generates the formula tokens autoregressively, enforcing the syntax constraints if desired (Middle). The generated tokens are decoded and converted into the usual infix notation (Bottom).
• Figure 3: Model architectures, displaying the inner workings of the "Neural Network Model" block in Figure \ref{['fig:summary']}. The transformer encoder-decoder model processes the tokens separately, using cross-attention mechanism to process the interactions between them (Top). In Mamba architecture, the input tokens and the generated tokens are concatenated in a single grammar (Bottom).
• Figure 4: Execution times of the combinatorial algorithm with various operator count limits and our models. The optional distinctiveness computation checks each formula against 1000 traces to find the formula with best distinctiveness.
• Figure 5: The distinctiveness distribution of the Mamba's predictions (blue) and the average/best (orange/green) of all formulae up to 4 operators.