Synthesis with Guided Environments

Synthesis is the automated construction of a system from its specification [5]. Given a linear temporal logic (LTL) formula \(\varphi \) over sets I and O of input and output signals, the goal is to return a transducer that realizes \(\varphi \). At each moment in time, the transducer reads a truth assignment, generated by the environment, to the signals in I, and generates a truth assignment to the signals in O. This process continues indefinitely, generating an infinite computation in \((2^{I \cup O})^\omega \). The transducer realizes \(\varphi \) if its interactions with all environments generate computations that satisfy \(\varphi \) [23].

The fact the system has to satisfy its specification in all environments has led to a characterization of the environment as hostile. In particular, in the game that corresponds to synthesis, the objective of the environment is to violate the specification \(\varphi \). In real-life applications, the satisfaction of the specification is often also in the environment’s interest. In particular, in cases where the system serves or guides the environment, we can expect the environment to follow guidance from the system. We introduce and study synthesis with guided environments (SGE, for short), where the system may harness the knowledge and computational power of the environment during the interaction, guiding it how to assign values to some of the output signals.

Specifically, in SGE, the set O of output signals is partitioned into sets \(C\) and \(G\) of controlled and guided signals. Then, a system that is synthesized by SGE assigns values to the signals in \(C\) and guides the environment how to assign values to the signals in \(G\). Clearly, not all output signals may be guided to the environment. For example, physical actions of the system, like closing a gate or raising a robot arm, cannot be performed by the environment. In addition, it may be the case that the system cannot trust the environment to follow instructions for some of the output signals. As argued above, however, in many cases we can expect the environment to follow the system’s guidance, and require the system to satisfy the specification only when the environment follows its guidance. Indeed, when we go to the cinema and end up seeing a bad movie, we cannot blame a recommendation system that guided us not to choose this movie. The recommendation system is bad (violates its specification, in our synthesis story) only if a user that follows its guidance is disappointed.¹

One advantage of SGE is that it enables a decomposition of the satisfaction task between the system and the environment. We will get back to this point after we describe the setting in more detail. The main advantage of SGE, however, has to do with partial visibility, namely the setting where the set I of input signals is partitioned into sets V and \(H\) of visible and hidden signals, and the systems views only the signals in V. Partial visibility makes synthesis much harder, as the hidden signals still appear in the specification, yet the behavior of the system should be independent of their truth values.

Synthesis with partial visibility has been the subject of extensive research. One line of work studies the technical challenges in solving the problem [7, 20, 25]. Essentially, in a setting with full visibility, the interaction between the system and the environment induces a single computation and hence a single run of a deterministic automaton for the specification. Partial visibility forces the algorithm to maintain subsets of states of the automaton. Indeed, now the interaction induces several computations, obtained by the different possible assignments to the hidden signals. This makes synthesis with partial visibility exponentially harder than synthesis with full visibility for specifications given by automata. When the specification is given by an LTL formula, this exponential price is dominated by the doubly-exponential translation of LTL formulas to deterministic automata, thus LTL synthesis with partial visibility is 2EXPTIME-complete, and is not harder than LTL synthesis with full visibility [26].

A second line of work studies different settings in which partial visibility is present. This includes, for example, distributed systems [21, 24, 28], systems with controlled sensing [2, 9] or with assumptions about visibility [14], and systems that maintain privacy [18, 31]. Finally, researchers have studied alternative forms of partial visibility (e.g., perspective games, where visibility of all signals is restricted in segments of the interaction), as well as partial visibility in richer settings (e.g., multi-agent [3, 4, 15] or stochastic [8, 16] systems) or in problems that are strongly related to synthesis (e.g., control [17], planning [10], and rational synthesis [6, 13]).

To the best of our knowledge, in all settings in which synthesis with partial visibility has been studied so far, there is no attempt to make use of the fact that the assignments to the hidden signals are known to the environment. In SGE, the instructions that the system sends to the environment may refer to the values of the hidden signals. Thus, the outcome of SGE is a transducer with a guided environment (TGE): a transducer whose transitions depend only on the assignments to the signals in V, it assigns values to the signals in \(C\), and instructs the environment how to assign values to the signals in \(G\) using programs that may refer to the values of the signals in \(H\).

