RNN Generalization to Omega-Regular Languages
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Regular omega-Languages with an Informative Right Congruence
A regular language is almost fully characterized by its right congruence relation. Indeed, a regular language can always be recognized by a DFA isomorphic to the automaton corresponding to its right congruence, hencefort…
Omega-Regular Reward Machines
Reinforcement learning (RL) is a powerful approach for training agents to perform tasks, but designing an appropriate reward mechanism is critical to its success. However, in many cases, the complexity of the learning ob…
Reinforcement Learning (RL)Reinforcement Learning for Omega-Regular Specifications on Continuous-Time MDP
Continuous-time Markov decision processes (CTMDPs) are canonical models to express sequential decision-making under dense-time and stochastic environments. When the stochastic evolution of the environment is only availab…
Decision Makingreinforcement-learningReinforcement LearningReinforcement Learning (RL)+2Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives
Recent advances in reinforcement learning (RL) have renewed focus on the design of reward functions that shape agent behavior. Manually designing reward functions is tedious and error-prone. A principled alternative is t…
Reinforcement Learning (RL)Spatiotemporal Tubes based Controller Synthesis against Omega-Regular Specifications for Unknown Systems
This paper provides a discretization-free solution to the synthesis of approx-imation-free closed-form controllers for unknown nonlinear systems to enforce complex properties expressed by $\omega$-regular languages, as r…
Robot Navigation