Nathanaël Fijalkow

CNRS, LaBRI, Bordeaux, and The Alan Turing Institute of data science, London

Workshop on the theory of regular cost functions

Main objective


Develop algorithms for answering boundedness questions

Input: $L$ a language
Question: $$\exists N \in \mathbb{N}, \forall w \in L, w \text{ has at most } N \text{ consecutive } a's$$

Invitation au voyage


Main point: the theory of regular cost functions gave solutions to problems in automata theory, database theory, logic...

Second point: it turned out that the theory of regular cost functions is a very conservative extension of classical automata theory: (almost) every notion is reflected here!

The consequence is that it requires deeply understanding (hence revisiting) automata theory!
History-deterministic automata

1990


Star-height problem: given a regular language $L$, what is the minimal star-height of a regular expression denoting $L$?

Cost automata

Theorem (Hashiguchi): the star-height problem can be reduced to the boundedness problem of cost automata word read "" counter value = 0 word read "b" counter value = 0 word read "ba" counter value = 1 word read "baa" counter value = 2 word read "baaa" counter value = 3 word read "baaab" counter value = 3
Induces   $f : A^* \to \mathbb{N} \cup \{ \infty \}$ $$f(w) = \text{min} \left\{ \text{max} \text{ counter value in } \rho \mid \rho \text{ accepting run} \right\}$$

2004

2006

The bounding quantifier

$$\mathbb{B}X \phi(X)\ \doteq\ \exists N \in \mathbb{N}, \forall X, \phi(X) \implies \text{Card}(X) \le N$$

Study of $\omega$BS-automata

2009

cost-MSO


Restriction of MSO + $\mathbb{B}$: no alternation of $\forall X$ and $\exists N \in \mathbb{N}$

Cost-MSO: MSO + $\text{Card}(X) \le N$ (positively)

Boundedness problem for cost-MSO

Input: $\phi$ cost-MSO formula
Question: $$\exists N \in \mathbb{N}, \forall x,\ x,N \models \phi$$

Main result


A non-example

$$f(w) = \text{min} \left\{ \text{max} \text{ counter value in } \rho \mid \rho \text{ accepting run} \right\}$$ $$f(a^{n_1} b a^{n_2} b \cdots a^{n_k} b) = \text{min}\ n_\ell$$ word read "" counter value = 0 (max = 0) counter value = 0 (max = 0) word read "a" counter value = 0 (max = 0) counter value = 1 (max = 1) word read "aa" counter value = 0 (max = 0) counter value = 2 (max = 2) word read "aaa" counter value = 0 (max = 0) counter value = 3 (max = 3) word read "aaab" counter value = 0 (max = 0) counter value = 3 (max = 3) word read "aaaba" counter value = 1 (max = 1) counter value = 3 (max = 3) word read "aaabaa" counter value = 2 (max = 2) counter value = 3 (max = 3) word read "aaabaab" counter value = 2 (max = 2) counter value = 3 (max = 3)

An example

$$f(a^{n_1} b a^{n_2} b \cdots a^{n_k} b) = \text{min}\ n_\ell$$ Promise: $f(w) = 2$. Non-determinism is resolved on-the-fly! word read "" counter value = 0 (max = 0) word read "a" counter value = 1 (max = 1) word read "aa" counter value = 2 (max = 2) word read "aaa" counter value = 0 (max = 2) word read "aaab" counter value = 0 (max = 2) word read "aaaba" counter value = 1 (max = 2) word read "aaabaa" counter value = 2 (max = 2) word read "aaabaab" counter value = 0 (max = 2)

Feel-good movie and paper

History-deterministic B-automata

Start from $\mathcal{A}$ a B-automaton.
We construct an equivalent history-deterministic B-automaton as composition of:
  • A history-deterministic automaton $\mathcal{B}$ that inputs letters and outputs a run tree.
  • A deterministic B-automaton $\mathcal{C}$ that inputs a run tree and checks whether all paths have small values.

The key idea

Look at it backwards!
Positionality for B-games
implies that
$\mathcal{B}$ is history-deterministic

Application:

Assume-Guarantee Synthesis for Prompt LTL


Prompt LTL: LTL + $F^{\le N}$

Input: $\phi,\psi$ prompt LTL formulae
Question: construct a system $S$ such that $$\forall N \in \mathbb{N}, \exists N' \in \mathbb{N},\ \ S,N \models \phi \implies S,N' \models \psi$$
Theorem: (F., Maubert, Vardi)
Assume-Guarantee Synthesis for Prompt LTL is effective