Consider, for example, a system in a medical clinic that directs patients “if you come for a vaccine, go to the first floor; if you come to the pharmacy, go to the second floor”. Such a system is as correct as a system that asks customers for the purpose of their visit and then outputs the floor to which they should go. Clearly, if the customers prefer not to reveal the purpose of their visit, we can direct them only with a system of this type. This is exactly what SGE does: it replaces assignments that depend on hidden signals or are complicated to compute with instructions to the environment. As another example, consider a smart-home controller that manages various smart devices within a home by getting inputs from devices like thermostats and security cameras, and generating outputs to devices like lighting systems or smart locks. When it is desirable to hide from the controller information like sleep patterns or number of occupants, we can do that by limiting its input, and guiding the user about the activation of some output devices, for example with instructions like, “if you expect guests, unlock the backyard gate". In the full version, we describe more elaborated examples, in particular of a server that directs users who want to upload data to a cloud. The users may hide from the server the sensitivity level of their data, and we can expect them to follow instructions that the server issues, for example instructions to use storage of high security only when the data they upload is sensitive.

We study several aspects of SGE. We start by examining the memory used by the environment. Clearly, this memory can be used to reduce the state space of the TGE. To see this, note that in an extreme setting in which the TGE can guide all output signals, it can simply instruct the environment to execute a transducer that realizes the specification. Beyond a trade-off between the size of the TGE and the memory of the environment, we discuss how the size of the memory depends on the sets of visible and guided signals. For example, we show that, surprisingly, having more guided signals does not require more memory, yet having fewer guided signals may require more memory.

We then describe an automata-based solution for SGE. The main challenge in SGE is as follows. Consider a system that views only input signals in V. Its interactions with environments that agree on the signals in V generate the same response. In synthesis with partial visibility, this is handled by universal tree automata that run on trees with directions in \(2^V\), thus trees whose branches correspond to the interaction from the point of view of the system [20]. In the setting of SGEs, the interactions with different environments that agree on the signals in V still generate the same response, but this response now involves programs that guide the environment on how to assign values to signals in \(G\) based on the values assigned to the signals in \(H\). As a result, the computations induced by these interactions may differ (not only on \(H\) but also on \(G\)). This differences between SGE and traditional synthesis with partial visibility is our main technical challenge. We show that we can still reduce SGE to the nonemptiness problem of universal co-Büchi tree automata, proving that SGE for LTL specifications is 2EXPTIME-complete. In more detail, given an LTL formula \(\varphi \) and a bound k on the memory that the environment may use, the constructed automaton is of size exponential in \(|\varphi |\) and linear in k, making SGE doubly-exponential in \(|\varphi |\) and exponential in k. Finally, we prove a doubly-exponential upper bound on the size of the memory needed by the environment, leading to an overall triply-exponential upper bound for the SGE problem with unbounded environment memory.

We continue and study the domain of programs that TGEs use. Recall that these programs instruct the environment how to update its memory and assign values to the guided signals, given a current memory state and the current assignment to the hidden signals. Thus, for a memory state space M, each program is of the form \(p:M \times 2^H\rightarrow M \times 2^G\). We study ways to reduce the domain \(2^{H}\), which is the most dominant factor. The reduction depends on the specification \(\varphi \) we wish to synthesize. We argue that the SGE algorithm can restrict attention to tight programs: ones whose domain is a set of predicates over \(H\) obtained by simplifying propositional sub-formulas of \(\varphi \). Further simplification is achieved by exploiting the fact that programs are called after an assignment to the signals in \(V \cup C\) has been fixed, and exploiting dependencies among all signals.

We conclude with directions for future research. Beyond extensions of the many settings in which synthesis has been studied to a setting with guided environments, we discuss two directions that are more related to “the guided paradigm” itself: settings with dynamic hiding and guidance of signals, thus when \(H\) and \(G\) are not fixed throughout the interaction; and bounded SGE, where, as in traditional synthesis [19, 29], beyond a bound on the memory used by the environment, there are bounds on the size of the state space of the TGE and possibly also on the size of the state space of its environment.

We describe on-going behaviors of reactive systems using the linear temporal logic LTL [22]. We consider systems that interact via sets I and O of input and output signals, respectively. Formulas of LTL are defined over \(I \cup O\) using the usual Boolean operators and the temporal operators \(\textbf{G}\) (“always") and \(\textbf{F}\) (“eventually"), \(\textbf{X}\) (“next time”) and \(\textbf{U}\) (“until”). The semantics of LTL is defined with respect to infinite computations in \((2^{I \cup O})^\omega \). Thus, each LTL formula \(\varphi \) over \(I \cup O\) induces a language \(L_\varphi \subseteq (2^{I \cup O})^\omega \) of all computations that satisfy \(\varphi \).

