# Decidable Weighted Expressions with Presburger Combinators

## TL;DR

This paper explores the expressive power and decision problems of weighted expressions combining automata and Presburger arithmetic, introducing a decidable class of synchronized expressions despite the undecidability of extensions with Kleene star.

## Contribution

It extends existing weighted expression formalism with Presburger combinators, analyzes their decision problems, and introduces a decidable class of synchronized expressions.

## Key findings

- Decision problems are PSpace-complete for the extended expressions.
- Extending with Kleene star leads to undecidability.
- Synchronized expressions form a decidable and expressive subclass.

## Abstract

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, by which to combine values given by unambiguous (max,+)-automata, using Presburger arithmetic. We show that important decision problems such as emptiness, universality and comparison 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 the decidable and still expressive class of synchronised expressions.