: 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íč

D. Chocholatý, T. Fiedor, V. Havlena, L. Holík, M. Hruška, O. Lengál, J. Síč

Brno University of Technology, Czech Republic

is a well-engineered automata library written in 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 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 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 , which is based on and outperforms the state of the art in string constraint solving on many standard benchmarks.

§ INTRODUCTION

We introduce a new finite automata library .
It is intended to be used in applications where automata languages are manipulated by set operations and queries, presumably in a tight loop where automata are iteratively combined together using the classical as well as special-purpose constructions. Examples are applications like
string constraint solving algorithms such as <cit.>,
processing of regular expressions <cit.>,
regular model checking (e.g., <cit.>),
or decision procedures for logics such as WS1S or quantified Presburger arithmetic <cit.>.

The solved problems are computationally hard, often beyond the PSPACE-completeness of basic automata problems such as language inclusion.
Efficiency is hence a primary concern.

Achieving speed in applications requires, on one hand, fast implementation of basic automata algorithms (union, intersection, complement, minimization or size reduction, determinization, emptiness/inclusion/equivalence/membership test, parsing of regular expressions)

and, on the other hand, access to low-level primitives to implement diverse application-specific algorithms and optimizations
that often build  on a tight integration with the application environment.

Moreover, processing of regular expressions and, even more so, string constraint solving are areas of active research,

with constantly evolving algorithms, heuristics, and optimizations.

An automata library hence needs flexibility, extensibility,
easy access to the low-level data structures,

and ideally a low learning curve, which is important when involving students in academic research and utilizing limited resources of small research teams.

Fast and simple are therefore our two main requirements for the library.

An additional third requirement is a well-engineered infrastructure and a good set of benchmarks and tests,
important for effective research and reliable deployment.

is therefore built around a data structure for the transition relation of a non-deterministic automaton that is a compromise between simplicity and speed.

It represents transitions explicitly, as triples of a sources state, a single symbol, and a target state.

This contrasts with various flavors of symbolic representation of transition relation used in advanced automata implementations in order to handle large or infinite alphabets (e.g. Unicode in processing of texts, or bit vectors in reasoning about LTL, arithmetic, or WS1S).

However, in the applications we consider, working internally with large alphabets can essentially always be avoided by preprocessing (mainly by mintermization, aka factorization of the alphabet).
The simplicity of an explicit representation then seems preferable.

It allows to use a data structure specifically tailored for computing post-images of tuples and sets of states in automata algorithms:
a source state-indexed array, storing at each index the transitions from that source state in a two layered structure, with the first layer divided and ordered by symbols, and the second layer ordered by target states.

The data structure seems to be unique among the existing libraries and yields an exceptional performance.

currently provides basic functionality, basic automata operations and tests, parsing of regexes and automata in a textual format, and mintermization.

From the more advanced algorithms for working with non-deterministic automata, it implements antichain-based inclusion checking <cit.>,
and simulation-based size reduction based on the advanced algorithm of <cit.>.

The inclusion check appears to be by a large margin the fastest implementation
available, and together with the tree automata library  <cit.>, is the only library with an implementation of a simulation algorithm of the
second generation originating from <cit.>
(the second generation algorithms combine partition-relation pairs to
manipulate preorders that were handled explicitly by the first generation
algorithms such as <cit.>).

is implemented in , uses almost exclusively the STL library for its data structures, and has no external dependencies[Although, at the moment, it uses the BDD library CUDD <cit.> in mintermisation and the regular expression parser from RE2 <cit.>.  The code from these projects is, however, contained within . Moreover, the connection to CUDD is not tight and we plan to remove it in the future.]
This makes it relatively easy to learn and integrate with other software projects.

It is a well-engineered project at GitHub, with modern test and quality of code assurance infrastructure.

Besides the API, it provides a Python binding for fast prototyping and easy experimenting, for instance using interactive Jupyter notebooks.

We evaluated its speed in, to our best knowledge, so far the most comprehensive comparison of automata libraries.

We compare with 7 well-known automata libraries on a large benchmark of problems from domains close to 's designation, mainly string constraint solving, processing regular expressions, and regular model checking.
consistently outperforms all other libraries, from several times to orders of magnitude.

The fact that is a good fit for string constraint solving is demonstrated by its central role in the string solver , which implements the algorithm of <cit.>,
and outperforms the state of the art on many standard benchmarks (see <cit.> for details).

Our contributions can be summarised by the following three points:

* , a fast, simple, and well-engineered automata library,
well suited for application in string constraint solving and regex processing, in research and student projects, as well as in industrial applications.

* An extension of a benchmark of automata problems from string constraint solving, processing regular expressions, regular model checking, and solving arithmetic constraints.

