Analyzing Büchi Automata with Graph Neural Networks
This work addresses efficiency challenges in program verification and model checking for researchers and practitioners, but it is incremental as it applies an existing method to a new domain.
The paper tackled the problem of analyzing Büchi automata, which are computationally hard to handle with traditional algorithms, by using graph neural networks to predict their basic properties, achieving reliable results when trained on random datasets.
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 paper, 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.