Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

1 Introduction

Linear-time Temporal Logic (LTL) is a specification language for formal verification and program synthesis [Pnueli, 1977]. While formal verification aims at verifying the correctness of programs, program synthesis consists in synthesising correctby-construction programs directly from their specification.

The synthesis problem for reactive systems [Pnueli and Rosner, 1989] is as follows: given a finite set of inputs I controlled by the environment, a finite set of outputs O controlled by the system, and a specification ϕ given as an LTL formula over alphabet I ×O, synthesise a reactive system S so that for every environment E, the closed system S||E satisfies ϕ.

The classical solution [Pnueli and Rosner, 1989; Vardi, 1995] goes in three steps. The first step is to construct a non-deterministic B¨uchi automaton A equivalent to ϕ. The second step is to determinise A into a parity automaton B. The third step is to construct and solve a parity game G based on B where Adam picks inputs and Eve picks outputs, such that solving this game is equivalent to the synthesis problem: a winning strategy for Eve yields a system S satisfying the specification. In particular this implies that if there exists a system satisfying the specification then there exists a finite one, given by a finite state Mealy machine.

One shortcoming of LTL is that it cannot bound the waiting time of eventualities. For instance the common requirement that every request (r) should be eventually granted (g), expressed as G(r =⇒ Fg) in LTL, is satisfied even when the waiting time between the moment a request is made and the moment it is granted can grow arbitrarily long. There are various approaches to tackle this shortcoming [Alur et al., 2001]. In this work we are interested in the logic PROMPTLTL [Kupferman et al., 2009] which extends LTL with a "bounded eventually" operator F≤B . This operator expresses an eventuality that should be satisfied within the next B steps, where B is a variable existentially quantified. A formula is satisfied in a model if there exists a value b for B that makes the formula true. For instance, the PROMPT-LTL formula G(r =⇒ F≤B g) expresses that there exists a bound on the waiting time.

Assume-guarantee originates as a modular approach to program verification that allows decomposition of proof obligations (see e.g. [Alur and Henzinger, 1999]). Informally, an assume-guarantee specification consists of two specifications ϕ and ψ. A system S satisfies this specification if whenever it is used in a context that satisfies the assumption ϕ, the guarantee ψ holds on the system or, said differently, for all environments E satisfying ϕ, the composed system S||E satisfies ψ.

