Where automatic structures benefit from weighted automata

Abstract

In this paper, we report on applications of weighted automata in the theory of automatic structures. All (except one) result were known before, but their proof using weighted automata is novel. More precisely, we prove that the extension of first-order logic by the infinity ∈ ∈∞∈, the modulo ∈ (p,q), and the (new) boundedness quantifier is decidable. The first two quantifiers are handled using closure properties of the class of recognizable formal power series and the fact that the preimage of a value under a recognizable formal power series is regular if the semiring is finite. Our reasoning regarding the boundedness quantifier uses Weber's decidability result of finite-valued rational transductions. We also show that the isomorphism problem of automatic structures is undecidable using an undecidability result on recognizable formal power series due to Honkala. © 2011 Springer-Verlag Berlin Heidelberg.