Logic and regular cost functions
Thomas Colcombet · Logic in Computer Science · 2017
Regular cost functions offer a toolbox for automatically solving problems of existence of bounds, in a way similar to the theory of regular languages. More precisely, it allows to test the existence of bounds for quantities that can be defined in cost monadic second-order logic (a quantitative variant of monadic second-order logic) with inputs that range over finite words, infinite words, finite trees, and (sometimes) infinite trees.Though the initial results date from the works of Hashiguchi in the early eighties, it is during the last decade that the theory took its current shape and that many new results and applications have been established.In this tutorial, two connections linking logic with the theory of regular cost functions will be described. The first connection is a proof of a result of Blumensath, Otto and Weyer stating that it is decidable whether the fixpoint of a monadic second-order formula is reached within a bounded number of iterations over the class of infinite trees. The second connection is how non-standard models (and more precisely non-standard analysis) give rise to a unification of the theory of regular cost functions with the one of regular languages.