Regular Cost Functions, Part I: Logic and Algebra over Words

TL;DR

This paper extends classical regular language theory to regular cost functions, introducing a logical and algebraic framework that enables the analysis of quantitative properties of words, with decidability results for certain problems.

Contribution

It introduces the cost monadic logic and stabilisation monoids, providing a new algebraic and logical foundation for regular cost functions and their decidability properties.

Findings

Defined cost monadic logic as a quantitative extension of MSO logic.

Established equivalences between automata, algebra, and logic for regular cost functions.

Proved decidability of some existence-of-bounds problems within this framework.

Abstract

The theory of regular cost functions is a quantitative extension to the classical notion of regularity. A cost function associates to each input a non-negative integer value (or infinity), as opposed to languages which only associate to each input the two values "inside" and "outside". This theory is a continuation of the works on distance automata and similar models. These models of automata have been successfully used for solving the star-height problem, the finite power property, the finite substitution problem, the relative inclusion star-height problem and the boundedness problem for monadic-second order logic over words. Our notion of regularity can be -- as in the classical theory of regular languages -- equivalently defined in terms of automata, expressions, algebraic recognisability, and by a variant of the monadic second-order logic. These equivalences are strict extensions of the corresponding classical results. The present paper introduces the cost monadic logic, the quantitative extension to the notion of monadic second-order logic we use, and show that some problems of existence of bounds are decidable for this logic. This is achieved by introducing the corresponding algebraic formalism: stabilisation monoids.