Efficient Representation and Manipulation of Automata on Linear Orderings

Abstract

Automata on linear orderings have been introduced by Bruyère and Carton as a broad generalization of finite-word, infinite-word and transfinite-word automata. Even though they were first seen as purely mathematical objects, automata on linear orderings can in fact serve as algorithmic tools for decision procedures, e.g., the monadic first-order theory of order on the reals or the rationals. In this context, efficient algorithms and data structures need to be carefully designed to implement and then manipulate these automata. This is the problem addressed in this work. We first show that the most crucial operation to optimize is the product of automata on linear orderings, which consists in computing an automaton that simulates the joint behaviour of several automata. From a theoretical point of view, this problem is intrinsically hard. Nevertheless, we investigate several strategies to implement it efficiently in most practical cases, including in the context of decision procedures. These strategies include both theoretical and practical contributions, that range from the definition of an efficient representation mechanism for automata on linear orderings to an actual implementation, in the C programming language, of these automata and their product operation. We then demonstrate experimentally that it is indeed possible to efficiently manipulate automata on linear orderings algorithmically. This paves the way for an actual decision procedure for the monadic first-order theory of order on the reals or the rationals, which could then lead to applications in verification and SMT solving. In parallel, we extended (together with Thomas Braipson and Bernard Boigelot) the formalism of automata on linear orderings, in order to allow their transitions to be labelled by the empty word. The resulting automata model, i.e., epsilon automata on linear orderings, is a powerful theoretical tool that could ease the developments of new methods involving automata on linear orderings.