Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Mata, a Fast and Simple Finite Automata Library (Technical Report)

David Chocholatý, Tomáš Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruška, Ondřej Lengál, Juraj Síč

TL;DR

It is shown that Mata is on this benchmark significantly faster than all libraries from a wide range of automata libraries the authors collected, and outperforms the state of the art in string constraint solving on many standard benchmarks.

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.

Mata, a Fast and Simple Finite Automata Library (Technical Report)

TL;DR

It is shown that Mata is on this benchmark significantly faster than all libraries from a wide range of automata libraries the authors collected, and outperforms the state of the art in string constraint solving on many standard benchmarks.

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.
Paper Structure (33 sections, 6 figures, 3 tables)

This paper contains 33 sections, 6 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Automata techniques.
  4. Representations of the transition relation.
  5. Alternating automata.
  6. String solving and SMT solvers.
  7. Automata libraries.
  8. Preliminaries on Finite Automata
  9. Words and alphabets.
  10. Finite automata.
  11. Automata operations.
  12. The Architecture of Mata
  13. Automata Representation
  14. Data structure for the transition relation.
  15. Automata Operations
  16. ...and 18 more sections

Figures (6)

  • Figure 1: The transition relation.
  • Figure 2: An example of a Python interface for Mata. The code (\ref{['fig:vis-code']}) loads automata from regular expressions (a, b are transition symbols; *, and + represent iterations: 0 or more, and 1 or more, respectively), concatenates them, and displays the trimmed concatenation using the conditional formatting with the output in (\ref{['fig:vis-aut']}).
  • Figure 3: NFA with explicit alphabet.
  • Figure 4: NFA with symbolic alphabet.
  • Figure 6: Cactus plot showing cumulative run time per benchmark. The time axis is logarithmic.
  • ...and 1 more figures