Decidable weighted expressions with Presburger combinators

摘要

In this paper, we investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, we consider a slight extension of an expression formalism, introduced by Chatterjee et al. in the context of infinite words, in order to combine values given by unambiguous sum-automata, using Presburger arithmetic. We show that important decision problems such as emptiness, universality, inclusion and equivalence are PSpace-C for these expressions. We then investigate the extension of these expressions with Kleene star. This allows to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems turn out to be undecidable, but we introduce a decidable and still expressive class of synchronised expressions.