Büchi automata (BAs) recognize -regular languages defined by formal specifications like linear temporal logic (LTL) and are commonly used in the verification of reactive systems. However, BAs face scalability challenges when handling and manipulating complex system behaviors. As neural networks are increasingly used to address these scalability challenges in areas like model checking, investigating their ability to generalize beyond training data becomes necessary. This work presents the first study investigating whether recurrent neural networks (RNNs) can generalize to -regular languages derived from LTL formulas. We train RNNs on ultimately periodic -word sequences to replicate target BA behavior and evaluate how well they generalize to out-of-distribution sequences. Through experiments on LTL formulas corresponding to deterministic automata of varying structural complexity, from 3 to over 100 states, we show that RNNs achieve high accuracy on their target -regular languages when evaluated on sequences up to 8× longer than training examples, with 92.6% of tasks achieving perfect or near-perfect generalization. These results establish the feasibility of neural approaches for learning complex -regular languages, suggesting their potential as components in neurosymbolic verification methods.
Linear Temporal Logic (LTL) [
While BAs provide exact solutions, they can become computationally expensive to handle and
manipulate when representing complex behaviors. Recently, neurosymbolic methods have been used in
verification contexts such as model checking [
Extending the existing work on regular language generalization to -regular languages requires
handling two practical challenges: (1) encoding: representing infinite sequences with finite-length
sequences; (2) labeling sequences: computing acceptance labels for large batches of sequences. While
ifnite automata accept a word when it terminates in an accepting state, BAs require -words to traverse
accepting states infinitely often, meaning RNNs must learn to recognize eventually periodic behavior
instead of just reaching an accepting state. We address challenge (1) by using ultimately periodic (UP)
-words, which uniquely characterize their -regular languages [
While existing model checking tools like Spot [
This work establishes the feasibility of RNNs generalizing to the recognition of -regular languages
while identifying challenges for future research. Our investigation complements ongoing
neurosymbolic advances in verification, for example, neural certificates for model checking [
The main contributions of this work are: • We present the first empirical evidence that RNNs achieve high accuracy on -regular languages when evaluated at lengths up to 8× longer than the sequences in their training distribution.1 • We provide an analysis of RNN generalization, showing that generalization is not limited to toy -regular languages and is robust across DBAs with over 100 states. We also show that the model complexity is correlated with the complexity of the BA recognizing the -regular language.
Practical training of RNNs on -regular languages requires a finite representation of -words and an
eficient method for computing acceptance labels for generated sequences given the infinite acceptance
condition of BAs. Our approach resolves the finite encoding problem by only using UP -words of an
-regular language, , where is a finite prefix and is an infinitely repeating sufix; these -words
uniquely characterize the language [
Importantly, the encoding $ establishes a bijection between UP -words in the target -regular
language and words in a derived regular language. The DBA can be algorithmically reconstructed from
1Code available at: https://github.com/pertcj/omega-generalization
the finite automaton recognizing this regular language [
To determine the label of a $ sequence, we simulate DBA behavior. Simulating the finite prefix yields the state in which terminates. For the sufix , we compute the state transition matrix induced by reading and use matrix exponentiation to determine reachability. The sequence is accepted if repeated application of can reach a cycle containing an accepting state.
We illustrate how we sample $ sequences with fixed length from a DBA. We first sample the position of $ uniformly between 1 and − 1 and then sample with length − 1 and with length − . We sample and by uniformly sampling valid paths in the DBA. Many DBAs exhibit strong acceptance biases that skew random sampling toward rejection or acceptance. For example, the presence of accepting or rejecting sink states (states that can only transition back to themselves) can dominate uniform sampling. We address this through targeted sampling strategies to improve the balance of our sampled sequences: (1) we oversample sequences, determine their labels, and selectively filter them, targeting a balanced class distribution; (2) when sampling accepted sequences, we exclude transitions to rejecting sink states during sampling (and vice versa for rejected sequences); (3) when sampling rejected sequences, we prevent transitions to accepting states within the sufix because if contains a state transition to an accepting state, the resulting -word is likely to be accepted. It is still possible to sample equivalent rejected sequences as this constraint is not applied to . By controlling the sampling of accepted and rejected sequences separately, the resulting dataset is more balanced compared to uniform sampling of sequences.
Our experiments aim to answer the following research questions:
RQ1: Can RNNs generalize to the recognition of sequences from -regular languages when trained only on short UP -words? RQ2: Do structural properties of the underlying DBAs influence (a) generalization performance and (b) learned model complexity?
To answer these questions, we use the -regular languages associated with two well-known LTL benchmarks. The first benchmark ( alaska_lift) [22] consists of two encodings of safe lift behaviors (we use the variants with bug-fixes [ 23]) parameterized by the number of floors: encoding (a) uses a linear number of propositions per floor and encoding (b) uses a logarithmic number of propositions per lfoor. The second benchmark ( acacia_example) [24] consists of 25 formulas specifying the behavior of arbiters and trafic light controllers [ 25]. For this benchmark, we use the negated versions of the formulas, which in our setting only flip the labels of the generated sequences.
For each LTL formula, we generate its corresponding DBA using Spot [
Each experiment trains a single-layer vanilla RNN [26] with a hidden dimension of 256 (consistent
with [
To address RQ1, we assess whether RNNs can learn to classify -words by measuring performance on the test data, reporting ID accuracy (lengths 2-64) and OOD accuracy (lengths 65-512) in a summary table. To address RQ2a, we plot the relationship between the number of states in the DBAs and generalization performance. To address RQ2b, we plot the number of states against the parameter norm (2 norm) of the trained models (post-training). We report the Pearson correlation coeficients [ 29] and their statistical significance between the number of states and both OOD accuracy and the trained models’ parameter norms to assess their linear correlations. 3.1. Results In Table 1, we present the results answering RQ1. The majority of tasks (92.6%) had perfect or nearperfect generalization. Two tasks had OOD accuracies of 81.5% and 76.8%.
In Figure 2, we present the plots comparing the number of states with OOD accuracy (Figure 2a) and the models’ parameter norms (Figure 2b). Figure 2a reveals that generalization performance remains consistently high across automata of varying complexity, with 85.2% of tasks achieving perfect accuracy regardless of state count, indicating that RNN capacity is robust to the structural complexity of the underlying BA. OOD accuracy showed no significant correlation with the number of states in the DBA ( = 0.115, = 0.567), suggesting that generalization performance does not necessarily degrade with increasing DBA complexity. Figure 2b shows a strong positive correlation between the number of states in the DBA and the parameter norm of the trained models ( = 0.880, < 0.001), indicating that model complexity aligns with the complexity of the target -regular languages.
)100 (%95 . cc 90 AD 85 O 80 O 75 0 25 50 75
100 25 50 75
(a) OOD accuracy (acc.) remains consistently high (b) Parameter (param.) norm of the trained RNNs across DBAs with large numbers of states. shows a strong positive correlation with the number of states in the DBAs.
We now examine the two tasks that exhibited poor generalization to understand their failure modes. During training, both tasks demonstrate unstable validation patterns that predict their generalization
r40 m o N . m30 a r a P 0 failures (see Figure 3a). Acacia 13 achieves 100% validation accuracy initially but then degrades to random chance (50%), while Acacia 22 oscillates between 100% and 50% throughout training, indicating that neither model converges to a stable representation of the ground truth -regular language. This instability corresponds to poor length generalization, as shown in Figure 3b, where both tasks achieve perfect accuracy on shorter OOD sequences before experiencing sharp degradation to 50% at longer lengths (degradation begins at 345 and 300 for Acacia 13 and Acacia 22, respectively). This degradation suggests that these models converged to local minima, achieving perfect in-distribution accuracy without learning the ground truth -regular language. The DBAs of both failure cases contained accepting sink states. If a sequence reaches such a state, the RNN must encode this information when processing all subsequent symbols. Further investigation is needed to confirm this hypothesis. 1.0 y c a rcu0.8 c A l.a0.6 V
0.0 0.5 Train Step 1.0 ×105
Our experiments demonstrate that RNNs generalize to the recognition of -regular languages from short UP -words. Across 27 tasks with a diverse range of system behaviors, we achieved perfect or near-perfect generalization in 92.6% of cases when testing on sequences up to 8 times longer than training examples. This finding remained consistent across automata ranging from 3 to 105 states, demonstrating that the approach scales to realistic verification problems. These results provide a foundation for developing diferentiable Büchi automata , components within neurosymbolic systems. These components might behave as monitors in reinforcement learning or enable gradient-based search in model checking.
This work has several limitations that future research should address. Sampling sequences from
complex automata (>200 states) proved impractical despite our attempts to speed up the process.
Our experiments were also restricted to DBAs as a first step; notably, DBAs cannot represent all
-regular languages [
This work was supported by the UK EPSRC grant 2760033. The authors would like to thank Frederik Kelbel for reading the paper and the reviewers for their constructive feedback.
During the preparation of this work, the authors used Claude Sonnet 4 in order to: Paraphrase and reword. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.