Analyzing Büchi Automata with Graph Neural Networks

This project, aims at demonstrating the feasibility of using Graph Neural Networks (GNN) to classify Büchi Automata (BA). Büchi Automata serve as formal models for verifying system properties, while Graph Neural Networks leverage machine learning techniques to process data represented as graphs. Our fundamental question centers around whether Graph Neural Networks can effectively learn and classify complex properties inherent to Büchi automata structures.

Büchi Automata on infinite words present many interesting problems and are used frequently in program verification and model checking. A lot of these problems on Büchi automata are computationally hard, raising the question if a learning-based data-driven analysis might be more efficient than using traditional algorithms. Since Büchi automata can be represented by graphs, graph neural networks are a natural choice for such a learning-based analysis.

In this project, we demonstrate how graph neural networks can be used to reliably predict basic properties of Büchi automata when trained on automatically generated random automata datasets. This by proposing a learning-based approach to analyze Büchi automata using Graph Neural Networks.