$\omega$-regular Expression Synthesis from Transition-Based B\"uchi Automata
<|reference_start|>$\omega$-regular Expression Synthesis from Transition-Based B\"uchi Automata: 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.<|reference_end|>
@article{pert2024$\omega$-regular,
    title={$\omega$-regular Expression Synthesis from Transition-Based B\"uchi
  Automata},
    author={Charles Pert and Dalal Alrajeh and Alessandra Russo},
    journal={arXiv preprint arXiv:2406.08136},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.08136},
    primaryClass={cs.FL}
}