Simon Dierl defends Doctoral Dissertation
Extended finite state automata are a powerful formalism that can model many complex
systems in a finite representation and remain amenable to analysis. A wide variety of
algorithms interacts with these automata: for example, automata learning algorithms derive
them from black-box systems, while model checking algorithms can verify their properties.
When developing such algorithms, it is essential to perform benchmarking, i.e., analyze the
algorithm’s performance on models of such machines. The choice of benchmark directly
impacts the quality of the evaluation, with better benchmarks allowing for well-founded
conclusions that are not restricted to, e.g., models of specific types of system.
However, sources for benchmarks for extended finite state automata are limited. Only a single
benchmark library and only simple synthesis algorithms are described in the literature. It
is not clear what, given these restrictive circumstances, a good selection of benchmarks for
a study is and to what extent choice of benchmarks ultimately impacts the strength of the
study’s results.
This thesis addresses this problem by analyzing limits in the availability and use of benchmarks
in both extended finite state automata and finite state automata research and identifying the
causes of these limits. We then address these causes and improve upon the current state of the
art in benchmarking by defining two synthesis algorithms for extended finite state automata.
We also tackle the lack of benchmark libraries by introducing recombinable benchmarks and
tools, which simplify the creation and reuse of such libraries.
By analyzing prior works and reflecting on the benchmarking performed in four case studies,
we argue that the optimal approach to benchmarking is the combination of synthetic automata
with well-curated, constantly-updated benchmark libraries. We successfully apply two novel
synthesis algorithms in case studies and show that their benchmarks enable well-founded,
strong conclusions. Finally, we retroactively analyze our approach to recombinability on our
case studies and show its practicality in terms of effort required.