Efficient Algorithms for Finite Automata

Nondeterministic finite automata are used in many areas of computer science, including, but not limited to, formal verification, the design of digital circuits or for the representation of a regular language. Their advantages over deterministic finite automata is that they may represent a language in even exponentially conciser way. However, this advantage may be lost if a naive approach to some operations is taken, in particular for checking language inclusion of a pair of automata, the naive implementation of which performs an explicit determinization of one of the automata. Recently, several new techniques for this operation that avoid explicit determinization (using the so-called antichains or bisimulation up to congruence) have been proposed. The main goal of the presented work is to efficiently implement these techniques as a new extension of the VATA library. The implementation has been evaluated and is superior to other implementations in over 90% of tested cases by the factor of 2 to 100