Universality of Büchi Automata: Analysis With Graph Neural Networks

The universality check of Buchi automata is a foundational problem in automata-based formal verification, closely related to the complementation problem, and is known to be computationally difficult, more concretely: PSPACE-complete. This article introduces a novel approach for creating labelled datasets of Buchi automata concerning their universality. We start with small automata, where the universality check can still be algorithmically performed within a reasonable timeframe, and then apply transformations that provably preserve (non-)universality while increasing their size. This approach enables the generation of large datasets of labelled Buchi automata without the need for an explicit and computationally intensive universality check. We subsequently employ these generated datasets to train Graph Neural Networks (GNNs) for the purpose of classifying automata with respect to their universality resp. non-universality. The classification results presented in this article indicate that such a network can learn patterns related to the behaviour of Buchi automata that facilitate the recognition of universality. Additionally, our results on randomly generated automata, which were not constructed using the aforementioned transformation techniques and classified algorithmically, demonstrate the network's potential in classifying Buchi automata with respect to universality, extending its applicability beyond cases generated using a specific technique.