-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.