The length of an LTL formula \(\varphi \), denoted \(|\varphi |\), is the number of nodes in the generating tree of \(\varphi \). Note that \(|\varphi |\) bounds the number of sub-formulas of \(\varphi \).

We model reactive systems that interact with their environments by finite-state transducers. A transducer is a tuple \(\mathcal {T}=\langle I,O,S,s_0,\delta ,\tau \rangle \), where I and O are sets of input and output signals, S is a finite set of states, \(s_0\in S\) is an initial state, \(\delta :S\times 2^I\rightarrow S\) is a transition function, and \(\tau : S \times 2^I \rightarrow 2^O\) is a function that labels each transition by an assignment to the output signals. Given an infinite sequence \(w_{I}=i_1\cdot i_2\cdots \in (2^I)^{\omega }\) of assignments to input signals, \(\mathcal {T}\) generates an infinite sequence \(w_{O}=o_1\cdot o_2\cdots \in (2^O)^{\omega }\) of assignments to output signals. Formally, a run of \(\mathcal {T}\) on \(w_{I}\) is an infinite sequence of states \(s_0\cdot s_1\cdot s_2\cdots \), where for all \(j \ge 1\), we have that \(s_j=\delta (s_{j-1},i_j)\). Then, the sequence \(w_O\) is obtained from the assignments along the transitions that the run traverses. Thus for all \(j \ge 1\), we have that \(o_j=\tau (s_{j-1},i_j)\). We define the computation of \(\mathcal {T}\) on \(w_{I}\) to be the word \(\mathcal {T}(w_{I})=(i_1\cup o_1)\cdot (i_2\cup o_2)\cdots \in (2^{I\cup O})^{\omega }\).

For a specification language \(L_\varphi \subseteq (2^{I\cup O})^{\omega }\), we say that \(\mathcal {T}\) (I, O)-realizes \(L_\varphi \) if for every input sequence \(w_{I}\in (2^I)^{\omega }\), we have that \(\mathcal {T}(w_{I}) \in L_\varphi \). In the synthesis problem, we are given a specification language \(L_\varphi \) and a partition of the signals to I and O, and we have to return a transducer that (I, O)-realizes \(L_\varphi \) (or determine that \(L_\varphi \) is not realizable). The language \(L_\varphi \) is typically given by an LTL formula \(\varphi \). We then talk about realizability or synthesis of \(\varphi \).

In synthesis with partial visibility, we seek a system that satisfies a given specification in all environments even when it cannot observe the assignments to some of the input signals. Formally, the set of input signals is partitioned into visible and hidden signals, thus \(I=V\cup H\). The specification \(\varphi \) is still over \(V\cup H\cup O\), yet the behavior of the transducer that models the system is independent of \(H\). Formally, \(\mathcal {T}=\langle V,H,O,S,s_0,\delta ,\tau \rangle \), where now \(\delta :S\times 2^V\rightarrow S\) and \(\tau : S \times 2^V\rightarrow 2^O\). Given an infinite sequence \(w_{I}=(v_1 \cup h_1)\cdot (v_2 \cup h_2) \cdots \in (2^{V\cup H})^{\omega }\), the run and computation of \(\mathcal {T}\) on \(w_I\) is defined as in the case of full visibility, except that now, for all \(j \ge 1\), we have that \(s_j=\delta (s_{j-1},v_j)\) and \(o_j=\tau (s_{j-1},v_j)\).

We can now define a transducer with a guided environment (TGE for short). TGEs extend traditional transducers by instructing the environment how to manage its guided signals. A TGE may be executed in a setting with partial visibility, thus \(I = V\cup H\). It uses the fact that the signals in \(H\) are known to the environment, and it guides the assignment to some of the output signals to the environment. In practice, not all output signals can be guided. Formally, the set of output signals is partitioned into controlled and guided signals, thus \(O=C\cup G\). In each transition, the TGE assigns values to the signals in \(C\) and instructs the environment how to assign values to the signals in \(G\). The environment may have a finite memory, in which case the transducer also instructs the environment how to update the memory in each transition. The instructions that the transducer generates are represented by programs, defined below.

