$\omega$-regular Expression Synthesis from Transition-Based B\"uchi Automata

TL;DR

This paper introduces a direct method for synthesising more compact $-regular expressions from transition-based Bbuchi automata, improving efficiency and scalability over traditional state-based approaches.

Contribution

It presents a novel, sound, and complete method for direct synthesis from transition-based NBAs, reducing expression complexity and increasing synthesis success from LTL formulas.

Findings

Synthesised expressions are more compact, with over 50% reduction on average.

Method successfully synthesises from more LTL formulas compared to state-based approaches.

Empirical results confirm improved efficiency and scalability.

Abstract

A popular method for modelling reactive systems is to use $\omega$-regular languages. These languages can be represented as nondeterministic B\"uchi automata (NBAs) or $\omega$-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 $\omega$-regular expressions from transition-based NBAs. We prove that the method is sound and complete. Our empirical results show that the $\omega$-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 $\omega$-regular expressions from more LTL formulas when using a transition-based instead of a state-based NBA.