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

• $(a + b^*)^* + a b^*$ has star-height $2$
• $a^* b^* + (ba)^*$ has star-height $1$

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
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\}$$

## The bounding quantifier

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

## 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$$

## 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$$

## 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!

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

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