* A comparison of a representative sample of well-known automata libraries against the above benchmark, demonstrating the superior performance of .

§ RELATED WORK

In this overview of automata algorithms and implementations,

we focus on the technology relevant to , i.e., automata used as a symbolic representation of sets of words and manipulated mainly by set operations. We omit automata technology made for other purposes, such as regular pattern matching, which concentrates on the membership test.

Automata techniques.
The most textbook-like approach is to keep finite automata deterministic (the so-called DFA), which has the advantage of simple algorithms and data structures. Essentially all classical problems reduce to product construction, determinization by subset construction, final state reachability test, and minimization (by Hopcroft's <cit.>, Moore's <cit.>, Brzozowski's <cit.>, or Huffman's <cit.> algorithms).
The obvious drawback is the susceptibility to state explosion in determinization.

An alternative is to determinize automata only when necessary (e.g., only before complementing).
Non-determinism may bring up to exponential savings in automata sizes and modern algorithms for nondeterministic finite automata (NFA) can in practice avoid the exponential worst-case cost of problems like the language inclusion test.

Namely, a major breakthrough in working with NFAs were the antichain-based algorithms for testing language universality and inclusion of NFA first introduced (to the best of our knowledge) in <cit.> and later rediscovered in <cit.>.
They dramatically improve practical efficiency of the subset construction by subsumption pruning (discarding larger sets).
They were later extended with simulation <cit.> (and generalized to numerous other kinds of automata and problems).
A principally similar is the bisimulation up-to congruence technique of <cit.>, which optimizes the NFA language equivalence test.  Although experimental data in various works are somewhat contradictory,
the more systematic studies so far found antichain-based algorithms more efficient <cit.>.

NFAs require more involved reduction methods than DFAs, such as those based on simulation <cit.> or bisimulation <cit.>.
Simulation reduces significantly more but is much more costly.
The algorithms for computing simulation of the second generation <cit.>, which use the so-called partition-relation pairs to represent preorders on states, are practically much faster than the first generation algorithms <cit.>.

Representations of the transition relation.
In order to handle automata over large or infinite alphabets, such as Unicode or bit vectors, some implementations of automata represent transitions symbolically.
Transitions may be annotated by sets of symbols represented as
BDDs, logical formulae, intervals of numbers, etc.
The most systematic approach to this has been taken in works on  symbolic automata <cit.>, where the symbol predicates may be taken from any effective Boolean algebra (essentially a countable set closed under Boolean operations).
Some libraries, such as Spot <cit.>, Owl <cit.>, or Mosel <cit.> use BDDs to compactly represent sets of symbols on transitions.
Even more compact are the symbolic representations of the transition relation used in  <cit.> and in the symbolic version of the tree automata library  <cit.>, where all transitions starting at a state are represented as a single multi-terminal BDDs with the target states in the leaves (the paths represent symbols).

Although symbolic representation may offer new optimization opportunities <cit.> and give more generality

, it also brings complexity and overhead.
Adapting the known algorithms may be nontrivial <cit.> to the point of being a difficult unsolved problem (such as the fast computation of simulation relation of <cit.>).

In our application area,
working with large alphabets can mostly be avoided in preprocessing, for instance by means of a priori mintermization
(partitioning the alphabet into groups of symbols indistinguishable from the viewpoint of the input problem).

The simplicity and transparency of explicit representation of transitions then seems preferable.

Alternating automata.

Alternating automata (AFA) received attention recently
in the context of string solving and regex processing  <cit.>.
They allow to keep automata operations implicit up to the point of the PSPACE-complete emptiness test, which can be solved by clever heuristics (e.g. <cit.>).

Available implementations were recently compared with selected NFA libraries <cit.> and neither approach dominated.

AFA are, however, often not a viable alternative since adapting complex algorithms from, e.g., string solving to AFA typically requires to redesign the entire algorithm from scratch (as, e.g., in <cit.>).

String solving and SMT solvers.
String constraint solving is currently the primary application target of . is already a basis of an efficient string solver  <cit.> and a number of other string solvers could perhaps benefit from its performance, especially those that already use automata as a primary data structure, e.g. <cit.>.

Besides, SMT string constraint solvers can also be used to reason about regular properties, though the results of <cit.> suggest that their efficiency is not on par with dedicated fast automata libraries.

Automata libraries.

We give overview of known automata libraries with a focus on those that we later include in our experimental comparison in <ref>.

The  <cit.> automata library is often considered a baseline in comparisons.
It implements both NFA and DFA, where each state keeps the set (implemented as a hash map) of transitions, which are represented symbolically using character ranges.
It is written in Java and relatively optimized.

