Ulrich Ultes-Nitsche | Searcharxiv

arXiv2022

Analyzing Büchi Automata with Graph Neural Networks

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.

cs.FL↗

arXiv2001

Checking Properties within Fairness and Behavior Abstractions

This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used. It shows that using a more abstract notion than truth under fairness, specifically the concept of a property being satisfied within fairness can lead to interesting possibilities. Technically, it is first established that deciding satisfaction within fairness is a PSPACE-complete problem and it is shown that properties satisfied within fairness can always be satisfied by some fair implementation. Thereafter, the interaction between behavior abstraction and satisfaction within fairness is studied and it is proved that satisfaction of properties within fairness can be verified on behavior abstractions, if the abstraction homomorphism is weakly continuation-closed.

cs.LO↗