Distributed Synthesis for Parameterized Temporal Logics

TL;DR

This paper investigates the synthesis of distributed systems from parameterized temporal logic specifications, showing that certain problems remain decidable or semi-decidable in various system models and extending results to stronger logics.

Contribution

It demonstrates that distributed synthesis for PROMPT-LTL is not harder than LTL in synchronous systems and provides a semi-decision procedure for asynchronous systems, extending to PLTL and PLDL.

Findings

Realizability for PROMPT-LTL in synchronous systems is as tractable as LTL.

Semi-decision procedure for asynchronous PROMPT-LTL synthesis based on bounded synthesis.

Results extend to stronger logics PLTL and PLDL.

Abstract

We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous distributed systems we show that, despite being more powerful, the realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to express scheduling assumptions and therefore consider an assume-guarantee synthesis problem. As asynchronous distributed synthesis is already undecidable for LTL, we give a semi-decision procedure for the PROMPT-LTL assume-guarantee synthesis problem based on bounded synthesis. Finally, we show that our results extend to the stronger logics PLTL and PLDL.

Equations

$$\phi ::=a\mid \neg a\mid \phi \wedge \phi \mid \phi \vee \phi \mid X\phi \mid \phi \mathbf{U}\phi \mid \phi \mathbf{R}\phi \mid {\mathbf{F}}_{\mathbf{P}}\phi ,$$

$$(r\to (r\mathbf{U}(\neg r\mathbf{U}{rel}_r(\psi ))))\wedge (\neg r\to (\neg r\mathbf{U}(r\mathbf{U}{rel}_r(\psi )))),$$

$$⟨P\cup \{p_r\},p_{env},\{I_p{\}}_{p\in P}\cup \{I_r\},\{O_p{\}}_{p\in P}\cup \{O_r\}⟩,$$

$$\{s_0\}\cup \left\{s_{v,x}\mid v\in V,x\in 2^{\{r,r^{\prime }\}}\right\}\cup \left\{s_{v,y}^{\prime }\mid v\in V,y\in 2^{\{r,r^{\prime }\}}\right\}\cup \left\{s_z^{\prime \prime }\mid z\in 2^{\{r^{\prime }\}}\right\}$$

$$((v,s),(v^{\prime },s^{\prime }))\in E^{\prime }\iff (v,v^{\prime })\in E\wedge s^{\prime }\in \delta (s,(v,L(v)))$$

$$\left\{(q^{\prime },\upsilon )\in Q\times 2^I\mid \left((q,s),(q^{\prime },\Delta (s,\upsilon ))\right)\in E\right\}\supseteq \delta (q,(l(s),s)).$$

