Workshop on the theory of regular cost functions, and beyond

Friday 21 September afternoon 2018, Berlin

Satellite event of Highlights of Logic, Games, and Automata

Organised by Laure Daviaud, Nathanaël Fijalkow, and Denis Kuperberg

The theory of regular cost functions is a quantitative extension of the theory of rational languages. Languages (which can be viewed as Boolean functions on words) are replaced by functions, which map words to natural integers and are characterized by boundedness properties. Automata, rational expressions, MSO logic and syntactic monoids all have their counterparts in the theory of regular cost functions.

The study was initiated by Thomas Colcombet in the 2009 ICALP paper showing an exact correspondence between B-automata (and S-automata), cost-MSO, and stabilisation monoids. This was inspired by works of Hashiguchi, Leung, Simon, and Kirsten and related to more recent works by Bojańczyk, Colcombet, and Löding, to study the star-height problem and more generally so-called ''boundedness problems'' (e.g. boundedness of distance automata).

The theory of regular cost functions blossomed in the past 10 years, leading to new insights with applications in automata theory, games, logic, and database theory. The goal of this workshop is to survey some of the results and to discuss new research directions.

Programme

Nathanaël Fijalkow: A simple construction for history-deterministic automata
Speaker:
Nathanaël Fijalkow
Abstract:
The theory of regular cost functions over finite words extends the crisp relationship between finite automata, monadic second-order logic, and semigroups, to a quantitative setting. A key technical notion to achieve this is that of history-deterministic automata.

In this talk, I will show a simple construction for history-deterministic automata based on a correspondence with automata over infinite words. This is a joint work with Thomas Colcombet published in ICALP 2016.
Slides:
HTML
Christof Löding: Regular Cost Functions on Infinite Trees
Speaker:
Christof Löding
Abstract:
Regular cost functions on infinite trees are defined in terms of a variant of distance-desert automata or B-automata using a parity condition in combination with set of counters that can be incremented, reset, or left unchanged in the transitions of the automaton. Such an automaton assigns a value to each tree that it accepts (a natural number or infinity). The central problem for these automata is the boundedness problem: Is the function computed by the automaton bounded on the set of accepted trees?

While this problem is known to be decidable for finite words, finite trees, and infinite words, the problem is still open for infinite trees.

The aim of this talk is to give on overview of known results and tools that have been developed for regular cost functions on infinite trees.
Slides:
PDF
Jean-Éric Pin: Varieties of cost functions: results and open problems
Speaker:
Jean-Éric Pin
Abstract:
This lecture is based on a joint paper with Laure Daviaud and Denis Kuperberg. The goal is to extend standard results on regular languages to the setting of regular cost functions, notably Eilenberg's variety theorem and its consequences.
Slides:
PDF
Damian Niwiński: On positional strategies over finite arenas
Speaker:
Damian Niwiński
Abstract:
This lecture reports on the ongoing work with Thomas Colcombet. We have previously realized that parity condition is essentially the only prefix-independent criterion that guarantees positional determinacy over all arenas. For finite arenas, there are more such criteria, often with quantitative flavour. We propose lexicographic energy condition as an analogue of parity condition for finite arenas, but can prove its universality only under some additional closure assumption, which possibly can be eliminated.
Slides:
PDF
Michał Skrzypczak: On positional strategies over finite arenas
Speaker:
Michał Skrzypczak
Abstract:
A series of works by Thomas Colcombet and Christof Löding proved that a logic called cost-MSO is decidable over a variety of structures. The proofs build upon a number of important concepts, just to mention boundedness games and history determinisation. However, we still lack one decidability result: cost-MSO is not known to be decidable over infinite trees. The importance of this problem is witnessed by a reduction from Rabin-Mostowski index problem to a boundedness problem over infinite trees. The lacking piece of the puzzle is an appropriate finite memory determinacy result, in the spirit of the famous Buchi-Landweber construction. During the talk, I will overview the known results, proving (in)determinacy under finite memory for certain classes of boundedness games.
No Slides!
Blackboard talk
Gabriele Puppis: The cost of equipping languages with infinite data
Speaker:
Gabriele Puppis
Abstract:
Data languages are sets of words where each position carries a letter (data value) from a potentially infinite alphabet. Because data values can be used to represent pointers in a heap, attributes of XML documents, key constraints in a database, etc., data languages have attracted much attention in the recent literature. However, they also pose intriguing questions concerning expressiveness (e.g. to what extent the ideal correspondence between automata, logic, and algebra can be lifted to the setting of data languages?), effectiveness (e.g. which formalisms for data languages have decidable emptiness and equivalence problems?), robustness (e.g. which formalisms are closed under union, complement, projection?).

In this talk I will tell about some recent attempts to identify well-behaved classes of data languages via formalisms based on monoids, logics, and automata. The talk is based on joint works with Thomas Colcombet, Clemens Ley, and Michał Skrzypczak.
Slides:
PDF