Publications
-
Transition‑Based Acceptance for ω‑Regular Expression Synthesis
Formal Aspects of Computing (FAC), 2026
Abstract
Reactive systems, which maintain ongoing interactions with their environment, are typically modeled using ω-regular languages. These languages characterize system behavior with infinite-length execution traces and are represented as nondeterministic Büchi automata (NBAs) or ω-regular expressions. Existing methods for synthesizing expressions from NBAs only handle state-based acceptance. This limitation forces the conversion of compact transition-based NBAs into larger state-based NBAs before synthesis. This article introduces the first direct synthesis method for ω-regular expressions from transition-based NBAs, eliminating the need for this transformation. The method works by decomposing an NBA into triplets of nondeterministic finite automata, subsuming existing pair-based decompositions to handle transition-based acceptance. We prove that our decomposition is correct, establishing our method’s soundness and completeness. We discuss the time and descriptional complexity of our method. Our empirical evaluation on 185 linear temporal logic formulas supports our hypothesis; transition-based synthesis reduces postfix size by 4.1× and 1.5× for recurrence and reactivity properties, respectively. We also analyze the structural NBA factors that determine when the transition-based NBA will yield a more compact expression and develop this into a simple criterion that, when applied, yields expressions that are at least as compact as those obtained by direct state-based synthesis.
-
Length Generalization with Log-Depth Recurrent Units
arXiv preprint, 2026
Abstract
Length generalization remains a persistent challenge for neural networks: recurrent models tend to suffer from positional biases, while transformers are constrained by fixed computational depth. Regular languages provide a frequently used testbed for evaluating length generalization, as label prediction can be checked for any sequence length. We propose MLP-LDRU, a type of Log-Depth Recurrent Unit, which captures a class of associativity-biased operators designed to approximate recurrence through parallel reduction. We evaluate MLP-LDRU on 21 regular-language tasks, consisting of standard benchmarks and new prefix languages, where it achieves 100% out-of-distribution accuracy on 18 tasks and at least 99.9% on the remaining 3 when increasing max training length, outperforming comparable recurrent and attention-based models. We further evaluate MLP-LDRU beyond regular languages on ListOps and NLP classification benchmarks, where it performs competitively.
-
Beyond Fixed Tasks: Unsupervised Environment Design for Task-Level Pairs
Association for the Advancement of Artificial Intelligence (AAAI), 2026
Abstract
Training general agents to follow complex instructions (tasks) in intricate environments (levels) remains a core challenge in reinforcement learning. Random sampling of task-level pairs often produces unsolvable combinations, highlighting the need to co-design tasks and levels. While unsupervised environment design (UED) has proven effective at automatically designing level curricula, prior work has only considered a fixed task. We present ATLAS (Aligning Tasks and Levels for Autocurricula of Specifications), a novel method that generates joint autocurricula over tasks and levels. Our approach builds upon UED to automatically produce solvable yet challenging task-level pairs for policy training. To evaluate ATLAS and drive progress in the field, we introduce an evaluation suite that models tasks as reward machines in Minigrid levels. Experiments demonstrate that ATLAS vastly outperforms random sampling approaches, particularly when sampling solvable pairs is unlikely. We further show that mutations leveraging the structure of both tasks and levels accelerate convergence to performant policies.
-
RNN Generalization to Omega-Regular Languages
Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY), 2025
Abstract
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.