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
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.
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.
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.
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.
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
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.