Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

Nathanaël Fijalkow, Bastien Maubert, and Moshe Y. Vardi

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

Step 1: Prompt LTL to Prompt Automata
Step 2: History-determinisation of Prompt Automata
Step 3: Domination Games

LTL (Reactive) Synthesis

Originates from Church's synthesis problem: given a (Boolean) specification $\phi$ over $$(I \times O)^\omega$$ construct a reactive system $S : I^+ \to O$ satisfying $\phi$: for all $w = i_0 i_1 \dots \in I^\omega$:
$$\begin{array}{ccccccc} \text{input} & i_0 & i_1 & i_2 & \dots \\ \text{output} & S(i_0) & S(i_0 i_1) & S(i_0 i_1 i_2) & \dots \end{array}$$

Classical Solution

Determinisation is required and crucial!

Prompt LTL

(Kupferman, Piterman, Vardi 2009)
LTL (simplified) syntax: Boolean formulas plus $\mathbf{X} \phi$ and $\mathbf{F} \phi$
$w,i \models \phi$ reads ``w satisfies $\phi$ from position $i$''

Prompt LTL extends LTL with $\mathbf{F}^{B} \phi$
$\mathbf{F}^{B} \models \phi[N]$ reads ``$\phi$ holds within the next $N$ positions''
$w,i \models \mathbf{F}^{B} \phi$ if there exists $N \in \mathbb{N}$ such that $w,i \models \mathbf{F}^{B} \phi[N]$

The Alternating Colour Technique

(Kupferman, Piterman, Vardi 2009)

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

Assume-Guarantee Synthesis

(Alur, Henzinger 1999)
An AG specification is $$A \implies G$$ where $A$ is over $I^\omega$ and $G$ over $(I \times O)^\omega$

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

For Prompt LTL implies an alternation of bounds: A system $S : I^+ \to O$ satisfies $(A,G)$ if for all $w \in I^\omega$, $$(\exists N \in \mathbb{N}, w \models A[N]) \implies (\exists N' \in \mathbb{N}, S(w) \models G[N'])$$
The alternating colour technique does not suffice!
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.

Assumption (over $I$):
  • The server is up infinitely many times;
  • There are infinitely many sessions.

Guarantee (over $I \times O$):
  • In each session each user who requests access is eventually granted access, or the session ends;
  • The server does not grant access when it is down.
Write $A,G$ for the LTL formulas above, and $A',G'$ for their Prompt LTL refinements:
Three systems:
  • Never grants access: satisfies LTL specification because every session ends!
  • LIFO: grants access to the user who made the latest unanswered request: does not satisfy $A' \implies G'$
  • FIFO: grants access to the user who made the earliest unanswered request: satisfies $A' \implies G'$

Regular cost functions

(Colcombet, 2009)
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

Main result

Theorem: Assume-Guarantee Synthesis for Prompt LTL is 2-EXPTIME complete (same complexity as for LTL).

The solution mimics the classical solution using the three steps: translate to automata, determinise, and solve a game.
(almost Kuperberg and Vanden Boom 2012 and 2014)

A Prompt 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!)
(continues Colcombet 2013, extends Colcombet and F. 2016)

A Prompt automaton $\mathcal{A}$ is history-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). \]
Note that the definition is non-uniform: $\sigma$ depends on $N$!

Theorem: For every Büchi Prompt automaton with $n$ states, there exists an equivalent history-deterministic parity Prompt automaton with $2^{O(n \log(n))}$ states.
(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.