Reasoning about Regular Properties: A Comparative Study

Download paper here

My contributions

1. I was the main designer for the experimental evaluation: how the benchmarks were run, how the benchmarks were evaluated, and how the results were presented.
2. I was the main maintainer of the virtual machine, where the tools and experiments were run; I set up most of the tools, as well as made support for each of the tools to be run.
3. I was the main devops for the comparison: I set up the repositories, readmes, and all the necessary informations needed for replication of the results. As well as the downloadable virtual machine.
4. I was overlooking the correctness of the experiments. I analysed the threats to validity of our claims and results.

Abstract

Several new algorithms for deciding emptiness of Boolean combinations of regular languages and of languages of alternating automata have been proposed recently, especially in the context of analysing regular expressions and in string constraint solving. The new algorithms demonstrated a significant potential, but they have never been systematically compared, neither among each other nor with the state-of-the art implementations of existing (non)deterministic automata-based methods. In this paper, we provide such comparison as well as an overview of the existing algorithms and their implementations. We collect a diverse benchmark mostly originating in or related to practical problems from string constraint solving, analysing LTL properties, and regular model checking, and evaluate collected implementations on it. The results reveal the best tools and hint on what the best algorithms and implementation techniques are. Roughly, although some advanced algorithms are fast, such as antichain algorithms and reductions to IC3/PDR, they are not as overwhelmingly dominant as sometimes presented and there is no clear winner. The simplest NFA-based technology may sometimes be a better choice, depending on the problem source and the implementation style. We believe that our findings are relevant for development of automata techniques as well as for related fields such as string constraint solving.

Cite us

FIEDOR Tomáš, HOLÍK Lukáš, HRUŠKA Martin, ROGALEWICZ Adam, SÍČ Juraj and VARGOVČÍK Pavol. Reasoning about Regular Properties: A Comparative Study. In: Automated Deduction - CADE 29. Cham: Springer Nature Switzerland AG, 2023, pp. 286-306. ISSN 0302-9743.