Non-Emptiness Test for Automata on Linear Orderings: an Efficient Implementation

Abstract

Automata on linear orderings are a form of finite-state automata introduced by Véronique Bruyère and Olivier Carton, that generalise the concepts of finite-word, infinite-word, and transfinite-word automata. They accept words indexed by linear orderings, defined as mappings from the elements of such orderings to a finite alphabet. This master’s thesis addresses the problem of deciding whether an arbitrary automaton on linear orderings accepts at least one word. In the scope of implementing a decision procedure for the monadic first-order theory of order over real or rational numbers, we focus on deciding whether a given automaton on linear orderings accepts at least one word indexed by the real or the rational numbers. Our work is based on a decision procedure recently obtained by Bernard Boigelot, Pascal Fontaine and Baptiste Vergain. While the critical step of the original procedure has quadratic cost in the size of the input automaton, the one that we propose is linear. Then, we implement this simplified procedure as a part of the LASH toolset, a C library dedicated to finite-state automata. By means of some examples, we demonstrate that our implementation can handle automata having more that 100,000 states in a matter of a few minutes. Besides this, we introduce a variant of automata on linear orderings that, while preserving the original expressive power, allows the presence of epsilon transitions. The theoretical usefulness of these automata is illustrated by correcting an erroneous construction in the original proof of equivalence between automata on linear orderings and their associated rational expressions.