Originates from Church's synthesis problem: given a (Boolean) specification $\phi$ over $$(I \times O)^\omega$$ construct a

Translate the LTL formula $\phi$ into a non-deterministic Büchi automaton $\mathcal{A}$Determinise $\mathcal{A}$: construct an equivalent parity automaton $\mathcal{B}$- From $\mathcal{B}$ construct a game where Adam gives inputs and Eve gives outputs,
and
solve it: a winning strategy is a reactive system satisfying $\phi$

LTL (simplified) syntax: Boolean formulas plus $\mathbf{X} \phi$ and $\mathbf{F} \phi$

$w,i \models \phi$ reads ``w satisfies $\phi$ from position $i$''

- $\mathbf{X} \phi$ reads ``$\phi$ holds at the next position''
- $\mathbf{F} \phi$ reads ``$\phi$ holds at some position in the future''

is a reduction from a Prompt LTL formula $\phi$ to an LTL formula $\phi'$ such that:

there exists a system satisfying $\phi$ if and only if there exists a system satisfying $\phi'$

An AG specification is $$A \implies G$$ where

A system $S : I^+ \to O$ satisfies $(A,G)$ if for all $w \in I^\omega$, $$w \models A \implies S(w) \models G$$

AG synthesis for LTL reduces to synthesis for LTL: $A \implies G$ is a formula of LTL

The system runs a server with $k$ users who can request access.
The server may be up or down at each time step.
When the server is up, it can grant access to a user, one at a time.
Additionally, time is divided in sessions: sometimes a session ends, and a new session starts.

Write $A,G$ for the LTL formulas above, and $A',G'$ for their Prompt LTL refinements:

- $A'$ includes: the server is up every $N$ steps for some $N \in \mathbb{N}$;
- $G'$ includes: each user who requests access is granted access within $N'$ steps for some $N' \in \mathbb{N}$.

Instead of considering $$L(\phi) = \{ w \in \Sigma^\omega : \exists N \in \mathbb{N}, w \models \phi[N] \} \subseteq \Sigma^\omega$$ Work with $$\begin{array}{lll} [\phi] : & \Sigma^\omega & \to & \mathbb{N} \cup \{ \infty \} \\ & w & \mapsto & \inf \{ N \in \mathbb{N} : w \models \phi[N] \} \end{array}$$ modulo an equivalence relation: $f \approx g$ if for all $X \subseteq \Sigma^\omega$, $f(X)$ is bounded if and only if $g(X)$ is bounded

The solution mimics the classical solution using the three steps:

(almost Kuperberg and Vanden Boom 2012 and 2014)

APrompt automaton has a counter which can be incremented or reset at each transition.
The value of a run is the maximal value of the counter along the run.

**Theorem**: For every Prompt LTL formula $\phi$, there exists a non-deterministic Büchi Prompt automaton $\mathcal{A}$
such that $[\phi] \approx [\mathcal{A}]$ (but not equal!)

A

(continues Colcombet 2013, extends Colcombet and F. 2016)

A Prompt automaton $\mathcal{A}$ ishistory-deterministic if for all $N \in \mathbb{N}$,
there exists $N' \in \mathbb{N}$ and a function $\sigma : \Sigma^+ \to \Delta$ such that for all $w \in \Sigma^\omega$,
\[
\text{if } [\mathcal{A}](w) \le N, \text{ then } \mathbf{val}(\sigma^\omega(w)) \le \alpha(N).
\]

A Prompt automaton $\mathcal{A}$ is

(revisits Colcombet and Goeller 2016)

Let $\mathcal{A},\mathcal{B}$ history-deterministic parity Prompt automata for the assumption and the guarantee.

We construct a domination game where the objective is: there exists a strategy such that for all $N \in \mathbb{N}$, there exists $N' \in \mathbb{N}$ such that \[ \text{Parity}_{\mathcal{A}} \wedge \text{val}_{\mathcal{A}}[N] \implies \text{Parity}_{\mathcal{B}} \wedge \text{val}_{\mathcal{B}}[N']. \]**Theorem**: Solving domination games is in **EXPTIME**.

Let $\mathcal{A},\mathcal{B}$ history-deterministic parity Prompt automata for the assumption and the guarantee.

We construct a domination game where the objective is: there exists a strategy such that for all $N \in \mathbb{N}$, there exists $N' \in \mathbb{N}$ such that \[ \text{Parity}_{\mathcal{A}} \wedge \text{val}_{\mathcal{A}}[N] \implies \text{Parity}_{\mathcal{B}} \wedge \text{val}_{\mathcal{B}}[N']. \]