Publication Details
Mata: A Fast and Simple Finite Automata Library
Fiedor Tomáš, Ing., Ph.D. (RG VERIFIT)
Havlena Vojtěch, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Hruška Martin, Ing., Ph.D. (Automata@FIT)
Lengál Ondřej, Ing., Ph.D. (DITS)
Síč Juraj, Mgr. (DITS)
Nondeterministic finite automata, automata library
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.
@inproceedings{BUT188471,
author="David {Chocholatý} and Tomáš {Fiedor} and Vojtěch {Havlena} and Lukáš {Holík} and Martin {Hruška} and Ondřej {Lengál} and Juraj {Síč}",
title="Mata: A Fast and Simple Finite Automata Library",
booktitle="Proceedings of TACAS'24",
year="2024",
journal="Lecture Notes in Computer Science",
number="14571",
pages="130--151",
publisher="Springer Verlag",
address="Luxembourgh",
doi="10.1007/978-3-031-57249-4\{_}7",
issn="0302-9743",
url="https://link.springer.com/chapter/10.1007/978-3-031-57249-4_7"
}