The library <cit.>, written in , implements symbolic NFA parameterized by an effective Boolean algebra.

The transition relation (as well as its inverse) are implemented as a hash map from states to the dynamic array of transitions from a given state, each transition annotated with a predicate over the algebra.
We use it in our comparison with the algebra of BDDs.
has been developed for a long time and has accumulated a number of novel techniques

<cit.>, written in C, is a famous optimized implementation of deterministic automata

used for deciding WS1S/WS$k$S formulae. To handle
DFA with complex transition relations over large alphabets of bit vectors, uses a compact  fully symbolic representation of the transition relation: a single MTBDD for all transitions originating in a state, with the target states in its leaves. can represent only a DFA, hence every operation implicitly determinizes its output.

<cit.>, written in , implements non-deterministic tree automata.
It can be used with NFA, too as they are a special case of tree automata. It is relatively optimized and features fast implementation of the antichain-based inclusion checking <cit.> (which for NFA boils down to the inclusion check of <cit.>) and the second generation simulation computation algorithm of <cit.>.

<cit.> is a library that targets weighted automata and transducers over an arbitrary semiring.
To implement the transition relation, it keeps a vector of transitions and for each state $s$ two vectors: one keeps the indices of transitions leaving $s$ and the other one the indices of transitions entering $s$.

<cit.> is a Java automata library and the basis of the automata learning framework LearnLib <cit.>.
It focuses on DFAs and implements their transition relation as a flattened 2D matrix that maps the source state and symbol to the target state.

<cit.> is written in Python.
It defines the transition relation in a liberal way, as any mapping from source states to a mapping of symbols to a target state (DFA) or to a set of target states (NFA).

<cit.> is a Python library written with efficiency in mind. It uses a similar structure as , but more specific, with the transition as a Python dictionary (a hash map), and states represented as numbers used as indices into an array.

There is a number of other automata libraries that we do not include into our comparison since they seem similar to the included ones or we were not able to use them. The C alternative of <cit.> and the Java implementation of symbolic NFA of <cit.> are in our experiment covered by and . Alaska <cit.> contains interesting implementations of antichain-based algorithms, but is no longer maintained nor available.

<cit.> is a long-developed tool for arithmetic reasoning based on automata, with an efficient core automata library, written in C.

Its transition relation is an array indexed by states, where every state is associated with a symbol-target ordered list of transitions.

uses partial symbolic representation – it encodes symbols as sequence of binary digits.

The comparison with in <cit.> on automata benchmark originating from arithmetic problems placed its performance significantly behind .

It seems to no longer be maintained, and we were not able to run it on our benchmarks.

There is also a number of implementations of automata over infinite words, for instance Spot <cit.>, Owl <cit.>, or Goal <cit.>, which are in their nature close to the finite word automata libraries (Spot and Owl are optimized and use BDDs on transition edges similarly as ), but implement different algorithms.

evolved from a prototype implementation used in the comparison of AFA emptiness checkers as a baseline implementation of classical automata <cit.>.
Surprised by its performance, we decided to turn it into a serious widely usable library.
Current is much more mature and efficient than the of <cit.>.

§ PRELIMINARIES ON FINITE AUTOMATA

Words and alphabets.

An alphabet is a set $\Sigma$ of symbols/letters (usually denoted $a,b,c,\ldots$) and the set of all words over $\Sigma$ is denoted as $\Sigma^*$.
The concatenation of words $u$ and $v$ is denoted by $u\concat v$.
The empty word, the neutral element of concatenation, is denoted by $\epsilon$ ($\epsilon \notin \Sigma$).

Finite automata.
A (nondeterministic) finite automaton (NFA) over an alphabet $\Sigma$ is a tuple
$\aut= (Q,\post,I,F)$
where $Q$ is a finite set of states,
$\post\colon Q\times(\Sigma\cup\{\epsilon\}) \to 2^Q$ is a symbol-post function, $I\subseteq Q$ is the set of initial states, and $F\subseteq Q$
is the set of final states.
A run of $\aut$ over a word $w \in \Sigma^*$ is
a sequence
\ldots
\aore_n p_n$
where for all $1\leq i \leq n$ it holds that $\aore_i \in \Sigma \cup
\{\epsilon\}$, $p_i \in \post(p_{i-1}, \aore_i)$, and $w = \aore_1
\concat \aore_2 \concats \aore_n$.
The run is accepting if $p_0 \in I$ and $p_n\in F$, and the language
$\langof{\aut}$ of $\aut$ is the set of all words for which $\aut$ has an accepting run.

