Mata: A Fast and Simple Finite Automata Library

Download paper here

My contributions

1. I was the one of the main designers 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 devops for the comparison as well as the project: I set up the repositories, readmes, and all the necessary informations needed for replication of the results. As well as the downloadable virtual machine. I set up the continuous integration, performance tests, etc.
3. I am the main author of the efficient Python binding for the Mata library.

Abstract

Mata is a well-engineered automata library written in C++ that offers a unique combination of speed and simplicity. It is meant to serve in applications such as string constraint solving and reasoning about regular expressions, and as a reference implementation of automata algorithms. Besides basic algorithms for (non)deterministic automata, it implements a fast simulation reduction and antichain-based language inclusion checking. The simplicity allows a straightforward access to the low-level structures, making it relatively easy to extend and modify. Besides the C++ API, the library also implements a Python binding.

The library comes with a large benchmark of automata problems collected from relevant applications such as string constraint solving, regular model checking, and reasoning about regular expressions. We show that Mata is on this benchmark significantly faster than all libraries from a wide range of automata libraries we collected. Its usefulness in string constraint solving is demonstrated by the string solver Z3-Noodler, which is based on Mata and outperforms the state of the art in string constraint solving on many standard benchmarks.

Cite us

CHOCHOLATÝ, David, FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS’24. Lecture Notes in Computer Science, vol 14571. Springer, Cham.