Efficiently Testing Emptiness of Automata on Linear Orderings

Automata on linear orderings are a type of finite-state automata introduced by Bruyère and Carton, that unify and broadly extend the usual finite-state automata on finite words, (bi-)infinite words, and ordinal words. These automata read words indexed by linear orderings, defined as mappings from the elements of any linear ordering to a finite alphabet. Several authors have studied the emptiness problem for these automata, on several domains, mainly to obtain decision procedures for some logics. The resulting algorithms are polynomial. In this paper, we review them and provide new algorithms, whose complexity is improved by one power in time and space. In particular, their space complexity is linear.