$\aut$ is called deterministic (DFA) if $|I| \leq 1$, $|\post(q,\epsilon)| = 0$, and $|\post(q,a)| \leq 1$ for each $q\in Q$ and $a \in \Sigma$.
A state is useful if it belongs to some accepting run, else it is useless.
An automaton with no useless states is trimmed.
A state is reachable if it appears on a run starting at an initial state.

In , we further use $\post(q) = \{ (a, \post(q, a)) \mid \post(q,a) \neq \emptyset \}$ to denote
the state-post of $q$.
We call symbol-post and state-post the post-image functions. We also use $\move{q}{a}{p}$ where $p \in \post(q,a)$ to denote transitions.
The set of all transitions of $\aut$ is called the transition relation of $\aut$ and we denote it by $\Delta$.

Automata operations.
In this paragraph we assume automata without $\epsilon$ transitions.

The subset construction generates from $\aut$ the DFA
$(\sc Q,\sc{\post\!}, \sc I, \sc F)$
where $\sc Q = \pow Q$,
$\sc I = \{I\}$,
$\sc F = \{S \in \sc Q\mid S\cap F\neq\emptyset\}$,
and where $\sc{\post\!}(S,a) = \bigcup_{s \in S} \post(s, a)$. The automaton for complement is obtained from it by complementing $\sc F$, i.e., the set of final
states is given as $\sc Q \setminus \sc F$.

The intersection of two automata $\aut_1 = (Q_1,\post_1,I_1,F_1)$ and $\aut_2= (Q_2,\post_2,I_2,F_2)$  is implemented by their product $(Q_1\times Q_2,\post^{{\times}},I_1\times I_2,F_1\times F_2)$ where $\post^{{\times}}((q,r),a) = \post_1(q,a) \times \post_2(r,a)$.

A sensible implementation of course only computes the reachable parts of the product and the subset construction.

The union $L(\aut_1) \cup L(\aut_2)$ is obtained by disjointly uniting all components of $\aut_1$ and $\aut_2$. Similarly, the concatenation
$L(\aut_1) . L(\aut_2)$ is the automaton $(Q_1\uplus Q_2,\post_1 \uplus\post_2 \uplus \post',I_1,F')$ where $\uplus$ denotes the disjoint union, $\post'(q,a) = \{ r \mid  q\in F_1 \land \exists s\in I_2\colon r \in \post_2(s,a) \}$ is the
connecting symbol-post and $F'$ is $F_2$ if $I_2 \cap F_2 = \emptyset$ and $F_1 \cup F_2$ otherwise  (this construction avoids introducing $\epsilon$-transitions).
Note that we omit superscript of symbol-post function when it is clear from the context.

§ THE ARCHITECTURE OF

We explain in this section the implementation techniques that make efficient on a wide range of automata operations.

§.§ Automata Representation

States and transition symbols are unsigned integers (starting from 0). This makes it easy to store information about them in a state-/symbol-indexed vectors.

A frequently used low-level data structure is , a set of ordered elements implemented as an ordered array (with std::vector as the underlying data structure).
It has constant time addition and removal of the largest element (and ), linear union, intersection, and difference (by variants of merging), good memory locality and fast iteration through elements, logarithmic lookup (by binary search), but a slow insertion and removal (and ) at other than the last position, as the elements on the right of the modified position must be shifted.
Many algorithms utilize the constant time handling of the largest element in, e.g., synchronized traversal of multiple containers.

Initial and final states are kept in sparse sets <cit.>, with fast iteration through elements and constant lookup, insertion, and removal.

The transition relation.

Data structure for the transition relation.

The main determinant of is its three-layered data structure for the transition relation.
It is implemented as a vector where, for every state $q$, $\code{\postvec[}q\code{]}$ is of the type , representing $\post(q)$ as an of objects of the type , each in turn representing one $\post(q,a)$ by storing the symbol $a$ and an of the target states.
The s in are ordered by their symbols
supports $\epsilon$-transitions and some operations can work with them internally.
We represent $\epsilon$ as the symbol with the highest possible number, hence with $\epsilon$ is always the last one in the vectors of s in .
The $\epsilon$ is therefore easy to be accessed in, e.g., $\epsilon$-transition elimination.
Some operations also support several $\epsilon$-like symbols (e.g.,
$\epsilon_1$, $\epsilon_2$, …), which are convenient in some algorithms in
string solving <cit.> or can play a role of different
synchronization symbols, etc.
A visualization of is shown in <ref>.

The weak point of is inherited from : slow or
of a specific transition (these operations are, however, used scarcely
in the considered scenarios).
Its strength is mainly fast iteration through the post-image of a state, of
a pair of states in the product construction, and of a set of states in the
subset construction.

§.§ Automata Operations

Generating post-images in subset construction.

