RNN能泛化到复杂时序逻辑语言，验证规模超训练数据8倍

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.