A More Robust Corpus of Büchi Automata
Corey Scott Fisher · Digital Commons - Trinity University (Trinity University) · 2015
Formal verification is a process that proves computational systems adhere to a specification. The automata-theoretic model uses automata, in our case Büchi automata, to model programs and specify how the programs should behave. A core part of formal verification is to check that the program is contained in its specification. Checking the containment of Büchi automata is PSPACE-complete: in the worst case taking time exponential in the size of the automata. Such terrible worst cases are not always present in practice, so researchers wish to test algorithms on more practical cases. To date, the field has used the Tabakov-Vardi random model of automata as a corpus for experiments. However, the Tabakov-Vardi model produces unstructured automata that thus do not strongly resemble real-world problems. We define 7 new models of random automata, most of which are based on structured graph models from other disciplines. Additionally, we define two properties that a random model should possess to be useful for experiments: texture and stability. We empirically examine the models. Six of the models are textured, and we found promising stability in two models.