In the subset construction, each iteration through $\post(S)$ for a set of states $S$ is keeping an array of iterators, one into each $\post(q)$ for all $q\in S$. Every iteration shifts the iterators to the right, to $\post(q,b)$ where $b$ is the closest from above to the current global minimal symbol $a$, and returns $\post(S,a)$ as the union of all $\post(q,a)$'s pointed to by the iterators.

No searching in vectors is needed. The entire iteration through all $\post(S)$'s makes the iterators in the s traverse their respective vectors only once.

Constructing the transitions leading from $S$ while iterating through $\post(S)$ is done by appending to s, without a need to insert at internal positions of vectors. The iteration through the s is ordered by symbol, hence each newly created transition from the macrostate $S$ has a larger symbol than all the previously created ones. The symbol-post therefore belongs at the end of the of symbol-posts of $\post(S)$, where it is ed.

Since the resulting automaton is deterministic, the vectors of targets are singletons, and their creation does not require either.

Generating post-images in product construction.
Similarly as in the subset construction above, iterating through $\post((q,r))$ in the product construction is done by synchronous iteration through $\post(q)$ and $\post(r)$ from the smallest common symbol to the largest.
In each step, the iteration returns the Cartesian product of the targets in the symbol-posts.

Unlike the subset construction, adding the corresponding transitions from $(q,r)$ to the product automaton sometimes does need an into the vector of targets.
It is however not that frequent:
Newly discovered product states are assigned the so far highest numbers,
so these are added to the target vectors by .
The may hence be needed only when creating a non-deterministic transition to a state discovered earlier.

Storing sets and pairs of states in the subset and product construction.
is also used to map generated sets in the subset to the identities of generated states. The map uses a hash table (std::unordered_map) where values are s.

The product construction uses either a two-dimensional array to map pairs of states to product states (for smaller automata) or a vector pro_map of hash tables, where the identity of the product state $(q,r)$ is found in the hash map prod_map[q] under the key $r$.

Emptiness test and trimming.
Emptiness test and trimming are used frequently and must be fast.
's emptiness test is just a state space exploration that utilizes the fast iteration through post-images of a state.

Trimming  consists of two steps: (1) identification of useful states and (2) removal of states that are not useful.
Identification of useful states must, besides forward exploration to identify reachable states, identify states that reach a final state. A naive solution would be a backward exploration from final states.
is, however, not well suited for backward search and although reverting it is doable, its cost is not negligible either.
We therefore use a smarter solution, which uses a simplification of the
non-recursive Tarjan's algorithm <cit.> to discover strongly connected
components (SCCs).
Tarjan's algorithm is essentially a depth-first exploration augmented to identify the SCCs. To identify useful states, on finding an SCC with a final state, we mark the entire SCC as useful together with all states on the path to that SCC, which is readily stored on the depth-first search stack. The cost of computing useful states is then similar to the cost of a single depth-first exploration, which is indeed negligible.

Removal of useless states then needs to be done in a -friendly way.
The naive approach that removes useless states and transitions incident with
them one by one would be extremely slow due to the need of searching and
calling in the s of .
Instead, we perform the whole removal and related operations in a single pass through .
Before the pass begins, first, we create a map renaming mapping each
useful state to its new name (the trimming also renames the states in order to have
the remaining states form a consecutive sequence).
During the pass, the following operations need to be performed:

* in the outermost loop, each useful state $q$ in is moved
to index renaming[$q$],

* in every vector of target states, each useful target is moved to the
left in the target vector by that many positions, as there were smaller
useless states before it, and

* while doing that, the target state $q$ is renamed to

Union and concatenation.
is relatively slow in operations that copy or create large parts of automata, such as non-deterministic union or concatenation, or simple copying of an automaton.
This is perhaps due to the imperfect memory locality (the three layers of vectors in ) and the need to copy every single transition (unlike, e.g., symbolic automata with BDDs on transitions, where the BDDs may be shared).
has, however, in-place variants of union and concatenation, which do not copy , but only append the vectors and rename the target states in the appended part, which is fast. The price for the speed is the loss of the original automata, but they are in many use cases not needed (as, e.g., in inductive constructions of automata from regular expressions or formulae).