Assume-guarantee synthesis is the problem of synthesising a system S satisfying an assume-guarantee specification. We refer to [Maoz and Sa'ar, 2012] for a discussion of practical applications of assume-guarantee synthesis. When considering LTL specifications, assume-guarantee verification and synthesis reduce to classical LTL model checking and synthesis: if ϕ and ψ are LTL formulas, then the assume-guarantee specification is equivalent to the LTL specification ϕ =⇒ ψ. But this is not true for PROMPT-LTL: when we ask that in all environments satisfying the assumption the system also satisfies the guarantee, there is an implicit quantification on the bounds with which the assumption and the guarantee are satisfied: a universal one for the assumption and an existential one for the guarantee. Because in PROMPT-LTL the only quantification on bounds is an existential one at the front of the formula, this alternation is not reflected in the formula ϕ =⇒ ψ and, in fact, cannot be captured by a PROMPT-LTL formula. Classical techniques to handle PROMPT-LTL such as the alternating colour technique [Kupferman et al., 2009] are thus difficult to apply, and the assume-guarantee synthesis problem for PROMPT-LTL has been open for a decade.

The problem of assume-guarantee synthesis for PROMPTLTL as defined above can be called uniform, as the system that one aims at synthesising does not depend on the bounds for which the assumption or the guarantee are satisfied. It was observed in [Jacobs et al., 2018] that this variant of the problem does not always admit finite implementations, as a satisfying system may require memory that depends on the bounds. Also, in the formulation of the problem they consider, the assumption talks about both inputs and outputs, which makes it possible to have solution systems that always falsify the assumption.

To eliminate such unsatisfactory solutions we consider assumptions that only talk about inputs. Also, to account for the fact that a system's memory may depend on the bound for the assumption, we introduce a non-uniform variant of the problem, which asks whether for every bound b on the assumption, there exists a bound b′ on the guarantee and a system Sb such that whenever the assumption is satisfied with bound b, the guarantee is satisfied with bound b′ .

We show that this problem is 2-EXPTIME-complete, hence not costlier than LTL synthesis. When the answer is positive, our solution produces a parameterised system which depends on the bound for the assumption.

We develop an automata-theoretic approach for PROMPTLTL using a subclass of cost automata that we call prompt automata. Cost automata are a type of automata with counters introduced in the theory of regular cost functions [Colcombet, 2009; Colcombet, 2013b], leading to a wealth of results extending many results from automata theory to a quantitative setting [Colcombet, 2013a].

The key difficulty is that prompt automata cannot be determinised, i.e. deterministic prompt automata are strictly less expressive than non-deterministic ones. Our main technical contribution is a history-determinisation procedure for prompt automata. History-determinism relaxes the notion of determinism: in a history-deterministic automaton, the nondeterminism can be resolved on the fly. This property is exactly what is required for later using these automata in a game context as in the usual solution for LTL synthesis.

A benefit of our approach is that it follows the classical route for solving the synthesis problem for LTL via automata, determinisation and game solving, which proved its efficiency in recent editions of the SYNTCOMP event [Jacobs and Bloem, 2018; Jacobs et al., 2019].

Assume-guarantee verification and synthesis have been extended in different directions, such as probabilistic systems [Kwiatkowska et al., 2010] or specifications in quantitative extensions of LTL [Almagor et al., 2017], or multiagent synthesis [Chatterjee and Henzinger, 2007; Fisman et al., 2010; Bloem et al., 2015; Kupferman et al., 2016; Brenguier et al., 2017; Filiot et al., 2018], but it has never been solved for PROMPT-LTL specifications.

Distributed synthesis for PROMPT-LTL was recently studied in [Jacobs et al., 2018], where it is observed that in the asynchronous setting, to define PROMPT-LTL synthesis in a meaningful way one has to resort to assume-guarantee synthesis for PROMPT-LTL, but no solution was provided.

Besides the works already mentioned, PROMPT-LTL has also been studied in relation with logics for strategic reasoning [Aminof et al., 2016; Fijalkow et al., 2018]. In the latter work, cost automata are used to solve an extension of Strategy Logic that subsumes PROMPT-LTL. However, even if this logic has in its syntax quantification on strategies and quantification on bounds, it cannot express assume-guarantee synthesis. The reason is that a syntactic constraint in the logic forbids alternation of quantification on bounds, inherent in assume-guarantee synthesis for PROMPT-LTL.

In Section 2 we define PROMPT-LTL. We define the assume-guarantee synthesis problem in Section 3 and present an example in Section 4. The first step of our solution, translating PROMPT-LTL formulas into prompt automata, is described in Section 5. The second step, history-determinisation of these automata, is developed in Section 6. The main ingredient of the third step is domination games, presented in Section 7. We wrap up and prove our main result in Section 8.

2 Prompt Linear Temporal Logic

We write [i, j] for the interval {i, i +1, . . . , j -1, j}, and we use parentheses to exclude extremal values, so that [i, j) is {i, i +1, . . . , j -1}. For an alphabet Σ, the set of finite words over Σ is Σ∗ and the set of infinite words is Σω . If w = a0a1a2 · · · ∈ Σω is an infinite word over Σ and i ∈ N, then we let wi = ai and w≤i = a0 . . . ai.

Definition 1. The syntax of PROMPT-LTL formulas over the alphabet Σ is given by the following grammar:

In the examples we use the classical additional operators F and G ("eventually" and "always"), both definable using the operators above. The size of a formula is defined classically as the size of the syntactic underlying tree denoting the formula.

PROMPT-LTL formulas are evaluated on infinite words at a position i ∈ N on the word and with a bound b ∈ N. The semantics is defined by induction with w ∈ Σω and i, b ∈ N. All cases are as for LTL, except for the following one:

An execution w ∈ Σω satisfies a formula ϕ for the bound b ∈ N, which we write w, b |= ϕ, if w, 0, b |= ϕ.

3 Assume-Guarantee Synthesis

Let I and O be finite sets of inputs and outputs respectively, which can be thought of as valuations over sets of input and output variables. We consider synchronous systems: at each time step the environment produces an input i ∈ I and the system reacts by producing an output o ∈ O. A system is a function S : I + → O that maps each nonempty finite sequence of inputs to an output. An infinite word over I ×O is called an execution. Given an infinite sequence of inputs w = a0a1a2 · · · ∈ I ω , we define the execution of S on w as S(w) = (a0, b0)(a1, b1)(a2, b2) . . . where for each i ≥ 0, bi = S(w≤i) is the output after the sequence of inputs w≤i.

An assume-guarantee (AG) specification is a pair of formulas (ϕ, ψ), with ϕ over the alphabet I and ψ over the alphabet I × O. We study the following decision problem, which we call (non-uniform) assume-guarantee synthesis problem [Pnueli, 1985; Kupferman et al., 2009]: for all b ∈ N, there exists b′ ∈ N and a system S such that

INPUT: A PROMPT-LTL AG specification (ϕ, ψ) {Yes if there exists a solution for (ϕ, ψ),

OUTPUT: No otherwise.

Our main result in this work is stated below.

Theorem 1. The assume-guarantee synthesis problem for PROMPT-LTL is 2EXPTIME-complete.

4 AMotivating Example

We consider the following scenario, where the goal is to synthesise a system to run a server. There are N users and each user can request access to the server. 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. We first give the specification of the server in natural language in an assume-guarantee form:

Assumption (over I):

• The server is up infinitely many times, and
• there are infinitely many sessions.

Guarantee (over I ×O):

• In each session each user who requests access is eventually granted access, or the session ends;
• and the server does not grant access when it is down.

Formally, the set of inputs is

Here reqi represents a request of user i, ε means that no request is made, up and down are states of the server, and new starts a new session. The set of outputs is

where ansi represents granting access to user i.

We emphasise that whenever a user is granted access to the server, this answers all of their past requests, not only the last one, and the end of a session answers all past requests.

There are two natural systems for the server. Both store the list of users who requested access and grants access to one of them whenever the server is up. The difference is in the order in which access is granted. The FIFO implementation grants access to the user who made the earliest unanswered request, and the LIFO implementation to the user who made the latest unanswered request. Both systems can be described as finite-state systems of size exponential in N.

At an intuitive level, the FIFO implementation is fairer than the LIFO one; let us see how this is reflected in formalising the specification in LTL and PROMPT-LTL.

We can write the specification above in two LTL formulas A and G and consider the LTL synthesis problem for the specification A =⇒ G. The formulas are

Both FIFO and LIFO implementations are correct systems. Since the end of a session answers all requests and there are infinitely many sessions, the system never that never grants any access is also a solution. This is obviously not a satisfactory system, we will see that finer specifications rule it out.

Let us write the guarantee formula G in PROMPT-LTL; the first part becomes: there exists a bound b′ such that in each session, each user who requests access is granted access within b′ steps, or the session ends. Formally, we define the PROMPT-LTL formula

Consider the PROMPT-LTL synthesis problem for the specification A =⇒ G′ . Neither FIFO nor LIFO implementations are correct systems, and indeed there are no solutions to this problem since the server can be down for arbitrarily long consecutive time sequences, which leaves no hope of granting access in bounded time. We refer to the figure on the left hand side in Figure 1 for an illustration of such an environment.

The issue here is that we ask the system to be correct against all environments satisfying A, and there is indeed no way to ensure bounded waiting time if there are no similar timing assumptions on the environment. The assumeguarantee formulation addresses this shortcoming.

We now write the assumption formula also using PROMPTLTL, expressing that there exists a bound b such that the server cannot be down for b consecutive steps. Formally,

Let us look at the PROMPT-LTL synthesis problem for the assume-guarantee specification (A′ ,G′ ). The FIFO implementation satisfies this specification, but the LIFO does not.

Let us first see that the LIFO implementation fails to guarantee a bound: a user can be left wanting for an arbitrary number of steps if another user keeps requesting and getting access to the server. We refer to the figure on the right hand side in Figure 1 for an illustration of this behaviour.

We now analyse the FIFO implementation. Let us consider an environment where the server is up at least once every b consecutive steps. Then inside a session every request will be granted within b′ = b · N steps, where N is the number of users. This is because a user only goes down in the list of unanswered requests and becomes the earliest unanswered request after at most N steps where the server is up. This example shows the essence of PROMPT-LTL assume-guarantee specification: how a timing assumption on the environment transfers to a timing guarantee on the system.

5 Prompt Automata

In this section we show how to translate PROMPT-LTL to prompt automata. We first recall the notion of cost functions, introduce prompt automata, and then present the translation. Let us fix Σ, Ω finite alphabets.

The first key conceptual idea is to reason with cost functions instead of languages. The usual way of reasoning semantically with a formula ϕ is to consider the language it defines by L(ϕ) = {w ∈ Σω : ∃b ∈ N,w, b |= ϕ}. Instead, we will consider a more precise object. We first define JϕK : Σω → N ∪ {∞} by

The function JϕK carries too much information: it gives the smallest value b ∈ N for each word w such that w, b |= ϕ. The foundational idea of the theory of regular cost functions [Colcombet, 2009; Colcombet, 2013b] is to use approximation: instead of considering functions Σω → N ∪ {∞}, we consider such functions up to an equivalence relation ≈ which informally says "two functions are equivalent if they are bounded on the same sets". Formally, for f, g : Σω → N ∪ {∞}, we say that f ≈ g if for all X ⊆ Σω , f(X) is bounded if and only if g(X) is bounded, where f(X) is bounded means that f(X) ⊆ [0, b] for some b ∈ N. The theory of regular cost functions replaces the notion of functions Σω → N∪ {∞} by cost functions: a cost function is an equivalence class for the relation ≈.

From now on functions are always considered up to the equivalence relation ≈. In particular, a formula of PROMPTLTL or an automaton defines a cost function, which is the equivalence class of the function it defines. Consequently, we say that two automata are equivalent if they define the same cost functions, although they may define different functions.

The approximation ≈ is appropriate for the assumeguarantee synthesis problem for PROMPT-LTL, since it is a boundedness problem that does not specify exact values.

A finite word λ ∈ {i, r}∗ is a sequence of counter operations: the counter is initialised with value zero, so val(ϵ) = 0, it is incremented by one using i, so val(λi) = val(λ) + 1, and reset to zero using r, so val(λr) = 0.

Desert : {i, r}ω → N ∪ {∞} is the supremum value of the counter, defined by

A cost function f with domain {0, ∞} is called a language, and is equally given as L = f -1 ({0}) ⊆ Σω . Note that for two languages L,L′ seen as functions, L = L′ is equivalent to L ≈ L′ . We say that λ satisfies L if f (λ) = 0, equivalently if λ ∈ L. We write ¬L for the complement of L, meaning Σω \ L. A function f : Σω → N ∪ {∞} and a bound b ∈ N induce a language f[b] = {λ ∈ Σω : f(λ) ≤ b}.

The parity language Parity uses alphabet [1, d] and is defined as the set of words in [1, d]ω such that the maximal priority appearing infinitely many times in λ is even. The special case where d = 2 yields B¨uchi language and is written B ¨uchi.

We use ∧ and ∨ to combine functions over products of labels, where ∧ is the maximum and ∨ the minimum. For instance, Parity ∧ Desert is a function over the set of labels [1, d] × {i, r} defined by

where λ(1) is the projection of λ on [1, d]ω and λ(2) the projection on {i, r}ω . Since Parity is a language, if λ satisfies parity then (Parity∧Desert)(λ) = Desert(λ), and otherwise (Parity ∧ Desert)(λ) = ∞.

Let f : Ωω → N ∪ {∞} a function. A (non-deterministic) f -automaton over the alphabet Σ is a tuple A = (Q, Qinit, ∆) where Q is a finite set of states, Qinit ⊆ Q a set of initial states, and ∆ ⊆ Q × Σ × Ω × Q is a transition relation.

Let q a state and a a letter. We call a-transitions the elements of Q × {a} × Ω × Q, and a-transitions from q the elements of {q} × {a} ×Ω×Q. We assume that automata are complete: for every state q and letter a there exists at least one a-transition from q.

A run over the finite or infinite word w = a0a1 . . . is a sequence ρ = δ0δ1 . . . of matching length consisting of consecutive transitions such that for all i, δi is an ai-transition and ρ starts from a state in Qinit. We extend f to infinite runs by letting f(ρ) = f(λ), where λ is the projection of ρ on the set of labels Ω. An f-automaton induces the function

If f is a language L, then the function JAK takes only values 0 and ∞ so it is also a language, so considering L(A) = {w ∈ Σω : JAK(w) = 0} we recover the usual definition of the language accepted by A. In this case, an Lautomaton is a non-deterministic automaton with acceptance condition L: a word is accepted if there exists a run in L, which we call an accepting run.

An automaton is deterministic if it has a unique initial state and for every state q there exists at most one (hence a unique) a-transition from q: then the transition relation becomes a function δ : Q×A→Ω×Q.

A Parity ∧ Desert-automaton is called a prompt automaton, and a B¨uchi∧Desert-automaton is called a B¨uchi prompt automaton. The Desert function over finite words was introduced independently in [Bala, 2004] and [Kirsten, 2004]. Prompt automata are a special case of B-automata [Colcombet, 2009] that corresponds over finite words to the notion of temporal cost automata [Colcombet et al., 2010].

Kuperberg and Vanden Boom showed that the classical translations from LTL to non-deterministic [Kuperberg, 2014] and alternating [Kuperberg and Vanden Boom, 2012] automata can be extended to COST-LTL and cost automata, which subsume PROMPT-LTL and prompt automata. We can easily adapt their translation to obtain the following:

Theorem 2. For every formula ϕ of PROMPT-LTL of size n, there exists a B¨uchi prompt automaton A of size O(2n ) such that JAK ≈ JϕK.

Compared to the classical translation from LTL to nondeterministic automata, the main difference is that when a state contains a subformula F≤B ψ, the automaton nondeterministically chooses between checking that ψ holds or postponing it to the next step and incrementing the counter.

6 History-Determinisation

Here we show how to construct a history-deterministic prompt automaton equivalent to a given prompt automaton.

Deterministic prompt automata are strictly less expressive than non-deterministic ones, which is a major issue in extending the classical solution to the synthesis problem from LTL to PROMPT-LTL. Indeed, recall that in this approach the second step is to turn a non-deterministic (B¨uchi) automaton into a (parity) deterministic one, before constructing a game equivalent to the synthesis problem for the LTL formula. This last construction would fail for non-deterministic automata. The solution comes from the notion of history-deterministic automata, which is a relaxation of deterministic automata that is tailored exactly to make the game construction work [Henzinger and Piterman, 2006].

Informally, a non-deterministic automaton is historydeterministic if its non-determinism can be resolved by a function σ : Σ+ → ∆ considering only the input read so far. In other words, σ reads the word letter by letter and constructs a run: for w ∈ Σ+, the choice of the next transition is σ(w) ∈ ∆. Hence σ induces a function σω : Σω → ∆ω picking a run σω (w) for a word w ∈ Σω .

Definition 2. An f-automaton A is history-deterministic if there exists a correction function α such that for all b ∈ N, there exists a function σ : Σ+ → ∆ such that for all w ∈ Σω , if JAK(w) ≤ b, then f(σω (w)) ≤ α(b).

There exists a direct procedure for history-determinisation of cost automata over finite words [Colcombet and Fijalkow, 2016], yielding a single-exponential (optimal) blow-up in size. Extending this construction to infinite words is an open problem whose solution would have interesting consequences for the theory of regular cost functions. The construction relies on the use of a determinisation procedure for classical automata (for instance, Safra's construction). Theorem 3 below is a partial answer to this problem: it extends the result given in [Colcombet and Fijalkow, 2016] to infinite words, but only for prompt automata (a strict subclass of cost automata). The key idea in our construction is reminiscent of the alternating colour technique [Kupferman et al., 2009], which Colcombet, Kuperberg, and Lombardy [Colcombet et al., 2010] used in the context of temporal cost automata for showing the equivalence between the two dual models of automata.

Theorem 3. For every B¨uchi prompt automaton with n states, there exists an equivalent history-deterministic prompt automaton with 2O(n log(n)) states and O(n) priorities.

We sketch the proof of Theorem 3.

Let A a B¨uchi prompt automaton with n states. Following [Colcombet et al., 2010], we define a clock to be an infinite word over the alphabet {ε, tick}, and for a clock c we let Desert(c) = Desert(λ), where λ ∈ {i, r}ω is obtained from c by replacing each ε with i and each tick with r. The alternating colour technique is based on the following two key observations: let ρ a run over w,

Fact 1. If Desert(ρ) ≤ b, then the counter in ρ is reset between every tick of the clock cb = εb tick εb tick . . .

Fact 2. If there is a clock c with Desert(c) ≤ b such that ρ resets between every tick in c, then Desert(ρ) ≤ 2b.

Intuitively, these two facts imply that Desert can be replaced by the property that there exists a clock c such that the counter in ρ is reset between every tick in c. The benefit of this replacement is that the latter is a regular property, hence a reduction from a quantitative property to a qualitative one.

Let w ∈ Σω and c ∈ {ε, tick}ω a clock, we write w ⊗ c for the word over alphabet Σ × {ε, tick} that projects on w and c. Let us define LA as the language of words of the form w ⊗ c such that there exists a run ρ of A over w satisfying B¨uchi and such that the counter is reset between every tick in c. Define also

Note that fA ≈ JAK, hence the following lemma proves the first half of Theorem 3.

Lemma 1. There exists a history-deterministic prompt automaton B recognising fA with 2O(n log(n)) states and O(n) priorities.

7 Domination Games

An Ω-labelled graph G = (V, E), or simply graph when Ω is clear from the context, is given by a set V of vertices and a set E ⊆ V × Ω × V of labelled edges: if (v, ℓ, v′ ) ∈ E, then there is an edge from v to v′ labelled by ℓ ∈ Ω and we say that v is the origin vertex of the edge (v, ℓ, v′ ), and v′ is its destination vertex. A path π is a (finite or infinite) sequence of consecutive edges (v, ℓ, v′ ) in E. We write π = (v0, ℓ0, v1)(v1, ℓ1, v2) · · · and πi = (vi, ℓi, vi+1). We also let π<i denote the prefix of π of length i, meaning π<i = π0 · · · πi-1. For a qualitative function W ⊆ Σω , we say that a path π satisfies W if λ(π) ∈ W, where λ(π) is the projection of π on the labels.

An Ω-labelled game G = (V,E, vinit,VEve,VAdam), or game, is a finite Ω-labelled graph G = (V,E) together with an initial vertex vinit ∈ V and two sets VEve and VAdam such that V = VEve⊎VAdam. The interaction between the two players goes as follows. A token is initially placed on the initial vertex vinit, and the player who controls this vertex pushes the token along an edge, reaching a new vertex; the player who controls this new vertex takes over, and this interaction goes on potentially forever, describing an infinite play.

A strategy is a map σ : E∗ → E. We say that a play π is consistent with a strategy σ for Eve (resp. for Adam) if for all i ≥ 0 such that vi ∈ VEve (resp. vi ∈ VAdam), we have σ(π<i) = πi.

We define strategies with memory. We let G = (V,E, vinit,VEve,VAdam) be a game. A memory structure M = (M,minit, µ) for G consists of a set M of memory states, an initial memory state minit ∈ M, and an update function µ : M × E → M. A memory structure is similar to an automaton synchronised with the game: it starts from minit and reads the sequence of edges produced by the game. Whenever an edge is taken, the current memory state is updated using the update function µ. A strategy relying on a memory structureM, whenever it picks the next move, considers only the current vertex and the current memory state: it is thus given by a next-move function σ : VEve ×M → E.

The notion of domination games was introduced for the study of the domination between cost functions [Colcombet, 2013a]. A domination game is a game G over the set of labels ([1, d1] × {i, r}) × ([1, d2] × {i, r}). A play π induces two projections: π1 ∈ ([1, d1] × {i, r})ω and π2 ∈ ([1, d2] × {i, r})ω . Eve wins a domination game if for all b ∈ N, there exists b′ ∈ N and a strategy σ for Eve such that all plays π consistent with σ satisfy

(Parity ∧ Desert)(π1) ≤ b ⇒ (Parity ∧ Desert)(π2) ≤ b′ . Otherwise, Adam wins.

The following is proved in [Colcombet and G¨oller, 2016].

Theorem 4. There exists an algorithm for deciding whether Eve wins in a domination game running in time O(nd ) where n is the number of vertices and d = dA + dB the total number of priorities. If Eve wins, then she has a finite memory winning strategy.

8 The Complete Solution

We recall that the assume-guarantee synthesis problem takes as input two PROMPT-LTL formulas ϕ over I and ψ over I ×O, and the goal is to decide whether for all b ∈ B, there exists b′ ∈ N and a system S : I + → O such that for all w ∈ I ω , JϕK(w) ≤ b =⇒ JψK(S(w)) ≤ b′ .

Let (ϕ, ψ) a PROMPT-LTL assume-guarantee specification. The three steps of the procedure are:

• Build two B¨uchi prompt automata Aint, Bint recognising JϕK and JψK (Theorem 2).
• Build two history-deterministic automata: a prompt automaton A equivalent to Aint and a prompt automaton B equivalent to Bint (Theorem 3).
• Build a domination game GA,B and solve it (Theorem 4).

We let A = (QA, qinit,A,∆A) and B = (QB, qinit,B,∆B) be the two history-deterministic automata above, and dA and dB the number of priorities used by A and B respectively.

In the domination game GA,B, Adam chooses the inputs and transitions in A, while Eve chooses the outputs and transitions in B. A round starts in (p, q) where p is a state of A and q a state of B. First Adam chooses an input i ∈ I and a transition (p, i, ℓA, p′ ) ∈ ∆A, and then Eve chooses an output o ∈ O and a transition (q, (i, o), ℓB, q′ ) ∈ ∆B. The round reaches (p′ , q′ ), and its label is (ℓA, ℓB).

Formally the domination game GA,B has vertices VAdam = QA × QB, and VEve = QA × QB × I, and set of edges consists of moves of Adam of the form ((p, q), (ℓA, ε), (p′ , q, i)) with (p, i, ℓA, p′ ) ∈ ∆A, and moves of Eve of the form ((p, q, i), (ε, ℓB), (p, q′ )) with (q, (i, o), ℓB, q′ ) ∈ ∆B.

A play π in GA,B induces a sequence of inputs πI ∈ I ω and a sequence of inputs and outputs πI×O ∈ (I ×O)ω .

Theorem 5. Eve wins in GA,B if and only if there exists a solution to the assume-guarantee synthesis problem.

As a tool for proving Theorem 5 we construct another game. In this game G Adam and Eve alternate, with Adam choosing inputs and Eve choosing outputs. The set of plays is (I ×O)ω , and we write πI×O for a play and πI ∈ I ω for the induced sequence of inputs. We write S for strategies of Eve in G because they indeed induce systems S : I + → O. Eve wins in G if for all b ∈ N, there exists b′ ∈ N and a strategy S such that all plays consistent with S satisfy JϕK(πI) ≤ b =⇒ JψK(πI×O) ≤ b′ . Otherwise Adam wins.

Fact 3. Eve wins in G if and only if there exists a solution to the assume-guarantee synthesis problem.

The benefit of this game reformulation is to take advantage of determinacy: since the condition is Borel, the game G is determined: either Eve has a winning strategy or Adam has one. This fact, together with the following lemma, proves that the two games G and GA,B are equivalent which, together with Fact 3, establishes Theorem 5.

Lemma 2.

• If Eve wins in G then she wins in GA,B;
• If Adam wins in G then he wins in GA,B.

Theorem 5 together with Theorem 4 establish the decidability of the assume-guarantee synthesis problem for PROMPT-LTL announced in Theorem 1. Let us have a more precise complexity analysis. We start with two PROMPT-LTL formula ϕ and ψ of size n, construct two B¨uchi prompt automata Aint and Bint of size s = 2O(n) , turn them into historydeterministic prompt automata A and B of size 22O(n) with 2O(n) priorities. This induces a domination game with 22O(n) vertices and 2O(n) priorities. The algorithm for solving this domination game runs in time 22O(n2 ) . Thus the whole procedure runs in doubly-exponential time. The lower bound is inherited from LTL synthesis.

We leave as an open question whether the uniform assumeguarantee synthesis problem is decidable, where there exists a system independent of b. These two problems (uniform and non-uniform) are not equivalent, which is related to the fact that prompt automata can be made history-deterministic in a non-uniformway, but not in a uniformway.