Publication result detail

Mata: A Fast and Simple Finite Automata Library

HOLÍK, L.; CHOCHOLATÝ, D.; FIEDOR, T.; HAVLENA, V.; HRUŠKA, M.; LENGÁL, O.; SÍČ, J.

Original Title

Mata: A Fast and Simple Finite Automata Library

English Title

Mata: A Fast and Simple Finite Automata Library

Type

Paper in proceedings outside WoS and Scopus

Original 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.

English 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.

Keywords

Nondeterministic finite automata, automata library

Key words in English

Nondeterministic finite automata, automata library

Authors

HOLÍK, L.; CHOCHOLATÝ, D.; FIEDOR, T.; HAVLENA, V.; HRUŠKA, M.; LENGÁL, O.; SÍČ, J.

RIV year

2025

Released

04.04.2024

Publisher

Springer Verlag

Location

Luxembourgh

Book

Proceedings of TACAS'24

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

14571

State

Federal Republic of Germany

Pages from

130

Pages to

151

Pages count

22

URL

https://link.springer.com/chapter/10.1007/978-3-031-57249-4_7

Full text in the Digital Library

http://hdl.handle.net/11012/252869

BibTex

@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"
}

Documents

978-3-031-57249-4_7