Antichain-based inclusion checking.
implements the antichain-based inclusion checking of <cit.>. Given the inclusion problem $L(\aut) \subseteq L(\but)$, the algorithm explores the space of the product of $\aut$ and the subset construction on $\but$, consisting of pairs $(q,S)$ with $q$ being a state of $\aut$ and $S$ being a set of states of $\but$. In particular, it searches, on the fly, for a reachable pair $(q,S)$ with a final $q$ and a non-final $S$, which would be a witness non-inclusion.
The algorithm optimizes the search by subsumption pruning—discarding states $(q,S)$ if another $(q,S')$ with $S\subseteq S'$ has been found.

Our implementation uses the infrastructure for computing post-images of product and subset construction discussed above. The reached pairs $(q,S)$ are stored in a state-$q$-indexed vector $\code{incl\_map}$ of collections of sets $S$. The sets are again represented as s.
On reaching a pair $(q,S)$, all sets $S'$ stored in
$\code{incl\_map[}q\code{]}$ are tested for inclusion with $S$.
If $S\supseteq S'$, then $S$ is dropped, and if $S\subseteq S'$, then $S'$ is
removed from $\code{incl\_map[}q\code{]}$ (as well as other sets $S''$ such
that $S \subseteq S''$) and $S$ is added to $\code{incl\_map[}q\code{]}$.

A large speed-up is sometimes obtained by prioritizing exploration of pairs $(q,S)$ with $S$ being of a small size. A smaller set means a better chance to subsume other pairs, to reach a witness of non-inclusion, and to generate other pairs with small sets. The algorithm then explores a much smaller state space.

uses an implementation of a fast algorithms for computing simulation,
namely, the algorithm from <cit.>, which was adapted
from Kripke structures to automata in <cit.>, and later further
optimized in <cit.>.
The implementation originates in  <cit.>.

Low-level API.
The API of contains an interface for accessing the most low-level
features needed to implement algorithms in the style described above.
For instance, the API provides iterators over transitions of $\Delta$ in the
form of triples $\move q a r$, iterators through moves (pairs $(a,r)$
such that $\move q a r \in \Delta$) of a state $q$, or generic
synchronized iterators, which allow a simultaneous iteration in a set of
vectors used in union and in computing the post-image in the product and subset

Since the main data structures are not complicated and have simple invariants, programming with them on the low level is possible even for an outsider.

This low-level API is, for instance, used in
the string solver .
<cit.> presents a detailed comparison
of with the state of the art in string solving.
Its exceptional performance on regex and word equation-heavy constraints is to
a large degree due to .

§ INFRASTRUCTURE OF

comes with the following tools and features to make using, developing, and extending it convenient.

from libmata import nfa, alphabets, parser, plotting
aut1 = parser.from_regex('((a+b)*a)*')
aut2 = parser.from_regex('aab*')
con_aut = nfa.nfa.concatenate(aut1, aut2).trim()
plotting.store()['alphabet'] =     alphabets.OnTheFlyAlphabet.from_symbol_map('a':97, 'b':98)
e_h = [
(lambda aut, e: e.symbol == 98, 'color':'black'),
(lambda aut, e: e.symbol == 97, 'style':'dashed','color':'black')
n_h = [
(lambda aut, q: q in aut.final_states,
(lambda aut, q: q in aut.initial_states,
'color': 'orange', 'fillcolor': 'orange'),
plotting.plot(con_aut, with_scc=True,
node_highlight=n_h, edge_highlight=e_h)

An example of using from Python.

The output.

An example of a Python interface for . The code (fig:vis-code) loads
automata from regular expressions (,  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 (fig:vis-aut).

Python interface.

provides an easy-to-use Python interface, making it a full-fledged automata library for Python projects.
It is available on the official Python package
repository[<https://pypi.org/project/libmata/>] and can be
installed easily using the  package manager:

$ pip install libmata

An example of using the Python binding is shown in <ref>.
The interface is implemented using the optimizing static compiler Cython wrapping the calls and
covers all important parts of the functionality.
This low-level interaction with the optimized code keeps the Python code
To show the capabilities of the

q0 a48 q1
q0 a52 q1
q1 a48 q1

NFA with explicit alphabet.

q0 ((!a0 | !a1)     a2) q2
q1 (a0     a1     !a2) q0
q2 ((a0     a1) | a2) q1

NFA with symbolic alphabet.

Examples of NFAs in the .mata format.

interface and to provide material for easy
onboarding, also contains several Jupyter notebooks with examples of
how to use it.

.mata format and parsing.

brings its own automata format. The main features of the format
are extensibility to cover various types of automata, human-readability, yet
still high level of compactness.
Each .mata file consists of automata definitions.
The first line of the definition describes the type of the automaton, together
with the alphabet.
The format supports both explicit and symbolic (bit vector) alphabets.
For a symbolic alphabet, symbols are encoded as formulae over atomic propositions, where
the parser of .mata implements mintermization (partitioning the alphabet
into groups of symbols indistinguishable from the viewpoint of the input
problem), which transforms it into an explicit alphabet with the symbols
representing the minterms.
The following lines contain a sequence of key-values statements that set particular
traits of the automaton, such as initial or final states. The rest of the definition
is a list of transitions. Examples of automata in .mata format are shown in

Other than the introduced format, can also parse automata from regular
expressions using the parser from the regex matcher RE2 <cit.>.
This means that can handle even complex syntax used in real-world regular expressions.

Continuous integration.

In order to keep the main branch of the library stable, we implement continuous integration via GitHub Actions.
In particular, actions automatically build the library including the Python binding on multiple operating systems, check for warnings, code
quality and run unit tests together with the code coverage. The actions are triggered after each commit, and the checks are mandatory
for merging branches to the main branch. All checks can also be run manually in
a local development environment.

§ EXPERIMENTAL EVALUATION

Cactus plot showing cumulative run time per benchmark. The time axis is logarithmic.

We compared against 7 selected libraries discussed in

<cit.>, <cit.>, <cit.>, <cit.>, <cit.>,
<cit.>, and  <cit.>,

[We also tried to compare with , but using it as a
standalone library that would parse automata in our format turned to be problematic. We were getting many inconsistent results and so we decided to drop it from the comparison.]

on a benchmark of basic
automata problems from string constraint solving, reasoning about regular
expressions, regular model checking, and a few examples from solving arithmetic
formulae. Most of the benchmark problems are taken from earlier works
<cit.>, but we
added new problems from string constraint solving and solving quantified linear
integer arithmetic (LIA).

We mainly aim to demonstrate the efficiency of the basic data structures and
implementation techniques of . This is best seen on standard constructions,
where all libraries implement the same high-level algorithm, such as
product, subset construction, or reachability test within complementation,
intersection, emptiness test, etc.

We then also showcase the efficiency of more advanced algorithms implemented only in and ,
the antichain-based inclusion test and
simulation reduction.

Statistics for the benchmarks. We list the number of timeouts (TO), average time on solved instances (Avg), median time over all instances (Med), and standard deviation over solved instances (Std), with the best values in bold. The times are in milliseconds unless seconds are explicitly stated. We use to denote a value close to zero.

Relative speedup of on instances where both libraries finished.

Cactus plot showing cumulative run time per operation. The time axis is logarithmic.

We use the following benchmark sets.

contains 384 instances of boolean combinations of regular properties, obtained from SMT formulae over the theory of strings.
These include difficult handwritten problems containing membership in regular expressions extended with intersection and complement from <cit.> and emptiness problems from Norn <cit.> and SyGuS-qgen benchmarks, collected in SMT-LIB <cit.>.

<cit.> contains 500 inclusion checks of the form $r_5 \subseteq r_1 \land r_2 \land r_3 \land r_4$ obtained analogously as in <cit.>. Each $r_i$ is one of the 75 regexes[<https://github.com/lorisdanto/symbolicautomata/blob/master/benchmarks/src/main/java/regexconverter/pattern%4075.txt>] from RegExLib <cit.>, selected so that $r_1 \land r_2 \land r_3 \land r_4 \land r_5$ is not empty.
Similar kind of these problems is solved in spam-filtering: one tests whether a new filter $r_5$ adds anything new to existing filters.

contains 4 sets of parametric intersection problems from <cit.> and 2 sets from <cit.>. In total, this includes 267 problems.
The parameter controls the size of the regex or the number of regexes to be combined.
is the variant of the benchmark that performs union instead of intersection.

contains 136 language inclusion problems derived from runs of an abstract regular model checker of <cit.> (verification of the bakery algorithm, bubble sort, and a producer-consumer system).

consists of 169 complementation problems created during the run of Amaya <cit.>, a tool for deciding linear integer arithmetic (LIA) formulae
using an automata-based decision procedure of <cit.>.

The formulae are taken from UltimateAutomizer <cit.> and tptp <cit.> benchmarks, collected in SMT-LIB <cit.>.

The transition relation in Amaya is represented symbolically using BDDs; in our experiments we tested both symbolic representation (in ) and explicit representation (in ), where explicit symbols are bit vectors represented by the BDDs.

consists of instances created during the run of the string solver <cit.> on the regex-heavy benchmark AutomatArk <cit.> from SMT-LIB <cit.>. We collected 751 complementation, 438 concatenation, and 4,872 intersection problems in , , and respectively.

Experimental setup.
We converted all benchmarks into a common textual automata format

(the .mata format, see <ref>),
and wrote dedicated parsers or conversions for all the libraries.
The conversion and parsing are not included in the run times since the parsers are not optimized and the typical use cases do not require parsing every input automaton from a textual format. From some of the benchmarks, we excluded small units of examples where the conversion failed.
We measure only the time needed for carrying out the specified operations on automata already parsed into  each library's internal data structures.

Automata in all benchmarks but and those coming from regexes, , , , and , had small or moderate alphabet sizes (all below 100 symbols, except with up to 252 symbols).

The explicit automata from LIA solving () have at most 1,024 symbols (corresponding to 10 bits).[It should be noted that these LIA problems are by no means representative of typical LIA formulae, which could generate much larger alphabets and transition relations that require some sort of symbolic representation.]

After performing mintermization on automata with symbolic representation (), the number of symbols was reduced to at most 30,

and mintermization runs on automata from regular expressions

returned alphabets with at most 80 symbols.

We summarize the results of each benchmark in cactus plots in <ref> (displaying cumulative run times of benchmarks, with the instances ordered by their run time) and <ref>. <Ref> shows relative speedups of over each library on problem instances that both libraries finished in time.

We also present statistics for individual automata operations across the entire benchmark in <ref> and <ref>.

We do not show the performance of 's Python interface in the plots and tables as it is matches that one of .

All examples were run in six parallel jobs on Fedora GNU/Linux 38 with an Intel Core 3.4 GHz processor and 20 GiB RAM with 60 s timeout.

consistently outperforms all other libraries on all benchmarks and in all operations, up to few exceptions. It is sometimes matched or outperformed by and in union and concatenation operation (on and ).
and are sometimes faster since they may be able to share parts of the representation (such as BDDs on the transitions) between the automata operands and the union/concatenation, while copies the entire data structure (and the memory locality of , with its three layers of vectors, is not perfect).

appears particularly fast in emptiness checking since it implicitly trims the automata, after which the emptiness test becomes a trivial query on emptiness of the set of states.
The cost of the emptiness check is thus hidden in the cost of other operations (we do not state statistics from trimming for for this reason).

and also have a smaller average time in constructing the complements in $\bpressym$, due to a few high run times of on examples that have many transitions per a pair of states. Solving these examples, and generally examples generated from solving LIA, is indeed a case for symbolic representation of transitions, and it is currently not a primary target of . However, is still much faster than any other library on mintermised versions of the same examples.
is faster in some parametric intersection examples because of its implicit determinization, which in some particular examples returns much smaller automata. When the other libraries are made to determinize, they behave analogously, and again solves most examples and takes the least time.

Still, on all operations except emptiness, is the fastest overall, and on emptiness it is by far the fastest from libraries that actually do solve the emptiness problem.

has especially efficient inclusion test, and trimming, an operation which is usually needed very frequently, is also a strong point of 's performance.

's simulation reduction (in the results) does not help much when the time for computing the simulation is counted in, as seen in <ref>.
Simulation reduction is indeed costly, and our eager strategy of reducing all automata is probably sub-optimal. The run times of complement, however, show a considerable speedup after automata are reduced, and solves some complement and also parametric intersection examples that no other library can.

Overall, appears significantly faster than all the libraries we have tried, with the closest competitor being often more than an order of magnitude slower.

Statistics for the operations on solved instances.
We list the average time (Avg), median time (Med), and standard deviation (Std), with the best values in bold.
The times are in milliseconds.

Note that only the operations that the given library finished within the timeout are counted, hence the numbers are significantly biased in favour of libraries that timeouted more (the harder benchmarks are no counted in), and should be red in the context of <ref> and the cactus plots.

We use to denote a value close to zero.

Threats to validity. Our results must be taken with a grain of salt
as the experiment contains an inherent room for error.

Mainly, not knowing every library intimately,
we might have missed the most optimal solutions,
and our parsers of the .mata format
might be building the internal data structures of the libraries in a sub-optimal way.

The experiment was also running in parallel on a server with limited resources,
which might lead to fluctuations in run times

We are, however, confident that our main conclusions are well justified.

§ CONCLUSIONS AND FUTURE WORK

We have introduced a new automata library , explained its principles, and evaluated its performance.
is not the most general or feature-full library. Libraries such as or are much more complex and comprehensive, are more widely applicable, either to various symbolic representations of automata or to automata with registers, while still being impressively efficient.
, however, does what it is meant to do better than all the other libraries: solve examples from string solving, regular expression processing, and regular model checking much faster, while staying simple and transparent, easily extensible and applicable to projects.

We continue working on 's set of features as well as its efficiency.
We plan to extend with transducers, add support for registers that could handle, e.g., counting in regular expressions, and experiment with the poor man's symbolic representation of bit vector alphabets represented as sequences of bits (used in  <cit.>), so that can be used adequately in applications such as solving WS1S and arithmetic formulae.
We believe that the efficiency of the basic data structures discussed here can be much improved by focusing on the low-level performance. Custom data structures, specialised memory management, improvement in memory locality, and, generally, the class of optimizations used in BDD packages, could shift 's performance much further.