RNN Generalization to Omega-Regular Languages
This addresses scalability challenges in formal verification for reactive systems, offering a potential neurosymbolic approach, though it is incremental as it builds on existing neural methods applied to new formal language domains.
This work tackled the problem of whether recurrent neural networks (RNNs) can generalize to ω-regular languages from linear temporal logic formulas, showing that RNNs achieve high accuracy on out-of-distribution sequences up to 8 times longer than training examples, with 92.6% of tasks achieving perfect or near-perfect generalization.
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 \times$ 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.