Consider a finite set M of memories, and sets \(H\subseteq I\) and \(G\subseteq O\) of input and output signals. Let \(\mathcal {P}_{M,H,G} = (M\times 2^G)^{M \times 2^H}\) denote the set of propositional programs that update the memory state and assign values to signals in \(G\), given a memory in M and an assignment to the signals in \(H\). Note that each member of \(\mathcal {P}_{M,H,G}\) is of the form \(p:M \times 2^H\rightarrow M\times 2^G\). For a program \(p\in \mathcal {P}_{M,H,G}\), let \(p_M:M\times 2^H\rightarrow M\) and \(p_G:M\times 2^H\rightarrow 2^G\) be the projections of p onto M and \(G\) respectively. Thus, \(p(m,h)=\langle p_M(m,h),p_G(m,h)\rangle \) for all \(\langle m,h\rangle \in M\times 2^H\). In Section 5 we discuss ways to restrict the set of programs that a TGE may suggest to its environment without affecting the outcome of the synthesis procedure.

Now, a TGE is \(\mathcal {T}=\langle V,H,C,G,S,s_0,\delta ,M,m_0,\tau \rangle \), where \(V\) and \(H\) are sets of visible and hidden input signals, \(C\) and \(G\) are sets of controlled and guided output signals, S is a finite set of states, \(s_0 \in S\) is an initial state, \(\delta :S\times 2^V\rightarrow S\) is a transition function, M is a set of memories that the environment may use, \(m_0 \in M\) is an initial memory, and \(\tau :S\times 2^V\rightarrow 2^C\times \mathcal {P}_{M,H,G}\) labels each transition by an assignment to the controlled output signals and a program. Note that \(\delta \) and \(\tau \) are independent of the signals in \(H\), and that \(\tau \) assigns values to the signals in \(C\) and instructs the environment how to use the signals in \(H\) in order to assign values to the signals in \(G\). The latter reflects the fact that the environment does view the signals in \(H\), and constitute the main advantage of TGEs over standard transducers.

Given an infinite sequence \(w_{I}=(v_1 \cup h_1)\cdot (v_2 \cup h_2) \cdots \in (2^{V\cup H})^{\omega }\), the run of \(\mathcal {T}\) on \(w_{I}\) is obtained by applying \(\delta \) on the restriction of \(w_{I}\) to \(V\). Thus, \(r=s_0\cdot s_1\cdot s_2\cdots \), where for all \(j \ge 1\), we have that \(s_{j}=\delta (s_{j-1},v_j)\). The interaction of \(\mathcal {T}\) with the environment generates an infinite sequence \(w_C=c_1 \cdot c_2 \cdot c_3 \cdots \in (2^C)^\omega \) of assignments to the controlled signals, an infinite sequence \(w_M=m_0\cdot m_1\cdot m_2 \cdots \in M^\omega \) of memories, and an infinite sequence \(w_P = p_1\cdot p_2\cdot p_3\cdots \in (\mathcal {P}_{M,H,G})^\omega \) of programs, which in turn generates an infinite sequence \(w_G=d_1 \cdot d_2 \cdot d_3 \cdots \in (2^G)^\omega \) of assignments to the guided signals. Formally, for all \(j \ge 1\), we have that \(\langle c_j,p_j\rangle = \tau (s_{j-1},v_j)\) and \(\langle m_j,d_j\rangle =p_j(m_{j-1},h_j)\). The computation of \(\mathcal {T}\) on \(w_{I}\) is then \(\mathcal {T}(w_{I})=(v_1 \cup h_1 \cup c_1\cup d_1)\cdot (v_2 \cup h_2 \cup c_2\cup d_2) \cdots \in (2^{V\cup H\cup C \cup G})^{\omega }\).

Note that while the domain of the programs in \(\mathcal {P}_{M,H,G}\) is \(M \times 2^H\), programs are chosen in \(\mathcal {T}\) along transitions that depend on \(2^V\). Thus, effectively, assignments made by programs depend on signals in both \(H\) and \(V\).

