LSV Seminar

Date

Tuesday, December 03 2013 at 11:00AM

Place

Salle de Conférence (Pavillon des Jardins)

Speaker

Thomas Colcombet (LIAFA, Université Paris Diderot)

This talk will be the occasion to give an introduction to regular cost-functions, to describe the main concepts involved, to give an overview of the known results and open problems, and to show some applications.

The theory of regular cost-functions offer a quantitative extension to the notion of regular language. Regular cost-functions can count, for instance the number of occurrence of some patterns, and can optimize quantities (for instance compute nested infima and suprema). In particular, some notions of resource consumption can be easily expressed using regular cost-functions. Regular cost-functions can be used over words, finite of infinite, or trees, finite or infinite (though infinite trees are only partially understood so far).

As it is the case for regular languages, this theory comes with several decision procedures and many forms of effectively equivalent computational models such as automata (B-automata and S-automata), algebra (stabilisation monoids), expressions (B-expressions and S-expressions), or logics (cost-monadic second-order logic). These results strictly extend their classical language counterparts.

The theory of regular cost-functions continues and uses the techniques and results developed formerly by Hashiguchi, Leung, Simon and Kirsten since the early eighties. At the same it provides a uniform and more general framework for understanding all these works.

The central question addressed by regular cost-functions is the ability to decide the existence of a bound on the range of some finitely represented function. On the one hand, only concentrating on bounds may be seen as a severe restriction (but otherwise, decidability would be immediately lost). On the other hand, many problems in computer science, or in mathematics turn out to be reducible to questions of existence of bounds on some quantities. For this reason, several non-trivial problems can be shown decidable by reduction to cost-function decision procedures. Let us cite for instance the finite power property (given a regular language L, does there exist n such that L^n=L*), the star height problem (given a regular language L and an integer k, is it possible to write L as a regular expression using at most k nesting of Kleene stars) and its extension to trees, the finite substitution problem, the problem of finitely unfolding fixpoints of MSO formulae while preserving their semantics, some quantitative variants of the Church synthesis problem, or the decidability of the Rabin-Mostowski hierarchy (a problem only partially solved so far).