Publication Details

Mata: A Fast and Simple Finite Automata Library

FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: Proceedings of TACAS'24. Luxembourgh: Springer Verlag, 2024, pp. 130-151. ISSN 0302-9743. Available from: https://link.springer.com/chapter/10.1007/978-3-031-57249-4_7
Czech title
Mata: Rychlá a jednoduchá knihovna pro konečné automaty
Type
conference paper
Language
english
Authors
Fiedor Tomáš, Ing., Ph.D. (DITS FIT BUT)
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Hruška Martin, Ing. (DITS FIT BUT)
Chocholatý David, Ing. (FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
URL
Keywords

Nondeterministic finite automata, automata 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.

Published
2024
Pages
130-151
Journal
Lecture Notes in Computer Science, no. 14571, ISSN 0302-9743
Proceedings
Proceedings of TACAS'24
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'24 (TACAS'24), Centre for Security, Reliability and Trust (SnT), University of Luxembourg., LU
Publisher
Springer Verlag
Place
Luxembourgh, LU
DOI
10.1007/978-3-031-57249-4_7
BibTeX 
@INPROCEEDINGS{FITPUB13199,
   author = "Tom\'{a}\v{s} Fiedor and Vojt\v{e}ch Havlena and Luk\'{a}\v{s} Hol\'{i}k and Martin Hru\v{s}ka and David Chocholat\'{y} and Ond\v{r}ej Leng\'{a}l and Juraj S\'{i}\v{c}",
   title = "Mata: A Fast and Simple Finite Automata Library",
   pages = "130--151",
   booktitle = "Proceedings of TACAS'24",
   journal = "Lecture Notes in Computer Science",
   number = 14571,
   year = 2024,
   location = "Luxembourgh, LU",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-031-57249-4\_7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13199"
}
Back to top