Benchmarking of algorithms on extended finite state automata

Abstract

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.