For a specification language \(L_\varphi \subseteq (2^{I\cup O})^{\omega }\), partitions \(I=V\cup H\) and \(O=C\cup G\), and a bound \(k \ge 1\) on the memory that the environment may use, we say that a TGE \(\mathcal {T}\), \((V,H,C,G)\)-realizes \(L_\varphi \) with memory k, if \(\mathcal {T}=\langle V,H,C,G,S,s_0,\delta ,M,m_0,\tau \rangle \), with \(|M|=k\), and \(\mathcal {T}(w_{I}) \in L_\varphi \), for every input sequence \(w_{I}\in (2^I)^{\omega }\). Then, in the synthesis with guided environment problem (SGE, for short), given such a specification \(L_\varphi \subseteq (2^{I \cup O})^\omega \), a bound \(k\ge 1\) and partitions \(I=V\cup H\) and \(O=C\cup G\), we should construct a TGE with memory k that \((V,H,C,G)\)-realizes \(L_\varphi \) (or determine that no such TGE exists).

Let us consider the special case of TGEs that operate in an environment with no memory, thus \(M=\{m\}\), for a single memory state m. Consider first the setting where \(\mathcal {T}\) has full visibility, thus \(V=I\) and \(H=\emptyset \). Then, programs are of the form \(p:{\{m\}}\times 2^{\emptyset }\rightarrow {\{m\}}\times 2^G\), and so each program is a fixed assignment to the signals in \(G\). Hence, TGEs that have full visibility and operate in an environment with no memory coincide with traditional transducers. Consider now a setting with partial visibility, thus \(V\ne I\). Now, programs are of the form \(p:{\{m\}}\times 2^{H}\rightarrow {\{m\}}\times 2^G\), allowing the TGE to guide the environment in a way that depends on signals in \(H\).

In this section we examine different aspects of the memory used by the environment. We discuss a trade-off between the size of the memory and the size of the TGE, and how the two depend on the partitions \(I=V\cup H\) and \(O=C\cup G\).

We first observe that in settings in which all output signals can be guided, the TGE can instruct the environment to simulate a transducer that realizes the specification. Also, in settings with full visibility, the advantage of guided environments is only computational, thus specifications do not become realizable, yet may be realizable by smaller systems. Formally, we have the following.

Note that Theorem 1 also implies that an optimal balance between controlled and guided signals in a setting with full visibility can achieve at most a quadratic saving in the combined states space of the TGE and its memory. This is similar to the quadratic saving in defining a regular language by the intersection of two automata. Indeed, handling of two independent specifications can be partitioned between the TGE and the environment. Formally, we have the following.

Unsurprisingly, larger memory of the environment enables TGEs to synthesize more specifications. Formally, we have the following.

We turn to consider how changes in the partition of the input and output signals may affect the required memory. In Theorem 4, proved in the full version, we show that increasing visibility or decreasing control, does not require more states or memory. On the other hand, in Theorem 5, we show that increasing control by the system may require the environment to use more memory. Thus, surprisingly, guiding more signals does not require more memory, yet guiding fewer signals may require more memory.

Recall that in the SGE problem, we are given an LTL specification \(\varphi \) over \(I \cup O\), partitions \(I=V\cup H\) and \(O=C\cup G\), and a bound \(k\ge 1\), and we have to return a TGE that \((V,H,C,G)\)-realizes \(\varphi \) with memory k. The main challenge in solving the SGE problem is that it adds to the difficulties of synthesis with partial visibility the fact that the system’s interactions with environments that agree on the visible signals may generate different computations. Technically, the system should still behave in the same way on input sequences that agree on the visible signals. Thus, the interaction should generate the same assignments to the controlled output signals and the same sequence of programs. However, these programs may generate different computations, as they also depend on the hidden signals.

Recall that TGEs generate in each transition a program \(p:M \times 2^H\rightarrow M \times 2^G\) that instructs the environment how to update its memory and assign values to the guided output signals. In this section we discuss ways to represent programs efficiently, and, in the context of synthesis, restrict the set of programs that a TGE may suggest to its environment without affecting the outcome of the synthesis procedure. Note that the number of programs in \(\mathcal {P}_{M,H,G}\) is \(2^{(\log |M|+|G|) \cdot |M| \cdot 2^{|H|}}\). Our main goal is to reduce the domain \(2^{H}\), which is the most dominant factor.

Naturally, the reduction depends on the specification we wish to synthesize. For an LTL formula \(\psi \), let \({ prop} (\psi )\) be the set of maximal predicates over \(I \cup O\) that are subformulas of \(\psi \). Formally, \({ prop} (\psi )\) is defined by an induction on the structure of \(\psi \) as follows.

