$ω$-regular Expression Synthesis from Transition-Based Büchi Automata

TL;DR

The paper introduces a direct method to synthesize ω-regular expressions from transition-based Büchi automata (NBAs), avoiding the traditionally required translation to state-based NBAs. It decomposes a transition-based NBA into triplets of NFAs for each pair of states, derives regular expressions from these NFAs, and composes them into an ω-regular expression that exactly recognises the NBA's language, with proofs of soundness and completeness. Empirical results show that this TB-NBA–driven approach yields substantially more compact expressions than SB-NBA–driven methods, especially for recurrence, obligation, reactivity, and safety LTL formulas, and it increases the set of formulas that can be processed within time limits. The work offers a modular framework (via NFA2Regex) and demonstrates significant practical impact for synthesising compact ω-regular expressions from LTL-driven specifications, with clear avenues for future extensions to broader LTL contexts and formal boundedness proofs.

Abstract

A popular method for modelling reactive systems is to use $ω$-regular languages. These languages can be represented as nondeterministic Büchi automata (NBAs) or $ω$-regular expressions. Existing methods synthesise expressions from state-based NBAs. Synthesis from transition-based NBAs is traditionally done by transforming transition-based NBAs into state-based NBAs. This transformation, however, can increase the complexity of the synthesised expressions. This paper proposes a novel method for directly synthesising $ω$-regular expressions from transition-based NBAs. We prove that the method is sound and complete. Our empirical results show that the $ω$-regular expressions synthesised from transition-based NBAs are more compact than those synthesised from state-based NBAs. This is particularly the case for NBAs computed from obligation, reactivity, safety and recurrence-type LTL formulas, reporting in the latter case an average reduction of over 50%. We also show that our method successfully synthesises $ω$-regular expressions from more LTL formulas when using a transition-based instead of a state-based NBA.

Figures (8)

• Figure 1: The transition-based NBA $B_1$. Edges with circled labels indicate accepting transitions.
• Figure 2: The NFAs $\mathcal{A}_{01,\,\text{all}}$, $\mathcal{A}_{11,\,\text{rej}}$ and $\mathcal{A}_{11,\,\text{acc}}$ of $B_1$. Regular expressions that agree with these automata are $a+ba^\ast b$, $c$ and $da^\ast b$, respectively.
• Figure 3: This presents a comparison between expressions synthesised from state-based and transition-based NBAs. Each circle represents an expression synthesised from LTL formulas in the timelines dataset without simplification. Circles below $y=x$ show that the metric was smaller for the expression synthesised from the transition-based NBA compared to the one from the state-based NBA.
• Figure 4: These plots present the proportional reductions in rpn for the formulas in the timelines dataset grouped by their type. Circles are outliers and represent formulas more than $1.5\times$ outside the interquartile range.
• Figure 5: Several patterns and complements give significantly smaller rpn for expressions from transition-based NBAs. However, most formulas in this dataset show no or negligible improvement.

Theorems & Definitions (6)

• definition thmcounterdefinition: Nondeterministic Finite Automaton
• definition thmcounterdefinition: Transition-based NBA
• proposition thmcounterproposition
• theorem thmcountertheorem: Soundness and completeness
• proof
• proof