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

A popular method for modelling reactive systems is to use ω-regular languages. These languages can be represented as nondeterministic B\"uchi 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.