$$\begin{array}[]{ll}&s_{0}\in S\\[5.0pt] &\lambda^{\mathbb{B}}(q_{0},s_{0})\\[5.0pt] \forall q,q^{\prime}\in Q,s\in S,\upsilon\in 2^{I}:&\lambda^{\mathbb{B}}(q,s)\land(q^{\prime},\upsilon)\in\delta(q,(l(s),s))\\ &\rightarrow\lambda^{\mathbb{B}}(q^{\prime},\Delta(s,\upsilon))\land\lambda^{\#}(q^{\prime},\Delta(s,\upsilon))\geq\lambda^{\#}(q,s)\\[5.0pt] \forall q,q^{\prime}\in Q,s\in S,\upsilon\in 2^{I}:&\lambda^{\mathbb{B}}(q,s)\land(q^{\prime},\upsilon)\in\delta(q,(l(s),s))\land q^{\prime}\in\reflectbox{$B$}\\ &\rightarrow\lambda^{\#}(q^{\prime},\Delta(s,\upsilon))>\lambda^{\#}(q,s)\\[5.0pt] \end{array}$$

$$⟨2^{I\cup O\cup \{r,r^{\prime }\}}\times X,Q\times S,(q_0,s_0),{\delta }^{\ast },B^{\ast }⟩,$$

$${\delta }^{\ast }((q,s),(\sigma ,x))=\left\{(q^{\prime },s^{\prime })\mid q^{\prime }\in \delta (q,\sigma )\wedge s^{\prime }\in {\delta }^{\prime }(s,\{q,x\}\cup (\sigma \cap \{r,r^{\prime }\}))\right\},$$

$$\phi ::=a\mid \neg a\mid \phi \wedge \phi \mid \phi \vee \phi \mid X\phi \mid \phi \mathbf{U}\phi \mid \phi \mathbf{R}\phi \mid {\mathbf{F}}_{\le z}\phi \mid {\mathbf{G}}_{\le z}\phi ,$$

$${\mathrm{var}}_{\mathbf{F}}(\phi )=\{z\in \mathcal{V}\mid F_{\le z}\psi \in \mathrm{cl}(\phi )\}$$

$${\mathrm{var}}_{\mathbf{G}}(\phi )=\{z\in \mathcal{V}\mid G_{\le z}\psi \in \mathrm{cl}(\phi )\}$$

$$\phi$$

$$g$$

Full text

††journal: Information and Computation

1 Introduction

Linear Temporal Logic [1] ($\mathrm{LTL}$) is the most prominent specification language for reactive systems and the basis for industrial languages like ForSpec [2] and PSL [3]. Its advantages include a compact variable-free syntax and intuitive semantics as well as the exponential compilation property, which explains its attractive algorithmic properties: every $\mathrm{LTL}$ formula can be translated into an equivalent Büchi automaton of exponential size [4]. This yields a polynomial space model checking algorithm and a doubly-exponential time algorithm for solving two-player games. Such games solve the monolithic $\mathrm{LTL}$ synthesis problem: given a specification, construct a correct-by-design implementation.

However, $\mathrm{LTL}$ lacks the ability to express timing constraints. For example, the request-response property $\operatorname{\mathbf{G}}(\mathit{req}\rightarrow\operatorname{\mathbf{F}}\mathit{resp})$ requires that every request $\mathit{req}$ is eventually responded to by a $\mathit{resp}$. It is satisfied even if the waiting times between requests and responses diverge, i.e., it is impossible to require that requests are granted within a fixed, but arbitrary, amount of time. While it is possible to encode an a-priori fixed bound for an eventually into $\mathrm{LTL}$, this requires prior knowledge of the system’s granularity and incurs a blow-up when translated to automata, and is thus considered impractical.

To overcome this shortcoming of $\mathrm{LTL}$, Alur et al. introduced parametric $\mathrm{LTL}$ ($\mathrm{PLTL}$) [5], which extends $\mathrm{LTL}$ with parameterized operators of the form $\operatorname{\mathbf{F}}_{\leq x}$ and $\operatorname{\mathbf{G}}_{\leq y}$, where $x$ and $y$ are variables. The formula $\operatorname{\mathbf{G}}(req\rightarrow\operatorname{\mathbf{F}}_{\leq x}\,resp)$ expresses that every request is answered within an arbitrary, but fixed, number of steps $\alpha(x)$. Here, $\alpha$ is a variable valuation, a mapping of variables to natural numbers. Typically, one is interested in whether a $\mathrm{PLTL}$ formula is satisfied with respect to some variable valuation, e.g., model checking a transition system $\mathcal{S}$ against a $\mathrm{PLTL}$ specification $\varphi$ amounts to determining whether there is an $\alpha$ such that every trace of $\mathcal{S}$ satisfies $\varphi$ with respect to $\alpha$. Alur et al. [5] showed that the $\mathrm{PLTL}$ model checking problem is PSpace-complete. Due to monotonicity of the parameterized operators, one can assume that all variables $y$ in parameterized always operators $\operatorname{\mathbf{G}}_{\leq y}$ are mapped to zero, as variable valuations are quantified existentially in the problem statements. Dually, again due to monotonicity, one can assume that all variables $x$ in parameterized eventually operators $\operatorname{\mathbf{F}}_{\leq x}$ are mapped to the same value, namely the maximum of the bounds. Thus, in many cases the parameterized always operators and different variables for parameterized eventually operators are not necessary.

Motivated by this, Kupferman et al. introduced $\mathrm{PROMPT}$–$\mathrm{LTL}$ [6], which can be seen as the fragment of $\mathrm{PLTL}$ without the parameterized always operator and with a single bound $k$ for the parameterized eventually operators. They proved that $\mathrm{PROMPT}$–$\mathrm{LTL}$ model checking is PSpace-complete and solving $\mathrm{PROMPT}$–$\mathrm{LTL}$ games is 2ExpTime-complete, i.e., not harder than $\mathrm{LTL}$ games. While the results of Alur et al. rely on involved pumping arguments, the results of Kupferman et al. are all based on the so-called alternating color technique, which basically allows to reduce $\mathrm{PROMPT}$–$\mathrm{LTL}$ to $\mathrm{LTL}$.

Intuitively, one introduces a new proposition that is thought of as coloring traces of a system. Then, one replaces each parameterized eventually operator $\operatorname{\mathbf{F}}_{\leq x}\varphi$ by an $\mathrm{LTL}$ formula requiring $\varphi$ to hold within at most one color change. If the distance between color changes is bounded from above, then satisfaction of the rewritten formula implies the existence of a bound $k$ for the bounded eventually operators such that the original formula is satisfied with respect to $k$. Dually, if the distance between color changes is bounded from below, then the other implication holds: the original $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula implies the rewritten $\mathrm{LTL}$ formula.

When applying this equivalence, one has to specify how the truth values for the new atomic proposition coloring the traces are determined. In a game setting (in particular in synthesis), the player who aims to satisfy the $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula determines these truth values and is required to change colors infinitely often. Then, a finite-state strategy automatically ensures an upper bound on the distance between color changes.

Later, the result on $\mathrm{PROMPT}$–$\mathrm{LTL}$ games was extended to $\mathrm{PLTL}$ games [7], relying on the monotonicity properties explained above and an application of the alternating color technique. These results show that adding parameters to $\mathrm{LTL}$ does not increase the asymptotic complexity of the model checking and the game-solving problem, which is still true for even more expressive logics like Parametric Linear Dynamic Logic ($\mathrm{PLDL}$) [8] and $\mathrm{PLTL}$ and $\mathrm{PLDL}$ with costs [9]. The former logic is an extension of $\mathrm{PLTL}$ with the full expressiveness of the $\omega$-regular languages. The latter logics are evaluated in weighted systems and generalize $\mathrm{PLTL}$ and $\mathrm{PLDL}$ by bounding the parameterized operators in the accumulated weight instead of bounding them in time.

The synthesis problems mentioned above assume a setting of complete information, i.e., every part of the system has a complete view on the system as a whole. However, this setting is unrealistic in distributed systems. Based on this observation, distributed synthesis is defined as the problem of synthesizing multiple components with incomplete information. Since there are specifications that are not implementable, one differentiates synthesis from the corresponding decision problem, i.e., the realizability problem of a formal specification. We focus on the latter, but note that typically algorithms for the realizability problem also solve the synthesis problem, as they rely on constructing implementations to prove realizability. This also holds in our work here.

The realizability problem for distributed systems dates back to work of Pnueli and Rosner in the early nineties [10]. They showed that the realizability problem for LTL becomes undecidable already for the simple architecture of two processes with pairwise different inputs. In subsequent work, it was shown that certain classes of architectures, like pipelines and rings, can still be synthesized automatically [11, 12]. Later, a complete characterization of the architectures for which the realizability problem is decidable was given by Finkbeiner and Schewe by the information fork criterion [13]. Intuitively, an architecture contains an information fork if there is an information flow from the environment to two different processes where the information to one process is hidden from the other and vice versa. The distributed realizability problem is decidable exactly for those architectures without an information fork. Beyond decidability results, semi-decision procedures like bounded synthesis [14] give an architecture-independent synthesis method that is particularly well-suited for finding small-sized implementations. Bounded synthesis searches for finite-state implementations of a fixed size by encoding the problem as a constraint system in a decidable first-order theory. In case of a positive answer, the result is returned, otherwise the bound is increased. If there is an upper bound on the size of a finite-state implementation, then bounded synthesis is a complete decision procedure, as it can be stopped if the upper bound is reached without a positive answer. If there is no such upper bound, it is indeed a semi-decision procedure that finds an implementation if one exists, but runs forever otherwise.

1.1 Our Contributions

As mentioned above, one can add parameters to $\mathrm{LTL}$ for free: the complexity of the model checking problem and of solving infinite games does not increase. This raises the question whether this is also true for distributed realizability of parametric temporal logics. For synchronous systems, we can answer this question affirmatively. For every class of architectures with decidable $\mathrm{LTL}$ realizability, the $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem is decidable, too. To show this, we apply the alternating color technique [6] to reduce the distributed realizability problem of $\mathrm{PROMPT}$–$\mathrm{LTL}$ to the one of $\mathrm{LTL}$: one can again add parameterized operators to $\mathrm{LTL}$ for free. To prove this result, we add a new process whose only task it is to determine a coloring with the fresh proposition. By ensuring that the new process does not introduce an information fork we obtain decidability for the same class of architectures as for $\mathrm{LTL}$.

For asynchronous systems, the environment is typically assumed to take over the responsibility for the scheduling decision [15]. Consequently, the resulting schedules may be unrealistic, e.g., one process may not be scheduled at all. While fairness assumptions such as “every process is scheduled infinitely often” solve this problem for $\mathrm{LTL}$ specifications, they are insufficient for $\mathrm{PROMPT}$–$\mathrm{LTL}$: a fair scheduler can still delay process activations arbitrarily long and thereby prevent the system from satisfying its $\mathrm{PROMPT}$–$\mathrm{LTL}$ specification for any bound $k$. Bounded fair scheduling, where every process is guaranteed to be scheduled in bounded intervals, overcomes this problem. Since bounded fairness can be expressed in $\mathrm{PROMPT}$–$\mathrm{LTL}$, the realizability problem in asynchronous architectures can be formulated more generally as an assume-guarantee realizability problem that consists of two $\mathrm{PROMPT}$–$\mathrm{LTL}$ specifications. Hence, we have to deal with two colorings of the traces when applying the alternating color technique: One induces bounds on the parameterized eventually operators in the assumption, the other on the bounds on the parameterized eventually operators in the guarantee.

We give a semi-decision procedure for this problem based on a new method for checking emptiness of two-colored Büchi graphs [6] and an extension of bounded synthesis [14]. As asynchronous $\mathrm{LTL}$ realizability for architectures with more than one process is undecidable [15], the same result holds for $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability. Thus, the semi-decision procedure is the best result one can hope for. Decidability in the one process case, which holds for $\mathrm{LTL}$ [15], is left open for $\mathrm{PROMPT}$–$\mathrm{LTL}$.

Finally, we show that all these results also hold for $\mathrm{PLTL}$ and $\mathrm{PLDL}$, even stronger logics to which the alternating color technique and bounded synthesis are still applicable.

This is a revised and extended version of a paper that appeared at GandALF 2016 [16].

1.2 Related Work

There is a rich literature regarding the synthesis of distributed systems from global $\omega$-regular specifications [10, 11, 12, 13, 17, 18, 19, 20]. We are not aware of work that is concerned with the realizability of parameterized logics in this setting. For local specifications, i.e., specifications that only relate the inputs and outputs of single processes, the realizability problem becomes decidable for a larger class of architectures [21]. An extension of these results to context-free languages was given by Fridman and Puchala [22]. The realizability problem for asynchronous systems and LTL specifications is undecidable for architectures with more than one process to be synthesized [15]. Later, Gastin et al. showed decidability of a restricted specification language and certain types of architectures, i.e., well-connected [23] and acyclic [24] ones. Bounded synthesis [14, 25] provides a flexible synthesis framework that can be used in both the asynchronous and the synchronous setting, based on a semi-decision procedure.

1.3 Structure

In Section 2, we introduce $\mathrm{PROMPT}$–$\mathrm{LTL}$ and the alternating color technique. In Section 3, we consider synchronous distributed synthesis for $\mathrm{PROMPT}$–$\mathrm{LTL}$ and the asynchronous case in Section 4. Then, in Section 5, we consider both problems for the more expressive logics $\mathrm{PLTL}$ and $\mathrm{PLDL}$. We conclude in Section 6 with a discussion of future work.

2 $\mathrm{PROMPT}$–$\mathrm{LTL}$

Throughout this work, we fix a set $\mathrm{AP}$ of atomic propositions. The formulas of $\mathrm{PROMPT}$–$\mathrm{LTL}$ are given by the grammar

[TABLE]

where $a\in\mathrm{AP}$ is an atomic proposition, $\neg,\wedge,\vee$ are the usual Boolean operators, and $\operatorname{\mathbf{X}},\mathbin{\mathbf{U}},\mathbin{\mathbf{R}}$ are the $\mathrm{LTL}$ operators next, until, and release. We use the derived operators $\mathbf{tt}\coloneqq a\vee\neg a$ and $\mathbf{ff}\coloneqq a\wedge\neg a$ for some fixed $a\in\mathrm{AP}$, and $\operatorname{\mathbf{F}}\varphi\coloneqq\mathbf{tt}\mathbin{\mathbf{U}}\varphi$ and $\operatorname{\mathbf{G}}\varphi\coloneqq\mathbf{ff}\mathbin{\mathbf{R}}\varphi$ as usual. Furthermore, we use $\varphi\mathbin{\rightarrow}\psi$ as a shorthand for $\neg\varphi\vee\psi$ if the antecedent $\varphi$ is an $\operatorname{\mathbf{F_{P}}}$-free formula (since in that case we can transform $\neg\varphi$ into negation normal form in the fragment above). We define the size of $\varphi$ to be the number of sub-fomulas of $\varphi$. The satisfaction relation for $\mathrm{PROMPT}$–$\mathrm{LTL}$ is defined between an $\omega$-word $w=w_{0}w_{1}w_{2}\cdots\in\left(2^{\mathrm{AP}}\right)^{\omega}$, a position $n\in\mathbb{N}$, a bound $k$ for the prompt-eventually operators, and a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula.

$(w,n,k)\vDash a$ if, and only if, $a\in w_{n}$.

• 2.

$(w,n,k)\vDash\neg a$ if, and only if, $a\notin w_{n}$.

• 3.

$(w,n,k)\vDash\varphi_{0}\wedge\varphi_{1}$ if, and only if, $(w,n,k)\vDash\varphi_{0}$ and $(w,n,k)\vDash\varphi_{1}$.

• 4.

$(w,n,k)\vDash\varphi_{0}\vee\varphi_{1}$ if, and only if, $(w,n,k)\vDash\varphi_{0}$ or $(w,n,k)\vDash\varphi_{1}$.

• 5.

$(w,n,k)\vDash\operatorname{\mathbf{X}}\varphi$ if, and only if, $(w,n+1,k)\vDash\varphi$.

• 6.

$(w,n,k)\vDash\varphi_{0}\mathbin{\mathbf{U}}\varphi_{1}$ if, and only if, there exists a $j\geq 0$ such that $(w,n+j,k)\vDash\varphi_{1}$ and $(w,n+j^{\prime},k)\vDash\varphi_{0}$ for every $j^{\prime}$ in the range $0\leq j^{\prime}<j$.

• 7.

$(w,n,k)\vDash\varphi_{0}\mathbin{\mathbf{R}}\varphi_{1}$ if, and only if, for all $j\geq 0$: $(w,n+j,k)\vDash\varphi_{1}$ or $(w,n+j^{\prime},k)\vDash\varphi_{0}$ for some $j^{\prime}$ in the range $0\leq j^{\prime}<j$.

• 8.

$(w,n,k)\vDash\operatorname{\mathbf{F_{P}}}\varphi$ if, and only if, there exists a $j$ in the range $0\leq j\leq k$ such that $(w,n+j,k)\vDash\varphi$.

For the sake of brevity, we write $(w,k)\vDash\varphi$ instead of $(w,0,k)\vDash\varphi$ and say that $w$ is a model of $\varphi$ with respect to $k$. Note that $(w,n,k)\vDash\varphi$ implies $(w,n,k^{\prime})\vDash\varphi$ for every $k^{\prime}\geq k$, i.e., satisfaction with respect to $k$ is an upward-closed property.

The Alternating Color Technique

In this subsection, we recall the alternating color technique, which Kupferman et al. introduced to solve model checking, assume-guarantee model checking, and the realizability problem for $\mathrm{PROMPT}$–$\mathrm{LTL}$ specifications [6].

Let $r\notin\mathrm{AP}$ be a fixed fresh proposition. An $\omega$-word $w^{\prime}\in\left(2^{\mathrm{AP}\cup\{r\}}\right)^{\omega}$ is an $r$-coloring of $w\in\left(2^{\mathrm{AP}}\right)^{\omega}$ if $w_{n}^{\prime}\cap\mathrm{AP}=w_{n}$, i.e., $w_{n}$ and $w_{n}^{\prime}$ coincide on all propositions in $\mathrm{AP}$. The additional proposition $r$ can be thought of as the color of $w_{n}^{\prime}$: we say that the color changes at position $n$, if $n=0$ or if the truth values of $r$ in $w_{n-1}^{\prime}$ and in $w_{n}^{\prime}$ are not equal. In this situation, we say that $n$ is a change point. An $r$-block is a maximal infix $w_{m}^{\prime}\cdots w_{n}^{\prime}$ of $w^{\prime}$ such that the color changes at $m$ and $n+1$, but not in between.

Let $k\geq 1$. We say that $w^{\prime}$ is $k$-spaced if the color changes infinitely often and each $r$-block has length at least $k$, and we say that $w^{\prime}$ is $k$-bounded, if each $r$-block has length at most $k$. Note that $k$-boundedness implies that the color changes infinitely often.

Given a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula $\varphi$, let $\mathit{rel}_{r}(\varphi)$ denote the formula obtained by inductively replacing every sub-formula $\operatorname{\mathbf{F_{P}}}\psi$ by

[TABLE]

which is only linearly larger than $\varphi$ and requires every prompt eventually to be satisfied within at most one color change (not counting the position where $\psi$ holds). Furthermore, the formula $\mathit{alt}_{r}=\operatorname{\mathbf{GF}}r\wedge\operatorname{\mathbf{GF}}\neg r$ is satisfied if the colors change infinitely often. Finally, we define the $\mathrm{LTL}$ formula $c_{r}(\varphi)=\mathit{rel}_{r}(\varphi)\wedge\mathit{alt}_{r}$. Kupferman et al. showed that $\varphi$ and $c_{r}(\varphi)$ are in some sense equivalent on $\omega$-words which are bounded and spaced.

Lemma 1** (Lemma 2.1 of [6]).**

Let $\varphi$ be a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula, and let $w\in\left(2^{\mathrm{AP}}\right)^{\omega}$.

If $(w,k)\vDash\varphi$, then $w^{\prime}\vDash c_{r}(\varphi)$ for every $k$-spaced $r$-coloring $w^{\prime}$ of $w$. 2. 2.

If $w^{\prime}$ is a $k$-bounded $r$-coloring of $w$ with $w^{\prime}\vDash c_{r}(\varphi)$, then $(w,2k)\vDash\varphi$.

Whenever possible, we drop the subscript $r$ for the sake of readability, if $r$ is clear from context. However, when we consider asynchronous systems in Section 4, we need to relativize two formulas with different colors, which necessitates the introduction of the subscripts.

3 Synchronous Distributed Synthesis

$\mathrm{PROMPT}$–$\mathrm{LTL}$ specifications can give guarantees that $\mathrm{LTL}$ cannot, for example by asserting not only that requests to a system are answered eventually, but also that there is an upper bound on the reaction time. This is especially important in distributed systems, since such timing constraints become more difficult to implement because of information flows between the various parts of the system.

Consider, for example, a distributed computation system, where a central server gets important and unimportant tasks, and can forward tasks to a number of clients. A client can either enqueue the task, which means that it will be processed eventually, or clear the client-side queue and process the task immediately. The latter operation is very costly (we have to remember the open tasks as they still need to be completed), but guarantees an upper bound on the completion time. While in $\mathrm{LTL}$ we can only specify that all incoming tasks are processed eventually, in $\mathrm{PROMPT}$–$\mathrm{LTL}$ we can specify that the answer time to important tasks is bounded by the formula $\operatorname{\mathbf{G}}(\mathit{important\text{-}task}\rightarrow\operatorname{\mathbf{F_{P}}}\mathit{finished\text{-}task})$.222A similar constraint could be simulated in $\mathrm{LTL}$ by writing that on every important incoming task, the worker queues are cleared. This, however, removes implementation freedom and requires the developer to determine how to implement the feature, instead of letting the synthesis algorithm decide.

Let us now formalize the distributed realizability problem. Let $X$ and $Y$ be finite and pairwise disjoint sets of variables. A valuation of $X$ is a subset of $X$; thus, the set of all valuations of $X$ is $2^{X}$. For $w=w_{0}w_{1}w_{2}\cdots\in(2^{X})^{\omega}$ and $w^{\prime}=w^{\prime}_{0}w^{\prime}_{1}w^{\prime}_{2}\cdots\in(2^{Y})^{\omega}$, let $w\cup w^{\prime}=(w_{0}\cup w^{\prime}_{0})(w_{1}\cup w^{\prime}_{1})(w_{2}\cup w^{\prime}_{2})\cdots\in(2^{X\cup Y})^{\omega}$.

Strategies

A strategy $f\colon(2^{X})^{*}\rightarrow 2^{Y}$ maps a history of valuations of $X$ to a valuation of $Y$. The behavior of a strategy $f\colon(2^{X})^{*}\rightarrow 2^{Y}$ is characterized by an infinite tree that branches by the valuations of $X$ and whose nodes $w\in(2^{X})^{*}$ are labeled with the strategic choice $f(w)$. For an infinite word $w=w_{0}w_{1}w_{2}\cdots\in(2^{X})^{\omega}$, the corresponding labeled path is defined as $(f(\varepsilon)\cup w_{0})(f(w_{0})\cup w_{1})(f(w_{0}w_{1})\cup w_{2})\cdots\in(2^{X\cup Y})^{\omega}$. We lift the set containment operator $\in$ to the containment of a labeled path $w=w_{0}w_{1}w_{2}\cdots\in(2^{X\cup Y})^{\omega}$ in a strategy tree induced by $f\colon(2^{X})^{*}\rightarrow 2^{Y}$, i.e., $w\in f$ if, and only if, $f(\varepsilon)=w_{0}\cap Y$ and $f((w_{0}\cap X)\cdots(w_{i}\cap X))=w_{i+1}\cap Y$ for all $i\geq 0$.

A $2^{Y}$-labeled $2^{X}$-transition system $\mathcal{S}$ is a tuple ${\langle S,s_{0},\Delta,l\rangle}$ where $S$ is a finite set of states, $s_{0}\in S$ is the designated initial state, $\Delta\colon S\times 2^{X}\rightarrow S$ is the transition function, and $l\colon S\rightarrow 2^{Y}$ is the state-labeling. We generalize the transition function to sequences over $2^{X}$ by defining $\Delta^{*}\colon(2^{X})^{*}\rightarrow S$ recursively as $\Delta^{*}(\varepsilon)=s_{0}$ and $\Delta^{*}(w_{0}\cdots w_{n-1}w_{n})=\Delta(\Delta^{*}(w_{0}\cdots w_{n-1}),w_{n})$ for $w_{0}\cdots w_{n-1}w_{n}\in(2^{X})^{+}$. A transition system $\mathcal{S}$ generates the strategy $f$ if $f(w)=l(\Delta^{*}(w))$ for every $w\in(2^{X})^{*}$. A strategy $f$ is called finite-state if there exists a transition system that generates $f$.

To reason about distributed systems, we have to combine strategies with different inputs, which we call the distributed product. To this end, we have to introduce widenings of strategies, which intuitively enlarge their domains with new atomic propositions that are ignored. Also, we need projections, which remove outputs from strategies.

In the following, we formally introduce these concepts. A visualization is given in Fig. 1.

Definition 1** (Distributed Product).**

Let $X,X^{\prime},Y$, and $Y^{\prime}$ be finite sets such that $Y$ and $Y^{\prime}$ are disjoint. Further, let $f\colon(2^{X})^{*}\rightarrow 2^{Y}$ and $f^{\prime}\colon(2^{X})^{*}\rightarrow 2^{Y^{\prime}}$ be two strategies with the same domain but different co-domains $2^{Y}$ and $2^{Y^{\prime}}$.

The product $f\times f^{\prime}\colon(2^{X})^{*}\rightarrow 2^{Y\cup Y^{\prime}}$ of $f$ and $f^{\prime}$ is defined as $(f\times f^{\prime})(w)=f(w)\cup f^{\prime}(w)$ for every $w\in(2^{X})^{*}$.

• 2.

The $2^{X}$-projection of a sequence $w_{0}\cdots w_{n}\in(2^{X\cup X^{\prime}})^{*}$ is $\mathrm{proj}_{2^{X}}(w_{0}\cdots w_{n})=(w_{0}\cap X)\cdots(w_{n}\cap X)\in(2^{X})^{*}$.

• 3.

The $2^{X^{\prime}}$-widening of $f$ is defined as $\mathrm{wide}_{2^{X^{\prime}}}(f)\colon(2^{X\cup X^{\prime}})^{*}\rightarrow 2^{Y}$ with $\mathrm{wide}_{2^{X^{\prime}}}(f)(w)=f(\mathrm{proj}_{2^{X}}(w))$ for $w\in(2^{X\cup X^{\prime}})^{*}$.

• 4.

Given some $g\colon(2^{X^{\prime}})^{*}\rightarrow 2^{Y^{\prime}}$, the distributed product $f\otimes g\colon(2^{X\cup X^{\prime}})^{*}\rightarrow 2^{Y\cup Y^{\prime}}$ is defined as the product $\mathrm{wide}_{2^{X^{\prime}\setminus X}}(f)\times\mathrm{wide}_{2^{X\setminus X^{\prime}}}(g)$.

Analogously, for transition systems $\mathcal{S}={\langle S,s_{0},\Delta,l\rangle}$ and $\mathcal{S}^{\prime}={\langle S^{\prime},s_{0}^{\prime},\Delta^{\prime},l^{\prime}\rangle}$ the distributed product, written $\mathcal{S}\otimes\mathcal{S}^{\prime}$, is defined as the transition system ${\langle S\times S^{\prime},(s_{0},s_{0}^{\prime}),\Delta^{\otimes},l^{\otimes}\rangle}$, where $\Delta^{\otimes}((s,s^{\prime}),w)=(s^{\prime\prime},s^{\prime\prime\prime})$ if, and only if, $\Delta(s,w)=s^{\prime\prime}$ and $\Delta^{\prime}(s^{\prime},w)=s^{\prime\prime\prime}$, and $l^{\otimes}(s,s^{\prime})=l(s)\cup l^{\prime}(s^{\prime})$.

Remark 1**.**

The strategy generated by $\mathcal{S}\otimes\mathcal{S}^{\prime}$ is equal to the distributed product of the strategies generated by $\mathcal{S}$ and $\mathcal{S}^{\prime}$.

We define the satisfaction of a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula $\varphi$ (over propositions $X\cup Y$) on strategy $f$ with respect to the bound $k$, written $(f,k)\vDash\varphi$ for short, as $(w,k)\vDash\varphi$ for all paths $w\in f$.

Distributed Systems

We characterize a distributed system as a set of processes with a fixed communication topology, called an architecture in the following. Recall that $\mathrm{AP}$ is the set of atomic propositions used to build formulas. An architecture $\mathcal{A}$ is a tuple ${\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$, where $P$ is the finite set of processes and $p_{\mathit{env}}\in P$ is the distinct environment process. We denote by $P^{-}=P\setminus{\{{p_{\mathit{env}}}\}}$ the set of system processes.

Given a process $p\in P$, the input and output signals of this process are $I_{p}\subseteq\mathrm{AP}$ and $O_{p}\subseteq\mathrm{AP}$, respectively, where we assume $I_{{p_{\mathit{env}}}}=\emptyset$. For $P^{\prime}\subseteq P$, let $I_{P^{\prime}}=\bigcup_{p\in P^{\prime}}I_{p}$ and $O_{P^{\prime}}=\bigcup_{p\in P^{\prime}}O_{p}$. While processes may share the same inputs (in case of broadcasting), the outputs of processes must be pairwise disjoint, i.e., for all $p\neq p^{\prime}\in P$ it holds that $O_{p}\cap O_{p^{\prime}}=\emptyset$. Finally, we require that every input of a process originates from some other process, i.e., $I_{P}\subseteq O_{P}$.

An implementation of a process $p\in P^{-}$ is a strategy $f_{p}\colon(2^{I_{p}})^{*}\rightarrow 2^{O_{p}}$ mapping finite input sequences to a valuation of the output variables.

Example 1**.**

Figure 2 shows example architectures $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$:

$\mathcal{A}_{1}=\langle{\{{p_{\mathit{env}}},p_{1},p_{2}\}},{p_{\mathit{env}}},{\{I_{p_{\mathit{env}}},I_{p_{1}},I_{p_{2}}\}},{\{O_{p_{\mathit{env}}},O_{p_{1}},O_{p_{2}}\}}\rangle$* with*

• (a)

$I_{p_{\mathit{env}}}=\emptyset,I_{p_{1}}={\{a\}},I_{p_{2}}={\{b\}}$* and*

• (b)

$O_{p_{\mathit{env}}}={\{a,b\}},O_{p_{1}}={\{c\}},O_{p_{2}}={\{d\}}$.

• 2.

$\mathcal{A}_{2}=\langle{\{{p_{\mathit{env}}},p_{1},p_{2}\}},{p_{\mathit{env}}},{\{I_{p_{\mathit{env}}},I_{p_{1}},I_{p_{2}}\}},{\{O_{p_{\mathit{env}}},O_{p_{1}},O_{p_{2}}\}}\rangle$* with*

• (a)

$I_{p_{\mathit{env}}}=\emptyset,I_{p_{1}}={\{a\}},I_{p_{2}}={\{b\}}$* and*

• (b)

$O_{p_{\mathit{env}}}={\{a\}},O_{p_{1}}={\{b\}},O_{p_{2}}={\{c\}}$.

The architecture $\mathcal{A}_{1}$ in Fig. 2(a) contains two system processes, $p_{1}$ and $p_{2}$, and the environment process ${p_{\mathit{env}}}$. The processes $p_{1}$ and $p_{2}$ receive the inputs $a$ and $b$, respectively, from the environment and output $c$ and $d$, respectively. Hence, the environment can provide process $p_{1}$ with information that is hidden from $p_{2}$ and vice versa. In contrast, architecture $\mathcal{A}_{2}$, depicted in Fig. 2(b), is a pipeline architecture where information from the environment can only propagate through the pipeline processes $p_{1}$ and $p_{2}$.

Distributed Realizability

Let $\mathcal{A}={\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$ be an architecture. The synchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem for $\mathcal{A}$ is to decide, given a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula $\varphi$, whether there exist a bound $k$ and a finite-state implementation $f_{p}$ for each process $p\in P^{-}$, such that the distributed product $\bigotimes_{p\in P^{-}}f_{p}$ satisfies $\varphi$ with respect to $k$, i.e., $(\bigotimes_{p\in P^{-}}f_{p},k)\vDash\varphi$. In this case, we say that $\varphi$ is realizable in $\mathcal{A}$. The synchronous $\mathrm{LTL}$ realizability problem is a special case of it, as $\mathrm{LTL}$ is a fragment of $\mathrm{PROMPT}$–$\mathrm{LTL}$.

In the following, we show how to solve the synchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem. In our reduction to synchronous $\mathrm{LTL}$ realizability, we introduce a new process that produces a coloring sequence needed for applying the alternating color technique [6]. Let $r\notin\mathrm{AP}$ be the fresh proposition introduced for the alternating color technique to relativize formulas and let $\mathcal{A}={\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$ be an architecture as above. We define the architecture $\mathcal{A}^{r}$ as

[TABLE]

where $I_{r}=\emptyset$ and $O_{r}={\{r\}}$. Intuitively, this describes an architecture where one additional process $p_{r}$ is responsible for providing sequences in $(2^{{\{r\}}})^{\omega}$, i.e., a coloring by $r$. We show that $\varphi$ in $\mathcal{A}$ and $c_{r}(\varphi)$ in $\mathcal{A}^{r}$ are equi-realizable by applying the alternating color technique. As the processes are synchronized, the proof is similar to the one for the single-process case by Kupferman et al. [6].

Theorem 1**.**

A $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula $\varphi$ is realizable in $\mathcal{A}$ if, and only if, $c_{r}(\varphi)$ is realizable in $\mathcal{A}^{r}$.

Proof.

Let $\mathcal{A}={\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$ be an architecture and $\varphi$ be a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula.

Assume that the $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula $\varphi$ is realizable in $\mathcal{A}$. Then, there exist finite-state strategies $f_{p}$ for $p\in P^{-}$ and a bound $k$ satisfying the synchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem ${\langle\mathcal{A},\varphi\rangle}$. For every $w\in\bigotimes_{p\in P^{-}}f_{p}$, it holds that $(w,k)\vDash\varphi$. By item 1 of Lemma 1, it holds that every $k$-spaced $r$-coloring $w^{\prime}$ of $w$ satisfies $c_{r}(\varphi)$. Let $f_{r}\colon(2^{\emptyset})^{*}\rightarrow 2^{\{r\}}$ be a (finite-state) strategy that produces the $k$-spaced sequence $(\emptyset^{k}{\{r\}}^{k})^{\omega}$. Then, the process implementations ${\{f_{p}\}}_{p\in P^{-}}$ together with $f_{r}$ are a solution to the synchronous $\mathrm{LTL}$ realizability problem ${\langle\mathcal{A}^{r},c_{r}(\varphi)\rangle}$.

Now, assume that the $\mathrm{LTL}$ formula $c_{r}(\varphi)$ is realizable in the architecture $\mathcal{A}^{r}$. Thus, there exist finite-state strategies $f_{p}$ for $p\in P^{-}$ and a finite-state strategy $f_{r}$ for process $p_{r}$. Note that the strategy $f_{r}\colon(2^{\emptyset})^{*}\rightarrow 2^{{\{r\}}}$ has a unique output $w_{r}\in(2^{{{\{r\}}}})^{\omega}$, as it has no inputs. We claim that $w_{r}$ is $k$-bounded, where $k$ is the number of states of the transition system $\mathcal{S}={\langle S,s_{0},\Delta,l\rangle}$ generating $f_{r}$. To see this, note that $f_{r}$ has no inputs, i.e., each state of $\mathcal{S}$ has a unique successor in $\Delta$, and the unique run of $\mathcal{S}$ on $\emptyset^{\omega}$ ends up in a loop which is traversed ad infinitum. As the output $w_{r}$ has infinitely many change points (since $c_{r}(\varphi)$ is realizable in $\mathcal{A}^{r}$), the loop contains at least one state $s$ labeled by $l(s)=\emptyset$ and at last one state $s^{\prime}$ with $l(s^{\prime})={\{r\}}$. Thus, the maximal length of a block of $w_{r}$ is bounded by the length of the loop, which in turn is bounded by the size of $\mathcal{S}$.

Hence, for every $w\in\bigotimes_{p\in P^{-}}f_{p}$, the word $w_{r}\cup w$ is a $k$-bounded $r$-coloring of $w$ with $w_{r}\cup w\vDash\mathit{rel}_{r}(\varphi)$. By item 2 of Lemma 1, for all such $w$ it holds that $(w,2k)\vDash\varphi$. Hence, ${\{f_{p}\}}_{p\in P^{-}}$ together with the bound $2k$ is a solution to the synchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem. ∎

Theorem 1 allows us to reduce the distributed realizability problem of $\mathrm{PROMPT}$–$\mathrm{LTL}$ to the distributed realizability problem of $\mathrm{LTL}$ in a strategy-preserving manner as shown in the accompanying proof. In particular, we are able to reuse semi-decision procedures for the latter, such as bounded synthesis [14], to effectively construct small solutions.

To conclude, we show that the newly introduced process $p_{r}$ also preserves the property whether the architecture has an information fork [13]. Formally, consider tuples ${\langle P^{\prime},V^{\prime},p,p^{\prime}\rangle}$, where $P^{\prime}$ is a subset of the processes, $V^{\prime}$ is a subset of the variables disjoint from $I_{p}\cup I_{p^{\prime}}$, and $p,p^{\prime}\in P^{-}\setminus P^{\prime}$ are two different processes. Such a tuple is an information fork in $\mathcal{A}$ if $P^{\prime}$ together with the edges that are labeled with at least one variable from $V^{\prime}$ forms a sub-graph of $\mathcal{A}$ rooted in the environment and there exist two nodes $q,q^{\prime}\in P^{\prime}$ that have edges to $p,p^{\prime}$, respectively, such that $O_{\{q,p\}}\nsubseteq I_{p^{\prime}}$ and $O_{\{q^{\prime},p^{\prime}\}}\nsubseteq I_{p}$. For example, the architecture in Fig. 2(a) contains the information fork $({\{{p_{\mathit{env}}}\}},\emptyset,p_{1},p_{2})$, while the pipeline architecture depicted in Fig. 2(b) has no information forks.

Lemma 2**.**

$\mathcal{A}^{r}$* contains an information fork if, and only if, $\mathcal{A}$ contains an information fork.*

Proof.

The if direction follows immediately by construction: if ${\langle P^{\prime},V^{\prime},p,p^{\prime}\rangle}$ is an information fork in $\mathcal{A}$, then it is an information fork in $\mathcal{A}^{r}$ as well. Hence, assume ${\langle P^{\prime},V^{\prime},p,p^{\prime}\rangle}$ is an information fork in $\mathcal{A}^{r}$. It holds that neither $p_{r}=p$ nor $p_{r}=p^{\prime}$ since $p_{r}$ has no incoming edges. As $I_{p_{r}}=\emptyset$, $p_{r}$ cannot be in a sub-graph that is rooted in the environment, hence, $p_{r}\notin P^{\prime}$ and $r\notin V^{\prime}$. It follows that ${\langle P^{\prime},V^{\prime},p,p^{\prime}\rangle}$ is an information fork in $\mathcal{A}$. ∎

Thus, we can use well-known results for the decidability of distributed realizability for $\mathrm{LTL}$ and weakly ordered architectures [13], i.e., those without an information fork.

Corollary 1**.**

Let $\mathcal{A}$ be an architecture. The synchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem for $\mathcal{A}$ is decidable if, and only if, $\mathcal{A}$ is weakly ordered.

4 Asynchronous Distributed Synthesis

The asynchronous system model is a generalization of the synchronous model discussed in the previous section. In an asynchronous system, not all processes are scheduled at the same time. We model the scheduler as part of the environment, i.e., at any given time the environment additionally signals whether a process is enabled. The resulting distributed realizability problem is already undecidable for $\mathrm{LTL}$ specifications and systems with more than one process [15].

We have to adapt the definition of the synchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem for the asynchronous setting. Using the definition from Section 3, the system can never satisfy a $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula if the scheduler is part of the environment, since it may delay scheduling indefinitely. Moreover, even if the scheduler is assumed to be fair, it can still build increasing delay blocks between process activation times such that it is impossible for the system to guarantee any bound $k\in\mathbb{N}$. Hence, we employ the concept of bounded fair schedulers and allow the system bound to depend on the scheduler bound. More generally, this is a typical instance of an assume-guarantee specification: under the assumption that the scheduler is bounded fair, the system satisfies its specification. In the following, we formally introduce the distributed realizability problem for asynchronous systems and assume-guarantee specifications.

Scheduling

To model scheduling, we introduce an additional set $\mathit{Sched}={\{\mathit{sched}_{p}\mid p\in P^{-}\}}$ of atomic propositions. The valuation of $\mathit{sched}_{p}$ indicates whether system process $p$ is currently scheduled or not. Given a (synchronous) architecture $\mathcal{A}={\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$, we define the asynchronous architecture $\mathcal{A}^{*}$ as the architecture with the environment output $O^{*}_{{p_{\mathit{env}}}}=O_{{p_{\mathit{env}}}}\cup\mathit{Sched}$. Furthermore, we extend the input $I_{p}$ of a process by its scheduling variable $\mathit{sched}_{p}$, i.e., $I_{p}^{*}=I_{p}\cup{\{\mathit{sched}_{p}\}}$ for each $p\in P^{-}$. The environment can decide at every step which processes to schedule. When a process is not scheduled, its state—and thereby its outputs—do not change [14]. Formally, for $p\in P^{-}$, let $f_{p}$ be a finite-state strategy for a process $p$ and $\mathcal{S}_{p}={\langle S,s_{0},\Delta,l\rangle}$ a transition system that generates $f_{p}$. For every path $w=w_{0}w_{1}w_{2}\cdots\in(2^{I_{p}^{*}})^{\omega}$, it holds that if $\mathit{sched}_{p}\notin w_{i}$ for some $i\in\mathbb{N}$, then $\Delta^{*}(w[i])=\Delta^{*}(w[i+1])$, where $w[i]$ denotes the prefix $w_{0}w_{1}\cdots w_{i}$ of $w$. For the remainder of this section, we will only consider such strategies.

Definition 2** (Assume-Guarantee Realizability).**

A $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee specification ${\langle\varphi,\psi\rangle}$ consists of a pair of $\mathrm{PROMPT}$–$\mathrm{LTL}$ formulas. The asynchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee realizability problem asks, given an asynchronous architecture $\mathcal{A}^{*}$ and ${\langle\varphi,\psi\rangle}$ as above, whether for each process $p\in P^{-}$ there exists a finite-state strategy $f_{p}$ such that for every bound $k$ on the assumption there is a bound $l$ on the guarantee such that for every $w\in\bigotimes_{p\in P^{-}}f_{p}$, we have that $(w,k)\vDash\varphi$ implies $(w,l)\vDash\psi$. In this case, we say that $\bigotimes_{p\in P^{-}}f_{p}$ satisfies ${\langle\varphi,\psi\rangle}$.

Consider the bounded fairness specification discussed above, which is expressed by the formula $\varphi=\bigwedge_{p\in P^{-}}\operatorname{\mathbf{GF_{P}}}\mathit{sched}_{p}$, i.e., for every point in time, every $p$ is scheduled within a bounded number of steps. We use $\varphi$ as an assumption on the environment which implies that the guarantee $\psi$ only has to be satisfied if $\varphi$ holds. Consider, for example, the asynchronous architecture corresponding to Fig. 2(a) and the $\mathrm{PROMPT}$–$\mathrm{LTL}$ specification $\psi=\operatorname{\mathbf{G}}(\operatorname{\mathbf{F_{P}}}c\land\operatorname{\mathbf{F_{P}}}\neg c\land\operatorname{\mathbf{F_{P}}}d\land\operatorname{\mathbf{F_{P}}}\neg d)$. Even when we assume a fair scheduler, i.e., $\varphi=\operatorname{\mathbf{GF}}\mathit{sched}_{p_{1}}\land\operatorname{\mathbf{GF}}\mathit{sched}_{p_{2}}$, the environment can prevent one process from satisfying the specification for any bound $l$. This problem is fixed by assuming the scheduler to be bounded fair, i.e., $\varphi=\operatorname{\mathbf{GF_{P}}}\mathit{sched}_{p_{1}}\land\operatorname{\mathbf{GF_{P}}}\mathit{sched}_{p_{2}}$. Then, there exist realizing implementations for processes $p_{1}$ and $p_{2}$ (that alternate between enabling and disabling the output), and the bound on the guarantee is $l=2\cdot k$ for every bound $k$ on the assumption.

While in the case of $\mathrm{LTL}$ the assume-guarantee problem ${\langle\varphi,\psi\rangle}$ can be reduced to the $\mathrm{LTL}$ realizability problem for the implication $\varphi\rightarrow\psi$, this is not possible in $\mathrm{PROMPT}$–$\mathrm{LTL}$ due to the quantifier alternation on the bounds. As a matter of fact, we do not know yet whether the $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee realizability problem in the single-process case is decidable. We show that even if the problem would turn out to be decidable, an implementation that realizes the specification in general may need infinite memory.

Lemma 3**.**

There exists a $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee specification that can be realized with an infinite-state strategy, but not with a finite-state one.

Proof.

Consider the assume-guarantee specification ${\langle\varphi,\psi\rangle}$ with $\varphi=\operatorname{\mathbf{GF_{P}}}o\lor\operatorname{\mathbf{FG}}\neg o$ and $\psi=\mathbf{ff}$ and a single process architecture with $I=\emptyset$ and $O={\{o\}}$. As the guarantee $\psi$ is false, the implementation has to falsify the assumption $\varphi$ for every bound $k$ on the prompt-eventually operator to realize ${\langle\varphi,\psi\rangle}$. To falsify $\varphi$ with respect to a fixed $k$, the implementation has to produce a sequence $w\in(2^{\{o\}})^{\omega}$ where $o$ is true infinitely often and where $\emptyset^{k}$ is an infix of $w$. Thus, the size of the implementation depends on $k$ and an implementation that falsifies $\varphi$ for every $k$ must have infinite memory. ∎

Moreover, already the $\mathrm{LTL}$ realizability problem is undecidable in the asynchronous case. Thus, the $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee realizability problem for asynchronous architectures may be at best solvable by a semi-decision procedure. We present such a semi-decision procedure for the asynchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee realizability problem based on bounded synthesis [14]. In bounded synthesis, a transition system of a fixed size is “guessed” and model checked by a constraint solver. Model checking for $\mathrm{PROMPT}$–$\mathrm{LTL}$ can be solved by checking pumpable non-emptiness of colored Büchi graphs [6]. However, the pumpability condition cannot directly be expressed in the bounded synthesis constraint system. Hence, in Section 4.1, we give an alternative solution to the non-emptiness of colored Büchi graphs by a reduction to Büchi graphs that have access to the state space of the transition system. We show how to extend bounded synthesis to such Büchi graphs in Section 4.2, and present a semi-decision procedure for $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee synthesis based on this extension in Section 4.3.

In the following we use transition systems as representations for finite-state strategies, since the algorithm developed in this section needs access to the syntactic representation of strategies.

4.1 Nonemptiness of Colored Büchi Graphs

In the case of $\mathrm{LTL}$ specifications, the nonemptiness problem for Büchi graphs gives a classical solution to the model checking problem for a given system $\mathcal{S}$. Let $\varphi$ be the $\mathrm{LTL}$ formula that $\mathcal{S}$ should satisfy. In a preprocessing step, the negation of $\varphi$ is translated to a nondeterministic Büchi word automaton $\mathcal{N}_{\neg\varphi}$ [26]. Then, $\varphi$ is violated by $\mathcal{S}$ if, and only if, the Büchi graph $G$ representing the product of $\mathcal{S}$ and $\mathcal{N}_{\neg\varphi}$ is nonempty. An accepting path $\pi$ in $G$ witnesses a computation of $\mathcal{S}$ that violates $\varphi$. Colored Büchi graphs are an extension to such graphs in the context of model checking $\mathrm{PROMPT}$–$\mathrm{LTL}$ [6].

A colored Büchi graph of degree two is a tuple $G={\langle{\{r,r^{\prime}\}},V,E,v_{0},L,\mathcal{B}\rangle}$, where $r$ and $r^{\prime}$ are propositions, $V$ is a set of vertices, $E\subseteq V\times V$ is a set of edges, $v_{0}\in V$ is the designated initial vertex, $L\colon V\rightarrow 2^{{\{r,r^{\prime}\}}}$ describes the color of a vertex, and $\mathcal{B}={\{B_{1},B_{2}\}}$ is a generalized Büchi condition of index two, i.e., $B_{1},B_{2}\subseteq V$. A Büchi graph is a special case where we omit the labeling function and are interested in finding an accepting path. A path $\pi=v_{0}v_{1}v_{2}\cdots\in V^{\omega}$ is pumpable if we can pump all its $r^{\prime}$-blocks without pumping its $r$-blocks. Formally, a path is pumpable if for all adjacent $r^{\prime}$-change points $i$ and $i^{\prime}$, there are positions $j$, $j^{\prime}$, and $j^{\prime\prime}$ such that $i\leq j<j^{\prime}<j^{\prime\prime}<i^{\prime}$, $v_{j}=v_{j^{\prime\prime}}$ and $r\in L(v_{j})$ if, and only if, $r\notin L(v_{j^{\prime}})$. A path $\pi$ is accepting, if it visits both $B_{1}$ and $B_{2}$ infinitely often. The pumpable nonemptiness problem for $G$ is to decide whether $G$ has a pumpable accepting path. It is NLogSpace-complete and solvable in linear time [6].

We give an alternative solution to this problem based on a reduction to the nonemptiness problem of Büchi graphs. To this end, we construct a non-deterministic safety automaton $\mathcal{N}_{\text{pump}}$ that characterizes the pumpability condition. A non-deterministic safety automaton $\mathcal{N}$ is a tuple ${\langle\Sigma,S,s_{0},\delta\rangle}$, where $\Sigma$ is a finite alphabet, $S$ is a finite set of states, $s_{0}\in S$ is the designated initial state, and $\delta\colon S\times\Sigma\rightarrow 2^{S}$ is the transition function. An infinite word is accepted by a safety automaton $\mathcal{N}$ if, and only if, there exists an infinite run on this word.

Lemma 4**.**

Let $G={\langle{\{r,r^{\prime}\}},V,E,v_{0},L,\mathcal{B}\rangle}$ be a colored Büchi graph of degree two. There exists a Büchi graph $G^{\prime}$, with $\mathcal{O}(\left|{G^{\prime}}\right|)=\mathcal{O}(\left|{G}\right|^{2})$, such that $G$ has a pumpable accepting path if, and only if, $G^{\prime}$ has an accepting path.

Proof.

We define a non-deterministic safety automaton $\mathcal{N}_{\text{pump}}={\langle V\times 2^{\{r,r^{\prime}\}},S,s_{0},\delta\rangle}$ over the alphabet $V\times 2^{{\{r,r^{\prime}\}}}$ that checks the pumpability condition. The product of $G$ and $\mathcal{N}_{\text{pump}}$ (defined later) represents the Büchi graph $G^{\prime}$ where every accepting path is pumpable.

The language $\mathcal{L}\subseteq(V\times 2^{{\{r,r^{\prime}\}}})^{\omega}$ of pumpable paths (with respect to a fixed set of vertices $V$) is an $\omega$-regular language that can be recognized by a small non-deterministic safety automaton. This automaton $\mathcal{N}_{\text{pump}}$ operates in 3 phases between every pair of adjacent $r^{\prime}$-change points: first, it non-deterministically remembers a vertex $v$ and the corresponding truth value of $r$. Then, it checks that this value changes and thereafter it remains to show that the vertex $v$ repeats before the next $r^{\prime}$-change point. Thus, the state space $S$ of $\mathcal{N}_{\text{pump}}$ is

[TABLE]

and the initial state is $s_{0}$. The state space corresponds to the 3 phases: in the states $s_{v,x}$ a vertex $v$ and a truth value of $r$ are remembered, before state $s^{\prime}_{v,y}$ the value of $r$ changes, and $s^{\prime\prime}_{z}$ is the state after the vertex repetition. The transition function $\delta\colon(S\times(V\times 2^{\{r,r^{\prime}\}}))\rightarrow 2^{S}$ is defined in the following. We use the notation $A=_{C}B$ to denote $(A\cap C)=(B\cap C)$.

$\delta(s_{0},(v,x))={\{s_{v,x}\}}$

• 2.

$\delta(s_{v,x},(v^{\prime},x^{\prime}))\ni\begin{cases}s_{v,x}&\text{if }x=_{\{r^{\prime}\}}x^{\prime}\\ s_{v^{\prime},x^{\prime}}&\text{if }x=_{\{r^{\prime}\}}x^{\prime}\\ s^{\prime}_{v,x^{\prime}}&\text{if }x=_{\{r^{\prime}\}}x^{\prime}\text{ and }x\neq_{\{r\}}x^{\prime}\end{cases}$

• 3.

$\delta(s^{\prime}_{v,y},(v^{\prime},x))\ni\begin{cases}s^{\prime}_{v,y}&\text{if }x=_{\{r^{\prime}\}}y\text{ and }v^{\prime}\neq v\\ s^{\prime\prime}_{y\cap{\{r^{\prime}\}}}&\text{if }x=_{\{r^{\prime}\}}y\text{ and }v^{\prime}=v\end{cases}$

• 4.

$\delta(s^{\prime\prime}_{z},(v,x))\ni\begin{cases}s^{\prime\prime}_{z}&\text{if }x=_{\{r^{\prime}\}}z\\ s_{v,x}&\text{if }x\neq_{\{r^{\prime}\}}z\end{cases}$

The size of $\mathcal{N}_{\text{pump}}$ is in $O(\left|{V}\right|)$. Figure 3 gives a visualization of this automaton.

We define the product $G^{\prime}$ of the colored Büchi graph $G={\langle{\{r,r^{\prime}\}},V,E,v_{0},L,\mathcal{B}\rangle}$ and the automaton $\mathcal{N}_{\text{pump}}$ as the Büchi graph $(V\times S,E^{\prime},(v_{0},s_{0}),\mathcal{B}^{\prime})$, where

[TABLE]

and where $\mathcal{B}^{\prime}=(B^{\prime}_{1},B^{\prime}_{2})$ is given by $B^{\prime}_{i}={\{(v,s)\mid v\in B_{i}\text{ and }s\in S\}}$ for $i\in{\{1,2\}}$. The size of $G^{\prime}$ is in $\mathcal{O}(\left|{G}\right|^{2})$. It remains to show that $G$ has a pumpable accepting path if, and only if, $G^{\prime}$ has an accepting path.

Consider a pumpable accepting path $\pi$ in $G$. We show that there is a corresponding accepting path $\pi^{\prime}$ in $G^{\prime}$. Let $i$ and $i^{\prime}$ be adjacent $r^{\prime}$-change points. Then, there are positions $j$, $j^{\prime}$, and $j^{\prime\prime}$ such that $i\leq j<j^{\prime}<j^{\prime\prime}<i^{\prime}$, $v_{j}=v_{j^{\prime\prime}}$ and $r\in L(v_{j})$ if, and only if, $r\notin L(v_{j^{\prime}})$. By construction, at position $i$, automaton $\mathcal{N}_{\text{pump}}$ is at some state from the set ${\{s_{0},s^{\prime\prime}_{\emptyset},s^{\prime\prime}_{\{r^{\prime}\}}\}}$. We follow the automaton and remember vertex $v$ and the truth value of $r$ at position $j\geq i$ (some state $s_{v,x}$). Next, we take the transition to $s^{\prime}_{v,y}$ where the truth value of $r$ changes (at position $j^{\prime}$). Lastly, we check that there is a vertex repetition (at position $j^{\prime\prime}$) and go to state $s^{\prime\prime}_{z}$. At the next $r^{\prime}$-change point $i^{\prime}$, the argument repeats. This path is accepting, as the original one is accepting.

Now, consider an accepting path $\pi$ in $G^{\prime}$. We show that there is a pumpable accepting path in $G$. Let $\pi^{\prime}$ be the projection of every position of $\pi$ to the first component. By construction, $\pi^{\prime}$ is an accepting path in $G$. Let $\pi_{i}\pi_{i+1}\cdots\pi_{i^{\prime}}$ be an $r^{\prime}$-block of $\pi$. As $\pi$ has a run of the automaton $\mathcal{N}_{\text{pump}}$, we know that there exists a state repetition between $i$ and $i^{\prime}$ where the truth value of $r$ changes in between. Hence, the path $\pi^{\prime}$ is pumpable. ∎

Remark 2**.**

Note that in the context of the previous proof, it would be enough to remember a vertex $v$ without the valuation of ${\{r,r^{\prime}\}}$, as the vertex determines the valuation by the labeling function $L\colon v\rightarrow 2^{\{r,r^{\prime}\}}$ of $G$. However, we will later use $\mathcal{N}_{\text{pump}}$ in a more general setting (cf. Section 4.3).

4.2 Bounded Synthesis

Bounded synthesis [14] is a semi-decision procedure for the distributed synthesis problem. In its original form, it takes as input a specification expressed by a universal co-Büchi automaton $\mathcal{U}$, a (possibly asynchronous) architecture $\mathcal{A}$, and a size bound $b$ (or a family of bounds on the individual processes), and decides whether a correct implementation of the given size exists. Bounded synthesis expresses the acceptance of a transition system $\mathcal{S}$ on $\mathcal{U}$, i.e., acceptance of all traces generated by $\mathcal{S}$, as a constraint system in a decidable first-order theory. In this section, we show a modification of bounded synthesis that gives the specification automaton access to the states of the system to be synthesized. This extension is needed for automata that can express the pumpability condition, in particular the one we constructed in the proof of Lemma 4. We will show in Section 4.3 how to obtain such an automaton from a $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee specification ${\langle\varphi,\psi\rangle}$, resulting in a semi-decision procedure for asynchronous distributed synthesis from this class of specifications.

For distributed architectures, bounded synthesis separately considers the problems of finding a global transition system that is accepted by $\mathcal{U}$ and of dividing the transition system into local components according to the given architecture. To this end, two sets of constraints are generated: (i) an encoding of the acceptance by $\mathcal{U}$ of a global transition system $\mathcal{S}$ of size $b$, and (ii) an encoding of the architectural constraints that divides this global system into local components. If the conjunction of both sets of constraints is satisfiable, then a satisfying assignment of the constraints represents a distributed system that satisfies $\varphi$ in $\mathcal{A}$. Since the architectural constraints we consider are the same as in standard bounded synthesis, we only have to modify the constraints encoding the existence of a global transition system that satisfies the given specification.

Extended Automata

We define a universal co-Büchi tree automaton as a tuple \mathcal{U}={\langle\Sigma,\Upsilon,Q,q_{0},\delta,\reflectbox{B}\rangle}, where $\Sigma$ is an input alphabet, $\Upsilon$ is a set of directions, $Q$ is a set of states, $\delta\colon Q\times\Sigma\rightarrow 2^{Q\times\Upsilon}$ is the transition function, and \reflectbox{B}\subseteq Q is the set of rejecting states.

As mentioned above, we want to check acceptance of a global transition system by $\mathcal{U}$. Therefore, we consider the sets of inputs $I=O^{*}_{{p_{\mathit{env}}}}$ and outputs $O=\bigcup_{p\in P^{-}}O^{*}_{p}$ of the composition of the system processes, and are interested in the acceptance of a $2^{O}$-labeled $2^{I}$-transition system $\mathcal{S}={\langle S,s_{0},\Delta,l\rangle}$. In addition, we want to recognize the pumpability condition. Therefore, we consider a state-aware universal co-Büchi tree automaton with $\Sigma=2^{O}\times S$ and $\Upsilon=2^{I}$, i.e., in addition to output valuations, the automaton has access to the current state of $\mathcal{S}$.

Acceptance of $\mathcal{S}$ by the automaton is defined in terms of run graphs: the run graph of an automaton \mathcal{U}_{S}={\langle 2^{O}\times S,2^{I},Q,q_{0},\delta,\reflectbox{B}\rangle} on $\mathcal{S}$ is the minimal directed graph $\mathcal{G}=(G,E)$ that satisfies the constraints:

$G\subseteq Q\times S$,

• 2.

$(q_{0},s_{0})\in G$, and

• 3.

for every $(q,s)\in G$, it holds

[TABLE]

The co-Büchi condition requires that, for an infinite path $g_{0}g_{1}g_{2}\cdots\in G^{\omega}$ of the run graph, g_{i}\in\reflectbox{B}\times S holds for only finitely many $i\in\mathbb{N}$. A run graph is accepting if every infinite path $g_{0}g_{1}g_{2}\cdots\in G^{\omega}$ of the run graph satisfies the co-Büchi condition. A transition system $\mathcal{S}$ is accepted by $\mathcal{U}_{S}$ if the (unique) run graph of $\mathcal{U}_{S}$ on $\mathcal{S}$ is accepting.

Annotated transition systems

We introduce an annotation function for transition systems that witnesses acceptance by a (possibly state-aware) universal co-Büchi tree automaton. The annotation assigns to each pair $(q,s)\in Q\times S$ a natural number or a special symbol $\bot$. Natural numbers indicate the maximal number of occurrences of rejecting states on any path to $(q,s)$ in the run graph; $\bot$ indicates that the pair $(q,s)$ is not reachable. Thus, if for a given transition system there exists an annotation that assigns natural numbers to all vertices of the run graph, then the number of visits to rejecting states must be bounded in any run. Such annotations are called valid, and transition systems with valid annotations are exactly those that are accepted by the automaton.

An annotation of a $2^{O}$-labeled $2^{I}$-transition system $\mathcal{S}={\langle S,s_{0},\Delta,l\rangle}$ on a state-aware universal co-Büchi tree automaton \mathcal{U}_{S}={\langle 2^{O}\times S,2^{I},Q,q_{0},\delta,\reflectbox{B}\rangle} is a function $\lambda\colon Q\times S\rightarrow\{\bot\}\cup\mathbb{N}$. An annotation is valid if it satisfies the following conditions:

$\lambda(q_{0},s_{0})\neq\bot$

• 2.

for any $(q,s)\in Q\times S$:

• if $\lambda(q,s)=n\neq\bot$ and $(q^{\prime},\upsilon)\in\delta(q,(l(s),s))$
• then $\lambda(q^{\prime},\Delta(s,\upsilon))\vartriangleright\lambda(q,s)$,
• where $\vartriangleright$ is interpreted as $>$ if q^{\prime}\in\reflectbox{B}, and $\geq$ otherwise.

An annotation is $c$-bounded if its codomain is contained in $\{\bot,0,\ldots,c\}$.

Theorem 2** (see [14]).**

A finite-state $O$-labeled $I$-transition system $\mathcal{S}={\langle S,s_{0},\Delta,l\rangle}$ is accepted by a state-aware universal co-Büchi tree automaton \mathcal{U}_{S}={\langle 2^{O}\times S,2^{I},Q,q_{0},\delta,\reflectbox{B}\rangle} if, and only if, it has a valid (\left|{S}\right|\cdot\left|{\reflectbox{B}}\right|)-bounded annotation.

Proof.

The original proof by Finkbeiner and Schewe [14] works without modifications for our extension to state-aware universal co-Büchi tree automata. ∎

For a given state-aware universal co-Büchi tree automaton \mathcal{U}_{S}={\langle 2^{O}\times S,2^{I},Q,q_{0},\delta,\reflectbox{B}\rangle}, Theorem 2 allows us to decide the existence of an $O$-labeled $I$-transition system with state space $S$ that is accepted by $\mathcal{U}_{S}$.

Encoding of global acceptance

The existence of a (global) transition system with a valid annotation can be encoded into a set of decidable constraints in first-order logic modulo a theory with uninterpreted functions and a partial order. Essentially, we can directly encode the conditions for a valid annotation into constraints, with uninterpreted transition function and labeling for the desired transition system. Such constraints can then be solved by off-the-shelf satisfiability modulo theories (SMT) tools.

Like the proof of Theorem 2, the original encoding can easily be extended to support our notion of state-aware universal Büchi tree automata. It is constructed in the following way:

Assume that $\mathcal{U}_{S}$ is defined in a suitable way, i.e., the sets $Q$ and

$B$

, state $q_{0}$, and transition relation $\delta\colon Q\times(2^{O}\times S)\rightarrow 2^{(Q\times 2^{I})}$ are defined. 2. 2.

Declare uninterpreted sets and functions for the transition system $\mathcal{S}$ and the annotation:

• (a)

Define the set of states $S$ as $\{1,\ldots,b\}$ for the given bound $b\in\mathbb{N}$.

• (b)

Declare the transition function of $\mathcal{S}$ as $\Delta:S\times 2^{I}\rightarrow S$ and the labeling function as $l:S\rightarrow 2^{O}$.

• (c)

Declare two functions that are used to model the annotation function: $\lambda^{\mathbb{B}}:Q\times S\rightarrow\mathbb{B}={\{\mathbf{tt},\mathbf{ff}\}}$ and $\lambda^{\#}:Q\times S\rightarrow\mathbb{N}$. 3. 3.

Assert the following constraints:

[TABLE]

The encoding ensures that $\lambda^{\mathbb{B}}(q,s)$ is true whenever $(q,s)\in Q\times S$ is reachable in the run graph of $\mathcal{U}_{S}$ on $\mathcal{S}$, and that $\lambda^{\#}$ respects the conditions for a valid annotation for all reachable vertices $(q,s)$. Since there are no conditions for the annotation on vertices that are not reachable, a solution for $\lambda^{\#}$ will represent a valid annotation of $\mathcal{S}$ on $\mathcal{U}_{S}$.

Note that our encoding is a strict generalization of the encoding of Finkbeiner and Schewe [14]. In particular, our encoding can also be used for specifications in $\mathrm{LTL}$ that are translated into a universal co-Büchi tree automaton (see Kupferman and Vardi [27]), which can be seen as a state-aware automaton that ignores the state of the transition system.

Encoding of architectural constraints

As mentioned above, the encoding of architectural constraints can be adopted from the original approach without changes. For a given asynchronous architecture $\mathcal{A}^{*}={\langle P,{p_{\mathit{env}}},\{I^{*}_{p}\}_{p\in P},\{O^{*}_{p}\}_{p\in P}\rangle}$, the additional constraints (1) assert that the state of a process $p\in P^{-}$ does not change if it is not scheduled and (2) that the transitions of a process only depend on its current state and the visible inputs. In addition, it can contain additional bounds on the state space of every single component.

The conjunction of both sets of constraints then asks for the existence of a distributed implementation $\mathcal{S}=\bigotimes_{p\in P^{-}}\mathcal{S}_{p}$ of size $b$ that is accepted by $\mathcal{U}$, possibly with additional bounds $b_{p}$ for every $p\in P^{-}$ on the size of the components.

Theorem 3** (see [14]).**

Given a state-aware universal co-Büchi tree automaton $\mathcal{U}_{S}$ 333As the symbol $S$ in $\mathcal{U}_{S}$ refers to the state-space of the distributed product, $\left|{S}\right|$ has to be equal to the product of bounds $b_{p}$ for $p\in P^{-}$., an asynchronous architecture $\mathcal{A}^{*}$, and a family of bounds $b_{p}$ for every $p\in P^{-}$, there is a constraint system (in a decidable first-order theory) that is satisfiable if, and only if, there exist implementations $\mathcal{S}_{p}$ of size $b_{p}$ for every $p\in P^{-}$ such that $\mathcal{S}=\bigotimes_{p\in P^{-}}\mathcal{S}_{p}$ is accepted by $\mathcal{U}_{S}$ and satisfies the architectural constraints of $\mathcal{A}^{*}$.

Proof.

Follows immediately from Theorem 2 and the correctness of the architectural constraints from Finkbeiner and Schewe [14]. ∎

4.3 A Semi-Decision Procedure for Assume-Guarantee Realizability

Since the assume-guarantee realizability problem for asynchronous architectures is undecidable and infinite-state strategies are required in general, we give a semi-decision procedure for the problem. Our solution is based on the techniques developed in the last subsections.

As the bounded synthesis approach described in the last subsection already accounts for “guessing” transition systems $\mathcal{S}_{p}$ for each system process $p$ according to the architectural constraints given by $\mathcal{A}^{*}$, we reduce the problem of model checking individual implementations $\mathcal{S}_{p}$ to model checking the product system $\mathcal{S}=\bigotimes_{p\in P^{-}}\mathcal{S}_{p}$. A transition system $\mathcal{S}$ satisfies an assume-guarantee specification ${\langle\varphi,\psi\rangle}$ if the strategy $f$ generated by $\mathcal{S}$ satisfies ${\langle\varphi,\psi\rangle}$, i.e., if for every bound $k$ there is a bound $l$ such that for every $w\in f$, we have that $(w,k)\vDash\varphi$ implies $(w,l)\vDash\psi$.

Given an assume-guarantee specification ${\langle\varphi,\psi\rangle}$, we first solve the problem of model checking assume-guarantee specifications by building a state-aware universal co-Büchi tree automaton $\mathcal{U}_{S}$ that accepts a transition system $\mathcal{S}$ if, and only if, $\mathcal{S}$ satisfies ${\langle\varphi,\psi\rangle}$. Given $\mathcal{U}_{S}$ and a bound $b$ on the size of the implementation, we can then use the encoding from Section 4.2 to decide realizability modulo this bound, and obtain a semi-decision procedure by solving the problem for increasing bounds.

Encoding ${\langle\varphi,\psi\rangle}$ into Büchi automata

Let $\mathcal{A}^{*}={\langle P,{p_{\mathit{env}}},\{I^{*}_{p}\}_{p\in P},\{O^{*}_{p}\}_{p\in P}\rangle}$ be an asynchronous architecture and let $I=O^{*}_{{p_{\mathit{env}}}}$ and $O=\bigcup_{p\in P^{-}}O^{*}_{p}$ be the set of inputs and outputs, respectively, of the composition of the system processes. First, we construct the non-deterministic Büchi automaton $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}={\langle 2^{I\cup O\cup{\{r,r^{\prime}\}}},Q,q_{0},\delta,B\rangle}$, where $\overline{c}_{r^{\prime}}(\psi)=\mathit{alt}_{r^{\prime}}\land\neg\mathit{rel}_{r^{\prime}}(\psi)$, whose language contains exactly those paths that satisfy ${\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$ [26]. Then, we use the following lemma to characterize whether a transition system $\mathcal{S}$ satisfies an assume-guarantee specification ${\langle\varphi,\psi\rangle}$ by reducing it to finding pumpable error paths in the two-color Büchi graph $G={\langle{\{r,r^{\prime}\}},V,E,v_{0},L,\mathcal{B}\rangle}$, as introduced in Section 4.1, which is the product of $\mathcal{S}={\langle S,s_{0},\Delta,l\rangle}$ and $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$. Formally, the elements of $G$ are defined as $V=S\times 2^{\{r,r^{\prime}\}}\times Q$, $E$ as $((s,R,q),(s^{\prime},R^{\prime},q^{\prime}))\in E$ if, and only if, there is an input valuation $\vec{i}\in 2^{I}$ such that $s^{\prime}=\Delta(s,\vec{i})$ and $(q^{\prime},\vec{i})\in\delta(q,l(s))$, $v_{0}=(s_{0},\emptyset,q_{0})$, $L$ as $L((s,R,q,q^{*}))=R$, and $\mathcal{B}={\{B\}}$.

Lemma 5**.**

Let ${\langle\varphi,\psi\rangle}$ be a $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee specification, $\mathcal{A}^{*}$ an asynchronous architecture and $\mathcal{S}_{p}$ a finite-state implementation for every system process $p\in P^{-}$. The distributed product $\mathcal{S}=\bigotimes_{p\in P^{-}}\mathcal{S}_{p}$ does not satisfy ${\langle\varphi,\psi\rangle}$ if, and only if, the product of $\mathcal{S}$ and $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$ is pumpable non-empty.

Proof.

Similar to the proof of Lemma 6.1 and Theorem 6.2 in [6]. The missing proof of Lemma 6.1 is given in [8] (Lemma 8). See also the discussion below its proof. ∎

To check the existence of pumpable error paths, we use the non-deterministic automaton $\mathcal{N}_{\text{pump}}={\langle V\times 2^{\{r,r^{\prime}\}},S,s_{0},\delta^{\prime},S\rangle}$ from the proof of Lemma 4. Here, we let $V=X\times Q$, where $X$ is a set with $b$ elements, representing the state space of the desired solution $\mathcal{S}$, and $Q$ is the state space of the automaton $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$ defined above, that is, we use as $V$ the state space $X\times Q$ of the colored Büchi graph that is used to model check an implementation $\mathcal{S}$ against a specification ${\langle\psi,\varphi\rangle}$.

The product of $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$ and $\mathcal{N}_{\text{pump}}$ is an automaton $\mathcal{N}$ that operates on the inputs $I$, outputs $O$, propositions ${\{r,r^{\prime}\}}$, and the state space $X$ of the implementation, and accepts all those paths that are pumpable and violate the assume-guarantee specification (cf. Lemma 4).

Formally, $\mathcal{N}$ is defined as:

[TABLE]

where $\delta^{*}\colon Q\times S\times 2^{I\cup O\cup{\{r,r^{\prime}\}}}\times{\{x\}}\rightarrow 2^{Q\times S}$ is defined as

[TABLE]

and $B^{*}$ is the Büchi condition ${\{(q,s)\mid q\in B,s\in S\}}$.

We complement $\mathcal{N}$, resulting in a universal co-Büchi automaton $\mathcal{U}$ that accepts a given sequence $w\in(2^{I\cup{\{r,r^{\prime}\}}})^{\omega}$ of inputs and the behavior of an implementation $\mathcal{S}$ on $w$ if, and only if, the execution of $\mathcal{S}$ on $w$ satisfies ${\langle\psi,\varphi\rangle}$. Finally, we construct a (state-aware) universal co-Büchi tree automaton \mathcal{U}_{S}=(2^{O}\times X,2^{I\cup{\{r,r^{\prime}\}}},Q,q_{0},\delta,\reflectbox{B}) by spanning a copy of $\mathcal{U}$ for every direction in $2^{I\cup{\{r,r^{\prime}\}}}$. Then, an implementation $\mathcal{S}$ with set $S$ of states is accepted by $\mathcal{U}_{S}$ if, and only if, $\mathcal{S}$ satisfies ${\langle\varphi,\psi\rangle}$ (for all possible input sequences). Thus, $\mathcal{U}_{S}$ solves the problem of model checking assume-guarantee specifications.

Encoding the automaton into constraints

Now, we can use the modified bounded synthesis algorithm from Section 4.2 to encode $\mathcal{U}_{S}$ into a set of constraints that is satisfiable if, and only if, there exists an implementation $\mathcal{S}$ that satisfies ${\langle\varphi,\psi\rangle}$. We obtain the following corollaries stating the correctness of the constraint system for single-process implementations (Corollary 2) and distributed implementations (Corollary 3), respectively.

Corollary 2**.**

Given a $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee specification ${\langle\varphi,\psi\rangle}$ and a bound $b$, there is a constraint system (in a decidable first-order theory) that is satisfiable if, and only if, there exists an implementation $\mathcal{S}$ of size $b$ such that $\mathcal{S}$ satisfies ${\langle\varphi,\psi\rangle}$.

Corollary 3**.**

Given a $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee specification ${\langle\varphi,\psi\rangle}$, an asynchronous architecture $\mathcal{A}^{*}$, and a family of bounds $b_{p}$ for each $p\in P^{-}$, there is a constraint system (in a decidable first-order theory) that is satisfiable if, and only if, there exist implementations $\mathcal{S}_{p}$ of size $b_{p}$ for each $p\in P^{-}$ such that $\bigotimes_{\mathcal{S}\in P^{-}}\mathcal{S}_{p}$ satisfies ${\langle\varphi,\psi\rangle}$ in $\mathcal{A}^{*}$.

By exhaustively traversing the space of bounds $(b_{p})_{p\in P^{-}}$ and by solving the resulting constraint system, we obtain a semi-decision procedure for the asynchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee realizability problem. Furthermore, this also solves the synthesis problem, as a satisfying assignment of the constraint system directly represents a valid implementation, where the transition relation is given by (the assignment of) the function $\Delta$, and the state labeling by (the assignment of) the function $l$.

Corollary 4**.**

Let $\mathcal{A}^{*}$ be an asynchronous architecture. The asynchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ assume-guarantee realizability problem for $\mathcal{A}^{*}$ is semi-decidable.

5 Beyond $\mathrm{PROMPT}$–$\mathrm{LTL}$

In this section, we consider distributed synthesis for logics stronger than $\mathrm{PROMPT}$–$\mathrm{LTL}$. As already pointed out in the introduction, $\mathrm{PROMPT}$–$\mathrm{LTL}$ is predated by parametric linear temporal logic ($\mathrm{PLTL}$), which was introduced by Alur et al. [5]. This logic is obtained by adding parameterized eventually operators of the form $\operatorname{\mathbf{F}}_{\leq x}\varphi$ and parameterized always operators of the form $\operatorname{\mathbf{G}}_{\leq y}$ to $\mathrm{LTL}$. Here, $x$ and $y$ are variables which are instantiated by a variable valuation $\alpha$ mapping variables to natural numbers that serve as bounds: $\operatorname{\mathbf{F}}_{\leq x}\varphi$ holds with respect to $\alpha$ if $\varphi$ holds within the next $\alpha(x)$ steps, while $\operatorname{\mathbf{G}}_{\leq y}\varphi$ holds with respect to $\alpha$, if $\varphi$ holds at least for the next $\alpha(y)$ steps. Thus, intuitively, the variables bound the scope of the operators. In particular, $\mathrm{PROMPT}$–$\mathrm{LTL}$ can be seen as the fragment of $\mathrm{PLTL}$ without parameterized always operators and where all parameterized eventually operators are parameterized by the same variable.

Alur et al. showed that the model checking problem for $\mathrm{PLTL}$, where the variable valuation $\alpha$ is existentially quantified, is PSpace-complete, and therefore not harder than $\mathrm{LTL}$ model checking. Later, a similar result was shown for solving infinite games with $\mathrm{PLTL}$ winning conditions, which is still complete for doubly-exponential time [7]. As for $\mathrm{PROMPT}$–$\mathrm{LTL}$, distributed synthesis for $\mathrm{PLTL}$ specifications has never been considered before.

The second logic we consider in this section is parametric linear dynamic logic ($\mathrm{PLDL}$) [8], which has its roots in another shortcoming of $\mathrm{LTL}$: it lacks the full expressive power of the $\omega$-regular languages. There is a long line of extensions of $\mathrm{LTL}$ addressing this issue [28, 4, 29]. Most recently, Vardi introduced linear dynamic logic ($\mathrm{LDL}$), which adds regular expressions as guards to the temporal operators of $\mathrm{LTL}$: the formula $\langle\/g\/\rangle\,\varphi$ holds if there is a position such that the prefix up to it matches the guard $g$ and $\varphi$ holds at this position. Similarly, $[{\kern 0.83328pt}g{\kern 0.83328pt}]\,\varphi$ holds, if $\varphi$ holds at all positions where the prefix up to it matches the guard. Thus, the diamond operator is a guarded eventually operator and the box operator is a guarded always operator. Vardi showed that $\mathrm{LDL}$ has the exponential compilation property [30], i.e., formulas can be translated into equivalent Büchi automata of exponential size. Thus, $\mathrm{LDL}$ model checking is still PSpace-complete while solving $\mathrm{LDL}$ games is still 2ExpTime-complete.

Now, $\mathrm{PLDL}$ is obtained by allowing parameterized diamond and box operators, with the expected semantics. For the first time, this logic addresses both shortcomings of $\mathrm{LTL}$, lack of timing constraints and limited expressiveness, simultaneously. Even in this setting, model checking is just PSpace-complete and solving games is 2ExpTime-complete [8]. Distributed synthesis for $\mathrm{PLDL}$ specifications has never been considered before.

In this section, we address the distributed synthesis problem for both logics, starting with the synchronous variant. For $\mathrm{PLTL}$, we rely on a reduction to the $\mathrm{PROMPT}$–$\mathrm{LTL}$ synthesis problem. The variable valuation $\alpha$ will be existentially quantified in the problem statement, just as the bound $k$ in the case of $\mathrm{PROMPT}$–$\mathrm{LTL}$ synthesis is existentially quantified. Now, consider a parameterized always operator $\operatorname{\mathbf{G}}_{\leq y}\varphi$: if $\varphi$ is satisfied for at last $\alpha(y)$ steps, then also for at least zero steps, i.e., at the current position. Thus, when the value for $y$ is existentially quantified, $\operatorname{\mathbf{G}}_{\leq y}\varphi$ degenerates to the formula $\varphi$, as $y$ can always be instantiated with [math].

Dually, consider a parameterized eventually operator $\operatorname{\mathbf{F}}_{\leq x}\varphi$: if $\varphi$ holds at least once within the next $\alpha(x)$ steps, then also at least once within the next $k$ steps, for every $k\geq\alpha(x)$. Thus, if $\alpha$ is existentially quantified, then one can replace all variables parameterizing parameterized eventually operators by a unique one. By applying these two replacements, one obtains an equivalent $\mathrm{PROMPT}$–$\mathrm{LTL}$ formula, provided $\alpha$ is existentially quantified. In fact, these observations were the impetus to introduce $\mathrm{PROMPT}$–$\mathrm{LTL}$. However, the situation is different when one is interested in a fixed variable valuation or for optimization problems. In this case, the replacements are no longer valid.

Then, we consider the synchronous synthesis problem for $\mathrm{PLDL}$, which we solve along the same lines as for its special case $\mathrm{PROMPT}$–$\mathrm{LTL}$: the alternating color technique has been reformulated for $\mathrm{PLDL}$ and the exponential compilation property holds as well. Finally, we also discuss the asynchronous synthesis problem. Here, the approach for $\mathrm{PLTL}$ and $\mathrm{PLDL}$ is similar. Hence, we restrict our attention to the case of $\mathrm{PLDL}$, as it subsumes $\mathrm{PLTL}$.

5.1 Synchronous Distributed Synthesis for Parametric Linear Temporal Logic

Let $\mathcal{V}$ be an infinite set of variables and let $\mathrm{AP}$ be a set of atomic propositions. The formulas of $\mathrm{PLTL}$ are given by the grammar

[TABLE]

where $a\in\mathrm{AP}$ and $z\in\mathcal{V}$. As before, we use the derived operators $\operatorname{\mathbf{F}}$ and $\operatorname{\mathbf{G}}$ as well as implications, which are defined as for $\mathrm{PROMPT}$–$\mathrm{LTL}$.

The set of sub-formulas of a $\mathrm{PLTL}$ formula $\varphi$ is denoted by $\mathrm{cl}(\varphi)$ and we define the size of $\varphi$ to be the cardinality of $\mathrm{cl}(\varphi)$. Furthermore, we define

[TABLE]

to be the set of variables parameterizing eventually operators in $\varphi$, and

[TABLE]

to be the set of variables parameterizing always operators in $\varphi$. Finally, $\mathrm{var}(\varphi)=\mathrm{var}_{\mathbf{F}}(\varphi)\cup\mathrm{var}_{\mathbf{G}}(\varphi)$ denotes the set of all variables appearing in $\varphi$.

To evaluate formulas, we define a variable valuation to be a mapping $\alpha\colon\mathcal{V}\rightarrow\mathbb{N}$ mapping each variable to a value. Now, we can define the model relation between a path $w=w_{0}w_{1}w_{2}\cdots$, a position $n$ of $w$, a variable valuation $\alpha$, and a $\mathrm{PLTL}$ formula. For the atomic propositions, Boolean connectives, and standard temporal operators, it is defined as for $\mathrm{PROMPT}$–$\mathrm{LTL}$, while for the parameterized operators it is defined as follows:

$(w,n,\alpha)\vDash\operatorname{\mathbf{F}}_{\leq z}\varphi$ if, and only if, there exists a $j\leq\alpha(z)$ such that $(w,n+j,\alpha)\vDash\varphi$.

• 2.

$(w,n,\alpha)\vDash\operatorname{\mathbf{G}}_{\leq z}\varphi$ if, and only if, for every $j\leq\alpha(z)$: $(w,n+j,\alpha)\vDash\varphi$.

For the sake of brevity, we write $(w,\alpha)\vDash\varphi$ instead of $(w,0,\alpha)\vDash\varphi$ and say that $w$ is a model of $\varphi$ with respect to $\alpha$.

As usual for parameterized temporal logics, the use of variables has to be restricted: parameterizing eventually and always operators by the same variable leads to an undecidable satisfiability problem [5].

Definition 3**.**

A $\mathrm{PLTL}$ formula $\varphi$ is well-formed if $\mathrm{var}_{\mathbf{F}}(\varphi)\cap\mathrm{var}_{\mathbf{G}}(\varphi)=\emptyset$.

In the following, we only consider well-formed formulas and omit the qualifier “well-formed”. Also, we will denote variables in $\mathrm{var}_{\mathbf{F}}(\varphi)$ by $x$ and variables in $\mathrm{var}_{\mathbf{G}}(\varphi)$ by $y$, if the formula $\varphi$ is clear from the context.

Our solution for the $\mathrm{PLTL}$ synthesis problem is based on the monotonicity of the parameterized temporal operators explained earlier, which is formalized in the following lemma.

Lemma 6** ([5]).**

Let $\varphi$ be a $\mathrm{PLTL}$ formula and let $\alpha$ and $\beta$ be variable valuations satisfying $\alpha(x)\leq\beta(x)$, for each $x\in\mathrm{var}_{\mathbf{F}}(\varphi)$, and $\alpha(y)\geq\beta(y)$, for each $y\in\mathrm{var}_{\mathbf{G}}(\varphi)$. If $(w,\alpha)\vDash\varphi$, then $(w,\beta)\vDash\varphi$.

Thus, let $\varphi$ be a $\mathrm{PLTL}$ formula and let $\varphi^{\prime}$ be the $\mathrm{PROMPT}$–$\mathrm{LTL}$-formula obtained from $\varphi$ by inductively replacing each sub-formula $\operatorname{\mathbf{F}}_{\leq x}\psi$ by $\operatorname{\mathbf{F_{P}}}\psi$ and each sub-formula $\operatorname{\mathbf{G}}_{\leq y}\psi$ by $\psi$. The following is a straightforward consequence of the previous lemma.

Corollary 5**.**

Let $\varphi$ be a $\mathrm{PLTL}$ formula and let $\varphi^{\prime}$ be defined as above.

For every $w$, if there exists a variable valuation $\alpha$ such that $(w,\alpha)\vDash\varphi$, then $(w,\max_{x\in\mathrm{var}_{\mathbf{F}}(\varphi)}\alpha(x))\vDash\varphi^{\prime}$. 2. 2.

For every $w$, if there exists a bound $k$ such that $(w,k)\vDash\varphi^{\prime}$, then $(w,\alpha)\vDash\varphi$, where $\alpha$ maps each $x\in\mathrm{var}_{\mathbf{F}}(\varphi)$ to $k$ and each other variable to [math].

Let $\mathcal{A}={\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$ be an architecture. Here, the synchronous $\mathrm{PLTL}$ realizability problem for $\mathcal{A}$ is the problem of deciding, given a $\mathrm{PLTL}$ formula $\varphi$, whether there exist a variable valuation $\alpha$ and a finite-state implementation $f_{p}$, for each process $p\in P^{-}$, such that the distributed product $\bigotimes_{p\in P^{-}}f_{p}$ satisfies $\varphi$ with respect to $\alpha$, i.e., $(\bigotimes_{p\in P^{-}}f_{p},\alpha)\vDash\varphi$. In this case, we say that $\varphi$ is realizable in $\mathcal{A}$.

Theorem 4**.**

Let $\mathcal{A}$ be an architecture. The synchronous $\mathrm{PLTL}$ realizability problem for $\mathcal{A}$ is decidable if, and only if, $\mathcal{A}$ is weakly ordered.

Proof.

Fix an architecture $\mathcal{A}$. By Corollary 5, a given $\mathrm{PLTL}$ formula $\varphi$ is realizable in $\mathcal{A}$ if, and only if, $\varphi^{\prime}$ as defined in the corollary is realizable in $\mathcal{A}$. Thus, Corollary 1 yields the desired result. ∎

Also, bounded synthesis is again applicable, as we can translate the relativized PLTL formulas into universal co-Büchi automata.

5.2 Synchronous Distributed Synthesis for Parametric Linear Dynamic Logic

As before, let $\mathcal{V}$ be an infinite set of variables and let $\mathrm{AP}$ be the set of atomic propositions. The formulas of $\mathrm{PLDL}$ are given by the grammar

[TABLE]

where $a\in\mathrm{AP}$, $z\in\mathcal{V}$, and $\phi$ ranges over propositional formulas over $\mathrm{AP}$. Here, expressions of the form $\varphi?$ are tests, which allow us to nest operators. The sets $\mathrm{var}_{\Diamond}(\varphi)$, $\mathrm{var}_{\Box}(\varphi)$, and $\mathrm{var}(\varphi)$ are defined analogously to the sets $\mathrm{var}_{\mathbf{F}}(\varphi)$, $\mathrm{var}_{\mathbf{G}}(\varphi)$, and $\mathrm{var}(\varphi)$ for $\mathrm{PLTL}$, taking sub-formulas in tests into account.

The satisfaction relation is defined, as before, among a path $w$, a position $n$, a variable valuation $\alpha$, and a formula $\varphi$. First, let the relation $\mathcal{R}(g,w,\alpha)\subseteq\mathbb{N}\times\mathbb{N}$ contain all pairs $(m,n)\in\mathbb{N}\times\mathbb{N}$ such that $w_{m}\cdots w_{n-1}$ matches $g$. Formally, it is defined inductively by

$\mathcal{R}(\phi,w,\alpha)={\{(n,n+1)\mid w_{n}\vDash\phi\}}$ for propositional $\phi$,

• 2.

$\mathcal{R}(\varphi?,w,\alpha)={\{(n,n)\mid(w,n,\alpha)\vDash\varphi\}}$,

• 3.

$\mathcal{R}(g_{0}+g_{1},w,\alpha)=\mathcal{R}(g_{0},w,\alpha)\cup\mathcal{R}(g_{1},w,\alpha)$,

• 4.

$\mathcal{R}(g_{0}\,;g_{1},w,\alpha)={\{(n_{0},n_{2})\mid\exists n_{1}\text{ s.t. }(n_{0},n_{1})\in\mathcal{R}(g_{0},w,\alpha)\text{ and }(n_{1},n_{2})\in\mathcal{R}(g_{1},w,\alpha)\}}$, and

• 5.

$\mathcal{R}(g^{*},w,\alpha)={\{(n,n)\mid n\in\mathbb{N}\}}\cup$

${\{(n_{0},n_{k+1})\mid\exists n_{1},\ldots,n_{k}\text{ s.t. }(n_{j},n_{j+1})\in\mathcal{R}(g,w,\alpha)\text{ for all }j\leq k\}}$.

Then, for atomic formulas and Boolean connectives it is defined as for $\mathrm{PROMPT}$–$\mathrm{LTL}$, while for the four temporal operators, it is defined as follows:

$(w,n,\alpha)\vDash\langle\/g\/\rangle\,\varphi$ if there exists $j\geq 0$ such that $(n,n+j)\in\mathcal{R}(g,w,\alpha)$ and $(w,n+j,\alpha)\vDash\varphi$,

• 2.

$(w,n,\alpha)\vDash[{\kern 0.83328pt}g{\kern 0.83328pt}]\,\varphi$ if for all $j\geq 0$, with $(n,n+j)\in\mathcal{R}(g,w,\alpha)$, we have $(w,n+j,\alpha)\vDash\varphi$,

• 3.

$(w,n,\alpha)\vDash{\langle\/g\/\rangle}_{\!\leq z}\,\varphi$ if there exists $j\leq\alpha(z)$ such that $(n,n+j)\in\mathcal{R}(g,w,\alpha)$ and $(w,n+j,\alpha)\vDash\varphi$, and

• 4.

$(w,n,\alpha)\vDash{[{\kern 0.83328pt}g{\kern 0.83328pt}]}_{\leq z}\,\varphi$ if for all $j\leq\alpha(z)$ with $(n,n+j)\in\mathcal{R}(g,w,\alpha)$, we have $(w,n+j,\alpha)\vDash\varphi$.

Again, we restrict ourselves to well-formed formulas, i.e., those formulas $\varphi$ with $\mathrm{var}_{\Diamond}(\varphi)\cap\mathrm{var}_{\Box}(\varphi)=\emptyset$. With this restriction, Lemma 6 holds for $\mathrm{PLDL}$, too.

Lemma 7**.**

Let $\varphi$ be a $\mathrm{PLDL}$ formula and let $\alpha$ and $\beta$ be variable valuations satisfying $\alpha(x)\leq\beta(x)$, for each $x\in\mathrm{var}_{\Diamond}(\varphi)$, and $\alpha(y)\geq\beta(y)$, for each $y\in\mathrm{var}_{\Box}(\varphi)$. If $(w,\alpha)\vDash\varphi$, then $(w,\beta)\vDash\varphi$.

Recall that the alternating color technique for $\mathrm{PROMPT}$–$\mathrm{LTL}$ replaces every prompt-eventually operator $\operatorname{\mathbf{F_{P}}}\psi$ by a formula that expresses that $\psi$ holds within one color change. In $\mathrm{LTL}$, this is naturally expressed by two nested until operators. In $\mathrm{PLDL}$, parameterized diamond operators, which are the analogues of prompt-eventually operators, are guarded by regular expressions, and, thus, one has to express that both the guard holds and at most one color change occurs. The simplest way to do it is to introduce a change point bounded variant of the diamond-operator (see [8]).

Formally, we add the operator ${\langle\/\cdot\/\rangle}_{\!\mathit{cp}}^{r}\,$ with the following semantics:

$(w,n,\alpha)\vDash{\langle\/g\/\rangle}_{\!\mathit{cp}}^{r}\,\psi$ if there exists a $j\in\mathbb{N}$ s.t. $(n,n+j)\in\mathcal{R}(g,w,\alpha)$, $w_{n}\cdots w_{n+j-1}$ contains at most one $r$-change point, and $(w,n+j,\alpha)\vDash\psi$.

Let $\mathrm{LDL_{cp}}$ be the logic obtained by disallowing parameterized operators but allowing the change point-bounded operator, whose semantics are independent of variable valuations. Hence, we drop them from our notation for the satisfaction relation $\vDash$ and the relation $\mathcal{R}$.

We need the following results from [8] which generalizes the replacement of $\mathrm{PLTL}$ sub-formulas $\operatorname{\mathbf{G}}_{\leq y}\psi$ by $\psi$ with respect to variable valuations mapping $y$ to zero. In $\mathrm{PLDL}$, the situation is different, e.g., the formulas ${[{\kern 0.83328pt}g{\kern 0.83328pt}]}_{\leq y}\,\psi$ and $\psi$ are not necessarily equivalent with respect to variable valuations mapping $y$ to zero, e.g., if $r=\varphi?$ is a test. This test has to be satisfied, even if $\alpha(y)=0$. However, one can easily simplify the guard $g$ to a guard $\widehat{g}$ that captures $g$ when restricted to matchings of length zero.

Lemma 8** ([8]).**

For every $\mathrm{PLDL}$ formula $\varphi$ there is an efficiently constructible $\mathrm{PLDL}$ formula $\varphi^{\prime}$ without paramterized box operators whose size is at most the size of $\varphi$ such that

$\mathrm{var}_{\Diamond}(\varphi)=\mathrm{var}_{\Diamond}(\varphi^{\prime})$, 2. 2.

for each $\alpha$ and each $w$, $(w,\alpha)\vDash\varphi$ implies $(w,\alpha)\vDash\varphi^{\prime}$, and 3. 3.

for each $\alpha$ and each $w$, $(w,\alpha)\vDash\varphi^{\prime}$ implies $(w,\alpha_{0})\vDash\varphi$.

In the third item, $\alpha_{0}$ is the valuation mapping each $x\in\mathrm{var}_{\Diamond}(\varphi)$ to $\alpha(x)$ and each other variable to [math].

Note that the formulas $\varphi$ and $\varphi^{\prime}$ as above are equivalent, if the variable valuation is existentially quantified.

Now, given such a $\mathrm{PLDL}$ formula $\varphi$, let $\mathit{rel}_{r}(\varphi)$ denote the formula obtained from the formula $\varphi^{\prime}$ as in Lemma 8 by inductively replacing each sub-formula ${\langle\/g\/\rangle}_{\!\leq x}\,\psi$ by ${\langle\/g\/\rangle}_{\!\mathit{cp}}^{r}\,\psi$. Furthermore, let $\mathit{alt}_{r}=[{\kern 0.83328pt}\mathbf{tt}^{*}{\kern 0.83328pt}]\,\langle\/\mathbf{tt}^{*}\/\rangle\,r\wedge[{\kern 0.83328pt}true^{*}{\kern 0.83328pt}]\,\langle\/\mathbf{tt}^{*}\/\rangle\,\neg r$, which is equivalent to the $\mathrm{LTL}$ formula $\operatorname{\mathbf{GF}}r\wedge\operatorname{\mathbf{GF}}\neg r$ from above. Now, define $c_{r}(\varphi)=\mathit{rel}_{r}(\varphi)\wedge\mathit{alt}_{r}$, which is an $\mathrm{LDL_{cp}}$ formula.

Lemma 9** ([8]).**

Let $\varphi$ be a $\mathrm{PLDL}$ formula and let $w\in\left(2^{\mathrm{AP}}\right)^{\omega}$.

If $(w,\alpha)\vDash\varphi$, then $w^{\prime}\vDash c_{r}(\varphi)$ for every $k$-spaced $r$-coloring $w^{\prime}$ of $w$, where $k=\max_{x\in\mathrm{var}_{\Diamond}(\varphi)}\alpha(x)$. 2. 2.

If $w^{\prime}$ is a $k$-bounded $r$-coloring of $w$ with $w^{\prime}\vDash c_{r}(\varphi)$, then $(w,\alpha)\vDash\varphi$, where $\alpha$ maps each $x\in\mathrm{var}_{\Diamond}(\varphi)$ to $2k$ and each other variable to zero.

Finally, the exponential compilation property holds for $\mathrm{LDL_{cp}}$ as well: every $\mathrm{LDL_{cp}}$ formula can be translated into an equivalent non-determinstic Büchi automaton of exponential size [8].

Now, the (synchronous) $\mathrm{PLDL}$ distributed synthesis problem is defined as its analogue for $\mathrm{PLTL}$. Let $\mathcal{A}={\langle P,{p_{\mathit{env}}},\{I_{p}\}_{p\in P},\{O_{p}\}_{p\in P}\rangle}$ be an architecture. Then, the synchronous $\mathrm{PLDL}$ realizability problem for $\mathcal{A}$ is the problem of deciding, given a $\mathrm{PLDL}$ formula $\varphi$, whether there exist a variable valuation $\alpha$ and a finite-state implementation $f_{p}$ for each process $p\in P^{-}$, such that the distributed product $\bigotimes_{p\in P^{-}}f_{p}$ satisfies $\varphi$ with respect to $\alpha$, i.e., $(\bigotimes_{p\in P^{-}}f_{p},\alpha)\vDash\varphi$. In this case, we say that $\varphi$ is realizable in $\mathcal{A}$.

Theorem 5**.**

Let $\mathcal{A}$ be an architecture. The synchronous $\mathrm{PLDL}$ realizability problem for $\mathcal{A}$ is decidable if, and only if, $\mathcal{A}$ is weakly ordered.

Proof.

Theorem 1 holds for $\mathrm{PLDL}$ as well, using the same proof: a $\mathrm{PLDL}$ formula $\varphi$ is realizable in $\mathcal{A}$ if, and only if, $c_{r}(\varphi)$ is realizable in $\mathcal{A}^{r}$. Now, the information fork criterion holds for $\omega$-regular conditions as well [13], which finishes the proof. ∎

Also, bounded synthesis is again applicable, as we can also translate the relativized PLDL formulas into universal co-Büchi automata.

5.3 Asynchronous Distributed Synthesis for PLDL

Finally, we consider the asynchronous setting. We focus on $\mathrm{PLDL}$, as $\mathrm{PLTL}$ is a fragment of $\mathrm{PLDL}$ and the approach for both problems is similar.

As for the asynchronous $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem, we require the implementations to only change their state if they are scheduled. Here, a $\mathrm{PLDL}$ assume-guarantee specification ${\langle\varphi,\psi\rangle}$ consists of a pair of $\mathrm{PLDL}$ formulas. The asynchronous $\mathrm{PLDL}$ assume-guarantee realizability problem asks, given an asynchronous architecture $\mathcal{A}^{*}$ and ${\langle\varphi,\psi\rangle}$ as above, whether there exists a finite-state implementation $f_{p}$, for each process $p\in P^{-}$, such that for each variable valuation $\alpha$ there is a variable valuation $\beta$ such that for each $w\in\bigotimes_{p\in P^{-}}f_{p}$, we have that $(w,\alpha)\vDash\varphi$ implies $(w,\beta)\vDash\psi$. In this case, we say that $\bigotimes_{p\in P^{-}}f_{p}$ satisfies ${\langle\varphi,\psi\rangle}$.

To solve the problem, we use the framework of bounded synthesis and emptiness checking for Büchi graphs as presented for $\mathrm{PROMPT}$–$\mathrm{LTL}$ in Section 4. In particular, we adapt the notation introduced in Subsection 4.3, e.g., the product system $\mathcal{S}=\bigotimes_{p\in P^{-}}\mathcal{S}_{p}$. Our semi-decision procedure again guesses implementations and then model checks whether their product $\mathcal{S}$ satisfies the assume-guarantee specification, based on a characterization in terms of $\mathcal{S}$ being pumpable non-empty. To this end, we have to lift Lemma 11 to $\mathrm{PLDL}$, which again requires to remove parameterized box operators. Once more, we rely on monotonicity, but due to the quantifier alternation and the implication between $\varphi$ and $\psi$, the application is not completely trivial. Given the assumption $\varphi$, let $\varphi^{\prime}$ be the formula as described in Lemma 8, which has no parameterized box operators. The formula $\psi^{\prime}$ is defined similarly.

Lemma 10**.**

Let $\mathcal{S}$, $\varphi^{\prime}$, and $\varphi^{\prime}$ as above. Then, $\mathcal{S}$ satisfies ${\langle\varphi,\psi\rangle}$ if, and only if, $\mathcal{S}$ satisfies ${\langle\varphi^{\prime},\psi^{\prime}\rangle}$.

Proof.

Let $f$ denote the strategy generated by $\mathcal{S}$.

For the implication from left to right, let $\mathcal{S}$ satisfy ${\langle\varphi,\psi\rangle}$, i.e., for each $\alpha$ there is a $\beta$ such that for all $w\in f$: $(w,\alpha)\vDash\varphi$ implies $(w,\beta)\vDash\psi$. As $\beta$ depends on $\alpha$, we write $\beta(\alpha)$ to make the dependency clear.

Now, given some arbitrary $\alpha$ let $\alpha_{0}$ denote the variable valuation mapping each $x\in\mathrm{var}_{\Diamond}(\varphi)=\mathrm{var}_{\Diamond}(\varphi^{\prime})$ to $\alpha(x)$ and each other variable to [math]. We claim that $(w,\alpha)\vDash\varphi^{\prime}$ implies $(w,\beta(\alpha_{0}))\vDash\psi^{\prime}$ for all $w\in f$, which implies that $\mathcal{S}$ satisfies ${\langle\varphi^{\prime},\psi^{\prime}\rangle}$.

Thus, assume the assumption is satisfied, i.e., $(w,\alpha)\vDash\varphi^{\prime}$. Then, we also have $(w,\alpha_{0})\vDash\varphi$ by Lemma 8. Thus, $(w,\beta(\alpha_{0}))\vDash\psi$, which implies $(w,\beta(\alpha_{0}))\vDash\psi^{\prime}$, again by Lemma 8.

For the other implication, let $\mathcal{S}$ satisfy ${\langle\varphi^{\prime},\psi^{\prime}\rangle}$, i.e., for each $\alpha$ there is a $\beta$ such that for all $w\in f$: $(w,\alpha)\vDash\varphi^{\prime}$ implies $(w,\beta)\vDash\psi^{\prime}$. Again, as $\beta$ depends on $\alpha$, we write $\beta(\alpha)$ to make the dependency clear.

We claim that $(w,\alpha)\vDash\varphi$ implies $(w,\beta(\alpha))\vDash\psi$ for all $w\in f$, which implies that $\mathcal{S}$ satisfies ${\langle\varphi,\psi\rangle}$.

Thus, assume the assumption is satisfied, i.e., $(w,\alpha)\vDash\varphi$. Then, we also have $(w,\alpha)\vDash\varphi^{\prime}$ by Lemma 8. Thus, $(w,\beta(\alpha))\vDash\psi^{\prime}$, which implies $(w,(\beta(\alpha))_{0})\vDash\psi$, again by Lemma 8. Here, $(\beta(\alpha))_{0}$ maps each variable in $\mathrm{var}_{\Diamond}(\psi)=\mathrm{var}_{\Diamond}(\psi^{\prime})$ to $(\beta(\alpha))(x)$ and each other variable to [math]. ∎

To simplify the notation we can assume that $\varphi$ and $\psi$ do not contain any parameterized box operators. Thus, the alternating color technique is applicable to them. Also, there is a non-deterministic Büchi automaton $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}={\langle 2^{I\cup O\cup{\{r,r^{\prime}\}}},Q,q_{0},\delta,B\rangle}$, where $\overline{c}_{r^{\prime}}(\psi)=\mathit{alt}_{r^{\prime}}\land\neg\mathit{rel}_{r^{\prime}}(\psi)$ whose language contains exactly those paths that satisfy ${\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$ [8]. Then, Lemma 11 holds in this setting as well.

Lemma 11**.**

Let ${\langle\varphi,\psi\rangle}$ be a PLDL assume-guarantee specification, $\mathcal{A}^{*}$ be an asynchronous architecture, and $\mathcal{S}_{p}$ be a finite-state implementation for each system process $p\in P^{-}$. The distributed product $\mathcal{S}=\bigotimes_{p\in P^{-}}\mathcal{S}_{p}$ does not satisfy ${\langle\varphi,\psi\rangle}$ if, and only if, the product of $\mathcal{S}$ and $\mathcal{N}_{\overline{c}_{r^{\prime}}(\psi)\land c_{r}(\varphi)}$ is pumpable non-empty.

From here on the algorithm is similar to that described in Section 4 and we obtain the same semi-decidability result.

Corollary 6**.**

Let $\mathcal{A}^{*}$ be an asynchronous architecture. The asynchronous PLDL assume-guarantee realizability problem for $\mathcal{A}^{*}$ is semi-decidable.

6 Conclusion

In this paper, we have initiated the investigation of distributed synthesis for parameterized specifications, in particular for $\mathrm{PROMPT}$–$\mathrm{LTL}$, PLTL, and PLDL. These logics subsume $\mathrm{LTL}$, and additionally allow to express bounded satisfaction of system properties, instead of only eventual satisfaction. To the best of our knowledge, this is the first treatment of parametrized temporal logic specifications in distributed synthesis.

We have shown that for the case of synchronous distributed systems, we can reduce the $\mathrm{PROMPT}$–$\mathrm{LTL}$ synthesis problem to an $\mathrm{LTL}$ synthesis problem. Thus, the complexity of $\mathrm{PROMPT}$–$\mathrm{LTL}$ synthesis corresponds to the complexity of $\mathrm{LTL}$ synthesis, and the $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem is decidable if, and only if, the $\mathrm{LTL}$ realizability problem is decidable. For the case of asynchronous distributed systems with multiple components, the $\mathrm{PROMPT}$–$\mathrm{LTL}$ realizability problem is undecidable, again corresponding to the result for $\mathrm{LTL}$. For this case, we give a semi-decision procedure based on a novel method for checking emptiness of two-colored Büchi graphs. Finally, we have shown that all these results also hold for $\mathrm{PLTL}$ and $\mathrm{PLDL}$. Furthermore, the approach is also applicable to $\mathrm{PLTL}$ and $\mathrm{PLDL}$ in a weighted setting [9], as even these logics have the exponential compilation property and the alternating color technique is applicable to them as well. Finally, we conjecture that the approach also extends to assume-guarantee synthesis with mutual assumptions between different processes [31, 32].

Among the problems that remain open is realizability of $\mathrm{PROMPT}$–$\mathrm{LTL}$ specifications in asynchronous distributed systems with a single component. This problem can be reduced to the (single-process) assume-guarantee realizability problem for $\mathrm{PROMPT}$–$\mathrm{LTL}$, which was left open in [6].

In the future, we also want to look into the synthesis of distributed systems with a parametric number of components [33, 34] from parameterized temporal logics. In addition to the even more difficult problems of realizability and synthesis, new questions arise in this context, such as: how does the bound on prompt eventualities increase with the number of components in the system?