Note that the definition is sensitive to syntax. For example, the formulas \((i_1 \vee o)\wedge \textbf{X}i_2\) and \((i_1 \wedge \textbf{X}i_2) \vee (o \wedge \textbf{X}i_2)\) are equivalent, but have different sets of maximal propositional assertions. Indeed, \({ prop} ((i_1 \vee o)\wedge \textbf{X}i_2)=\{i_1\vee o, i_2\}\), whereas \({ prop} ((i_1 \wedge \textbf{X}i_2) \vee (o \wedge \textbf{X}i_2))=\{i_1,i_2,o\}\).

It is well known that the satisfaction of an LTL formula \(\psi \) in a computation \(\pi \in (2^{I \cup O})^\omega \) depends only on the satisfaction of the formulas in \({ prop} (\psi )\) along \(\pi \): if two computations agree on \({ prop} (\psi )\), then they also agree on \(\psi \). Formally, for two assignments \(\sigma ,\sigma ' \in 2^{I \cup O}\), and a set \(\varTheta \) of predicates over \(I \cup O\), we say that \(\sigma \) and \(\sigma '\) agree on \(\varTheta \), denoted \(\sigma \approx _{\varTheta } \sigma '\), if for all \(\theta \in \varTheta \), we have that \(\sigma \models \theta \) iff \(\sigma ' \models \theta \). Then, two computations \(\pi =\sigma _1\cdot \sigma _2\cdots \) and \(\pi ' =\sigma '_1\cdot \sigma '_2\cdots \) in \((2^{I \cup O})^\omega \) agree on \(\varTheta \), denoted \(\pi \approx _{\varTheta } \pi '\), if for all \(j \ge 1\), we have \(\sigma _j \approx _{\varTheta } \sigma '_j\).

As we shall formalize below, Proposition 1 enables us to restrict the set of programs so that only one computation from each equivalence class of the relation \(\approx _{{ prop} (\psi )}\) may be generated by the interaction of the system and the environment.

For an LTL formula \(\psi \), let \({ cl}_{H}(\psi )\) be the set of maximal subformulas of formulas in \({ prop} (\psi )\) that are defined only over signals in \(H\). Formally, \({ cl}_{H}(\psi )=\bigcup _{\theta \in { prop} (\psi )}{ cl}_{H}(\theta )\), where \({ cl}_{H}(\theta )\) is defined for a propositional formula \(\theta \) as follows.

For example, if \(H=I=\{i_1,i_2,i_3\}\) and \(O=\{o\}\), then \({ cl}_{H}((i_1 \vee i_2)\wedge (i_3\vee o))=\{i_1 \vee i_2,i_3\}\). Note that formulas in \({ cl}_{H}(\psi )\) are over \(H\), and that the relation \(\approx _{{ cl}_{H}(\psi )}\) is an equivalence relation on \(2^H\). We say that a program \(p: M \times 2^H\rightarrow M \times 2^G\) is tight for \(\psi \) if for every memory \(m \in M\) and two assignments \(h,h' \in 2^{H}\), if \(h \approx _{{ cl}_{H}(\psi )} h'\), then \(p(m,h)=p(m,h')\).

In Theorem 10 below, proved in the full version, we argue that in the context of LTL synthesis, one can always restrict attention to tight programs.

Theorem 10 enables us to replace the domain \(M \times 2^H\) by the more restrictive domain \(M \times 2^{{ cl}_{H}(\varphi )}\). Below we discuss how to reduce the domain further, taking into account the configurations in which the programs are going to be executed.

Recall that whenever a TGE instructs the environment which program to follow, the signals in \(V\) and \(C\) already have an assignment. Indeed, \(\tau : S \times 2^V\rightarrow 2^C\times \mathcal {P}_{M,H,G}\), and when \(\langle c,p\rangle \in \delta (s,v)\), we know that the program p is going to be executed when the signals in V and C are assigned v and c. In the full version, we use the values of \(V\cup C\) in order to make the equivalence classes on \(2^H\) even coarser.

Consider a TGE \(\mathcal {T}\) with memory M that \((V,H,C,G)\)-realizes a specification. As shown in Figure 2 (left), the TGE’s operation can be viewed as two distributed processes executed together: the TGE \(\mathcal {T}\) itself, and a transducer \(\mathcal {T}_G\) with state space M, implementing \(\mathcal {T}\)’s instructions to the environment. In each round, the transducer \(\mathcal {T}_G\) receives from the environment an assignment to the signals in \(H\), received from \(\mathcal {T}\) a program, and uses both in order to generate an assignment to the signals in G and update its state.

We examine whether viewing TGEs this way can help reduce SGE to known algorithms for the synthesis of distributed systems. We argue that the approach here, where we do not view \(\mathcal {T}_G\) as a process in a distributed system, is preferable. In distributed-systems synthesis, we are given a specification \(\varphi \) and an architecture describing the communication channels among processes. The goal is to design strategies for these processes so that their joint behavior satisfies \(\varphi \). Synthesis of distributed systems is generally undecidable [24], primarily due to information forks – processes with incomparable information (e.g., when the environment sends assignments of disjoint sets of signals to two processes) [28]. The SGE setting corresponds to the architecture in Figure 2: Process \(P_1\) is the TGE \(\mathcal {T}\), which gets assignments to \(V\) and generates assignments to \(C\). Instead of designing \(P_1\) to generate instructions for the environment, the synthesis algorithm also returns \(P_2\), which instructs the environment on generating assignments to \(G\). The process \(P_2\) gets (in fact generates) assignments to both \(V\) and \(H\), eliminating information forks, making SGE solvable by solving distributed-system synthesis for this architecture. A solution in the TGE setting, that is composed of a TGE \(\mathcal {T}\) and an environment transducer \(\mathcal {T}_G\), induces a solution in the distributed setting: \(P_1\) follows \(\mathcal {T}\), and \(P_2\) simulates the joint operation of \(\mathcal {T}\) and \(\mathcal {T}_G\), assigning values to \(G\) as instructed by \(\mathcal {T}\). Conversely, a TGE can encode through \(\mathcal {P}_{M,H,G}\) the current assignment to V together with a description of the structure of \(P_2\), achieving the architecture in Figure 2 (right).

Using programs in \(\mathcal {P}_{M,H,G}\) goes beyond sending \(V\)’s values, which are already known to the environment. Programs leverage the TGE’s computation, particularly its current state, to save resources and utilize less memory. Not using the communication channel between the TGE and the environment could result in a significant increase in the size of process \(P_2\). For example, when \(|M|=1\) (specifications where \(G\)’s assignment depends only on \(V\)’s history and \(H\)’s current assignment), the process \(P_2\) is redundant. As demonstrated in Section 5, programs in \(\mathcal {P}_{M,H,G}\) can be described symbolically. Formally, we have the following.

Dynamic hiding and guidance. In the setting studied here, the partition of I and O into visible, hidden, controlled, and guided signals is fixed throughout the computation. In some settings, these partitions may be dynamic. For example, when visibility depends on sensors that the system may activate and deactivate [2] or when signals are sometimes hidden in order to maintain privacy [18]. The decision which signals to hide in each round may depend on the system (e.g., when it instructs the environment which signals to hide in order to maintain its privacy), the environment (e.g., when it prefers not to share sensitive information), or an external authority (e.g., when signals become hidden due to actual invisibility). As for output signals, their guidance may depend on the history of the interaction (e.g., we may be able to assume amenability from the environment only after some password has been entered).

Bounded SGE. SGE involves a memory that can be used by the environment. As in the study of traditional bounded synthesis [19, 29], it is interesting to study SGE with given bounds on both the state spaces of the system and the environment. In addition to better modeling the setting, the bounds are used in order to improve the complexity of the algorithm, and they can also serve in heuristics, as in SAT-based algorithms for bounded synthesis [11]. In the setting of SGE, it is interesting to investigate the tradeoffs among the three involved bounds. It is easy to see that the two bounds that are related to the environment, namely the bound on its state space and the bound on the memory supervised by the system, are dual: an increase in the memory supervised by the system makes more specifications realizable, whereas an increase in the size of the state space of the environment makes fewer specifications realizable.

Another parameter that is interesting to bound is the number of different programs that a TGE may use, or the class of possible programs. In particular, restricting SGE to programs in which guided output signals can be assigned only the values of hidden signals or values stored in registers, will simplify an implementation of the algorithm. Likewise, the update of the memory during the interaction may be global and fixed throughout the computation.