We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal logics like LTL, CTL, or CTL\(^*\). We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the \(\exists ^*\), \(\exists ^*\forall ^1\), and the \( linear \;\forall ^*\) fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL, we present a semi-decision procedure that constructs implementations and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy, and information-flow.
Notes
Supported by the European Research Council (ERC) Grant OSARES (No. 683300).
1 Introduction
Hyperproperties [5] generalize trace properties in that they not only check the correctness of individual computation traces in isolation, but relate multiple computation traces to each other. \(\text {HyperLTL}\) [4] is a logic for expressing temporal hyperproperties, by extending linear-time temporal logic (LTL) with explicit quantification over traces. \(\text {HyperLTL}\) has been used to specify a variety of information-flow and security properties. Examples include classical properties like non-interference and observational determinism, as well as quantitative information-flow properties, symmetries in hardware designs, and formally verified error correcting codes [12]. For example, observational determinism can be expressed as the \(\text {HyperLTL}\) formula stating that, for every pair of traces, if the observable inputs are the same, then the observable outputs must be same as well. While the satisfiability [9], model checking [4, 12], and runtime verification [1, 10] problem for \(\text {HyperLTL}\) has been studied, the reactive synthesis problem of \(\text {HyperLTL}\) is, so far, still open.
In reactive synthesis, we automatically construct an implementation that is guaranteed to satisfy a given specification. A fundamental difference to verification is that there is no human programmer involved: in verification, the programmer would first produce an implementation, which is then verified against the specification. In synthesis, the implementation is directly constructed from the specification. Because there is no programmer, it is crucial that the specification contains all desired properties of the implementation: the synthesized implementation is guaranteed to satisfy the given specification, but nothing is guaranteed beyond that. The added expressive power of HyperLTL over LTL is very attractive for synthesis: with synthesis from hyperproperties, we can guarantee that the implementation does not only accomplish the desired functionality, but is also free of information leaks, is symmetric, is fault-tolerant with respect to transmission errors, etc.
Advertisement
More formally, the reactive synthesis problem asks for a strategy, that is a tree branching on environment inputs whose nodes are labeled by the system output. Collecting the inputs and outputs along a branch of the tree, we obtain a trace. If the set of traces collected from the branches of the strategy tree satisfies the specification, we say that the strategy realizes the specification. The specification is realizable iff there exists a strategy tree that realizes the specification. With LTL specifications, we get trees where the trace on each individual branch satisfies the LTL formula. With HyperLTL, we additionally get trees where the traces between different branches are in a specified relationship. This is dramatically more powerful.
Consider, for example, the well-studied distributed version of the reactive synthesis problem, where the system is split into a set of processes, that each only see a subset of the inputs. The distributed synthesis problem for LTL can be expressed as the standard (non-distributed) synthesis problem for HyperLTL, by adding for each process the requirement that the process output is observationally deterministic in the process input. HyperLTL synthesis thus subsumes distributed synthesis. The information-flow requirements realized by HyperLTL synthesis can, however, be much more sophisticated than the observational determinism needed for distributed synthesis. Consider, for example, the dining cryptographers problem [3]: three cryptographers \(C_a,C_b,\) and \(C_c\) sit at a table in a restaurant having dinner and either one of cryptographers or, alternatively, the NSA must pay for their meal. Is there a protocol where each cryptographer can find out whether it was a cryptographer who paid or the NSA, but cannot find out which cryptographer paid the bill?
Synthesis from LTL formulas is known to be decidable in doubly exponential time. The fact that the distributed synthesis problem is undecidable [21] immediately eliminates the hope for a similar general result for HyperLTL. However, since LTL is obviously a fragment of HyperLTL, this immediately leads to the question whether the synthesis problem is still decidable for fragments of HyperLTL that are close to LTL but go beyond LTL: when exactly does the synthesis problem become undecidable? From a more practical point of view, the interesting question is whether semi-algorithms for distributed synthesis [7, 14], which have been successful in constructing distributed systems from LTL specifications despite the undecidability of the general problem, can be extended to HyperLTL?
In this paper, we answer the first question by studying the \(\exists ^*\), \(\exists ^*\forall ^1\), and the \( linear \;\forall ^*\) fragment. We show that the synthesis problem for all three fragments is decidable, and the problem becomes undecidable as soon as we go beyond these fragments. In particular, the synthesis problem for the full \(\forall ^*\) fragment, which includes observational determinism, is undecidable.
Advertisement
We answer the second question by studying the bounded version of the synthesis problem for the \(\forall ^*\) fragment. In order to detect realizability, we ask whether, for a universal HyperLTL formula \(\varphi \) and a given bound n on the number of states, there exists a representation of the strategy tree as a finite-state machine with no more than n states that satisfies \(\varphi \). To detect unrealizability, we check whether there exists a counterexample to realizability of bounded size. We show that both checks can be effectively reduced to SMT solving.
Related Work.\(\text {HyperLTL}\) [4] is a successor of the temporal logic \(\text {SecLTL}\) [6] used to characterize temporal information-flow. The model-checking [4, 12], satisfiability [9], monitoring problem [1, 10], and the first-order extension [17] of \(\text {HyperLTL}\) has been studied before. To the best of the authors knowledge, this is the first work that considers the synthesis problem for temporal hyperproperties. We base our algorithms on well-known synthesis algorithms such as bounded synthesis [14] that itself is an instance of Safraless synthesis [18] for \(\omega \)-regular languages. Further techniques that we adapt for hyperproperties are lazy synthesis [11] and the bounded unrealizability method [15, 16].
Hyperproperties [5] can be seen as a unifying framework for many different properties of interest in multiple distinct areas of research. Information-flow properties in security and privacy research are hyperproperties [4]. \(\text {HyperLTL}\) subsumes logics that reason over knowledge [4]. Information-flow in distributed systems is another example of hyperproperties, and the \(\text {HyperLTL}\) realizability problem subsumes both the distributed synthesis problem [13, 21] as well as synthesis of fault-tolerant systems [16]. In circuit verification, the semantic independence of circuit output signals on a certain set of inputs, enabling a range of potential optimizations, is a hyperproperty.
2 Preliminaries
HyperLTL.\(\text {HyperLTL}\) [4] is a temporal logic for specifying hyperproperties. It extends \(\text {LTL}\) by quantification over trace variables \(\pi \) and a method to link atomic propositions to specific traces. The set of trace variables is \(\mathcal {V}\). Formulas in \(\text {HyperLTL}\) are given by the grammar
where \(a \in \text {AP}\) and \(\pi \in \mathcal {V}\). The alphabet of a \(\text {HyperLTL}\) formula is \(2^ AP \). We allow the standard boolean connectives \(\wedge \), \(\rightarrow \), \(\leftrightarrow \) as well as the derived \(\text {LTL}\) operators release , eventually , globally , and weak until .
The semantics is given by the satisfaction relation \(\vDash _T\) over a set of traces \(T \subseteq (2^\text {AP})^\omega \). We define an assignment \(\varPi : \mathcal {V}\rightarrow (2^\text {AP})^\omega \) that maps trace variables to traces. \(\varPi [i,\infty ]\) is the trace assignment that is equal to \(\varPi (\pi )[i,\infty ]\) for all \(\pi \) and denotes the assignment where the first i items are removed from each trace.
We write \(T \vDash \varphi \) for \(\{\} \vDash _T \varphi \) where \(\{\}\) denotes the empty assignment. Two \(\text {HyperLTL}\) formulas \(\varphi \) and \(\psi \) are equivalent, written if they have the same models.
(In)dependence is a common hyperproperty for which we define the following syntactic sugar. Given two disjoint subsets of atomic propositions \(C \subseteq \text {AP}\) and \(A \subseteq \text {AP}\), we define independence as the following \(\text {HyperLTL}\) formula
(1)
This guarantees that every proposition \(c \in C\) solely depends on propositions A.
Strategies. A strategy\(f :(2^{I})^* \rightarrow 2^{O}\) maps sequences of input valuations \(2^{I}\) to an output valuation \(2^{O}\). The behavior of a strategy \(f:(2^{I})^* \rightarrow 2^{O}\) is characterized by an infinite tree that branches by the valuations of I and whose nodes \(w \in (2^{I})^*\) are labeled with the strategic choice f(w). For an infinite word \(w = w_0 w_1 w_2 \cdots \in (2^{I})^\omega \), the corresponding labeled path is defined as \((f(\epsilon ) \cup w_0)(f(w_0) \cup w_1)(f(w_0 w_1) \cup w_2)\cdots \in (2^{I \cup O})^\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^{I \cup O})^\omega \) in a strategy tree induced by \(f :(2^{I})^* \rightarrow 2^{O}\), i.e., \(w \in f\) if, and only if, \(f(\epsilon ) = w_0 \cap O\) and \(f((w_0 \cap I) \cdots (w_i \cap I)) = w_{i+1} \cap O\) for all \(i \ge 0\). We define the satisfaction of a \(\text {HyperLTL}\) formula \(\varphi \) (over propositions \(I \cup O\)) on strategy f, written \(f \vDash \varphi \), as \(\{w \mid w \in f\} \vDash \varphi \). Thus, a strategy f is a model of \(\varphi \) if the set of labeled paths of f is a model of \(\varphi \).
3 \(\text {HyperLTL}\) Synthesis
In this section, we identify fragments of \(\text {HyperLTL}\) for which the realizability problem is decidable. Our findings are summarized in Table 1.
Table 1.
Summary of decidability results.
\(\exists ^*\)
\(\exists ^* \forall ^1\)
\(\exists ^* \forall ^{>1}\)
\(\forall ^*\)
\(\forall ^* \exists ^*\)
\( linear \;\forall ^*\)
\(\textsc {PSpace}\)-complete
\(\textsc {3ExpTime}\)
undecidable
decidable
Definition 1
(HyperLTL Realizability). A \(\text {HyperLTL}\) formula \(\varphi \) over atomic propositions \(\text {AP}= I \mathbin {\dot{\cup }}O\) is realizable if there is a strategy \(f :(2^{I})^* \rightarrow 2^{O}\) that satisfies \(\varphi \).
We base our investigation on the structure of the quantifier prefix of the HyperLTL formulas. We call a HyperLTL formula \(\varphi \) (quantifier) alternation-free if the quantifier prefix consists solely of either universal or existential quantifiers. We denote the corresponding fragments as the (universal) \(\forall ^*\) and the (existential) \(\exists ^*\) fragment, respectively. A HyperLTL formula is in the \(\exists ^* \forall ^*\) fragment, if it starts with arbitrarily many existential quantifiers, followed by arbitrarily many universal quantifiers. Respectively for the \(\forall ^*\exists ^*\) fragment. For a given natural number n, we refer to a bounded number of quantifiers with \(\forall ^n\), respectively \(\exists ^n\). The \(\forall ^1\) realizability problem is equivalent to the \(\text {LTL}\) realizability problem.
\(\varvec{\exists ^*}\)Fragment. We show that the realizability problem for existential \(\text {HyperLTL}\) is \(\textsc {PSpace}\)-complete. We reduce the realizability problem to the satisfiability problem for bounded one-alternating \(\exists ^*\forall ^2 \text {HyperLTL}\) [9], i.e., finding a trace set T such that \(T \vDash \varphi \).
Lemma 1
An existential \(\text {HyperLTL}\) formula \(\varphi \) is realizable if, and only if, is satisfiable.
Proof
Assume \(f :(2^{I})^* \rightarrow 2^{O}\) realizes \(\varphi \), that is \(f \vDash \varphi \). Let \(T = \{w \mid w \in f\}\) be the set of traces generated by f. It holds that \(T \vDash \varphi \) and \(T \vDash D_{I \mapsto O}\). Therefore, \(\psi \) is satisfiable. Assume \(\psi \) is satisfiable. Let S be a set of traces that satisfies \(\psi \). We construct a strategy \(f :(2^{I})^* \rightarrow 2^{O}\) as
$$\begin{aligned} f(\sigma ) = {\left\{ \begin{array}{ll} w_{|\sigma |} \cap O &{} \text {if } \sigma \text { is a prefix of some } w|_I \text { with } w \in S \text {, and} \\ \emptyset &{} \text {otherwise} . \end{array}\right. } \end{aligned}$$
where \(w|_I\) denotes the trace restricted to I, formally \(w_i \cap I\) for all \(i \ge 0\). Note that if there are multiple candidates \(w \in S\), then \(w_{|\sigma |} \cap O\) is the same for all of them because of the required non-determinism \(D_{I \mapsto O}\). By construction, all traces in S are contained in f and with \(S \vDash \varphi \) it holds that \(f \vDash \varphi \) as \(\varphi \) is an existential formula.
Theorem 1
Realizability of existential \(\text {HyperLTL}\) specifications is decidable.
Proof
The formula \(\psi \) from Lemma 1 is in the \(\exists ^*\forall ^2\) fragment, for which satisfiability is decidable [9].
Corollary 1
Realizability of \(\exists ^* \text {HyperLTL}\) specifications is \(\textsc {PSpace}\)-complete.
Proof
Given an existential \(\text {HyperLTL}\) formula, we gave a linear reduction to the satisfiability of the \(\exists ^*\forall ^2\) fragment in Lemma 1. The satisfiability problem for a bounded number of universal quantifiers is in \(\textsc {PSpace}\) [9]. Hardness follows from \(\text {LTL}\) satisfiability, which is equivalent to the \(\exists ^1\) fragment.
\({\varvec{\forall }^*}\)Fragment. In the following, we will use the distributed synthesis problem, i.e., the problem whether there is an implementation of processes in a distributed architecture that satisfies an \(\text {LTL}\) formula. Formally, a distributed architecture \(A\) is a tuple \({\langle P, p_{env}, \mathcal {I}, \mathcal {O} \rangle }\) where P is a finite set of processes with distinguished environment process \(p_\textit{env} \in P\). The functions \(\mathcal {I} :P \rightarrow 2^{\text {AP}}\) and \(\mathcal {O} :P \rightarrow 2^{\text {AP}}\) define the inputs and outputs of processes. While processes may share the same inputs (in case of broadcasting), the outputs of processes must be pairwise disjoint, i.e., for all \(p \ne p' \in P\) it holds that \(\mathcal {O}(p) \cap \mathcal {O}(p') = \emptyset \). W.l.o.g. we assume that \(\mathcal {I}({p_\textit{env}}) = \emptyset \). The distributed synthesis problem for architectures without information forks [13] is decidable. Example architectures are depicted in Fig. 1. The architecture in Fig. 1a contains an information fork while the architecture in Fig. 1b does not. Furthermore, the processes in Fig. 1b can be ordered linearly according to the subset relation on the inputs.
Fig. 1.
Distributed architectures
×
Theorem 2
The synthesis problem for universal \(\text {HyperLTL}\) is undecidable.
Proof
In the \(\forall ^*\) fragment (and thus in the \(\exists ^*\forall ^*\) fragment), we can encode a distributed architecture [13], for which \(\text {LTL}\) synthesis is undecidable. In particular, we can encode the architecture shown in Fig. 1a. This architecture basically specifies c to depend only on a and analogously d on b. That can be encoded by \(D_{\{a\} \mapsto \{c\}}\) and \(D_{\{b\} \mapsto \{d\}}\). The \(\text {LTL}\) synthesis problem for this architecture is already shown to be undecidable [13], i.e., given an \(\text {LTL}\) formula over \(I=\{a,b\}\) and \(O=\{c,d\}\), we cannot automatically construct processes \(p_1\) and \(p_2\) that realize the formula.
Linear\({\varvec{\forall }^*}\)Fragment. For characterizing the linear fragment of HyperLTL, we will present a transformation from a formula with arbitrarily many universal quantifiers to a formula with only one quantifier. This transformation collapses the universal quantifier into a single one and renames the path variables accordingly. For example, is transformed into an equivalent \(\forall ^1\) formula . However, this transformation does not always produce equivalent formulas as is not equivalent to its collapsed form . Let \(\varphi \) be . We define the collapsed formula of where \(\psi [\pi _i \mapsto \pi ]\) replaces all occurrences of \(\pi _i\) in \(\psi \) with \(\pi \). Although the collapsed term is not always equivalent to the original formula, we can use it as an indicator whether it is possible at all to express a universal formula with only one quantifier as stated in the following lemma.
Lemma 2
Either or \(\varphi \) has no equivalent \(\forall ^1\) formula.
Proof
Suppose there is some \(\psi \in \forall ^1\) with . We show that . Let T be an arbitrary set of traces. Let \(\mathcal {T} = \{\{w\} \mid w \in T \}\). Because \(\psi \in \forall ^1\), \(T \vDash \psi \) is equivalent to , which is by assumption equivalent to . Now, \(\varphi \) operates on singleton trace sets only. This means that all quantified paths have to be the same, which yields that we can use the same path variable for all of them. So that is again equivalent to \(T \vDash collapse (\varphi )\). Because and it holds that .
The \(\text {LTL}\) realizability problem for distributed architectures without information forks [13] are decidable. These architectures are in some way linear, i.e., the processes can be ordered such that lower processes always have a subset of the information of upper processes. The linear fragment of universal \(\text {HyperLTL}\) addresses exactly these architectures.
In the following, we sketch the characterization of the linear fragment of \(\text {HyperLTL}\). Given a formula \(\varphi \), we seek for variable dependencies of the form \(D_{J \mapsto \{o\}}\) with \(J\subseteq I\) and \(o \in O\) in the formula. If the part of the formula \(\varphi \) that relates multiple paths consists only of such constraints \(D_{J \mapsto \{o\}}\) with the rest being an \(\text {LTL}\) property, we can interpret \(\varphi \) as a description of a distributed architecture. If furthermore, the \(D_{J_i \mapsto \{o_i\}}\) constraints can be ordered such that \(J_i\subseteq J_{i+1}\) for all i, the architecture is linear. There are three steps to check whether \(\varphi \) is in the linear fragment:
1.
First, we have to add input-determinism to the formula . This preserves realizability as strategies are input-deterministic.
2.
Find for each output variable \(o_i \in O\) possible sets of variables \(J_i\), \(o_i\) depends on, such that \(J_i\subseteq J_{i+1}\). To check whether the choice of J’s is correct, we test if \( collapse (\varphi ) \wedge \bigwedge _{o_i \in O} D_{J_i \mapsto \{o_i\}}\) is equivalent to \(\varphi _ det \). This equivalence check is decidable as both formulas are in the universal fragment [9].
3.
Finally, we construct the corresponding distributed realizability problem with linear architecture. Formally, we define the distributed architecture \(A= {\langle P, p_{env},\mathcal {I},\mathcal {O} \rangle }\) with \(P = \{p_i \mid o_i \in O\} \cup \{{p_\textit{env}}\}\), \(\mathcal {I}(p_i) = J_i\), \(\mathcal {O}(p_i) = \{o_i\}\), and \(\mathcal {O}({p_\textit{env}}) = I\). The \(\text {LTL}\) specification for the distributed synthesis problem is \( collapse (\varphi ).\)
Definition 2
(linear fragment of\(\forall ^\mathbf{*}\)). A formula \(\varphi \) is in the linear fragment of \(\forall ^*\) iff for all \(o_i \in O\) there is a \(J_i \subseteq I\) such that and \(J_i \subseteq J_{i+1}\) for all i.
Note, that each \(\forall ^1\) formula \(\varphi \) (or \(\varphi \) is collapsible to a \(\forall ^1\) formula) is in the linear fragment because we can set all \(J_i=I\) and additionally \( collapse (\varphi )=\varphi \) holds.
As an example of a formula in the linear fragment of \(\forall ^*\), consider with \(I=\{a,b\}\) and \(O=\{c,d,e\}\). The corresponding formula asserting input-deterministism is \(\varphi _{det}=\varphi \wedge D_{I \mapsto O}\). One possible choice of J’s is \(\{a,b\}\) for c, \(\{a\}\) for d and \(\{a,b\}\) for e. Note, that one can use either \(\{a,b\}\) or \(\{a\}\) for c as \(D_{\{a\} \mapsto \{d\}} \wedge (c_\pi \leftrightarrow d_\pi )\) implies \(D_{\{a\} \mapsto \{c\}}\). However, the apparent alternative \(\{b\}\) for e would yield an undecidable architecture. It holds that \(\varphi _{det}\) and \( collapse (\varphi ) \wedge D_{\{a,b\} \mapsto \{c\}} \wedge D_{\{a\} \mapsto \{d\}} \wedge D_{\{a,b\} \mapsto \{e\}}\) are equivalent and, thus, that \(\varphi \) is in the linear fragment.
Theorem 3
The linear fragment of universal \(\text {HyperLTL}\) is decidable.
Proof
It holds that for some \(J_i\)’s. The \(\text {LTL}\) distributed realizability problem for \( collapse (\varphi )\) in the constructed architecture A is equivalent to the \(\text {HyperLTL}\) realizability of \(\varphi \) as the architecture \(A\) represents exactly the input-determinism represented by formula \(\bigwedge _{o_i \in O} D_{J_i \mapsto \{o_i\}}\). The architecture is linear and, thus, the realizability problem is decidable.
\(\varvec{\exists ^* \forall ^1}\)Fragment. In this fragment, we consider arbitrary many existential path quantifier followed by a single universal path quantifier. This fragment turns out to be still decidable. We solve the realizability problem for this fragment by reducing it to a decidable fragment of the distributed realizability problem.
Theorem 4
Realizability of \(\exists ^* \forall ^1 \text {HyperLTL}\) specifications is decidable.
Proof
Let \(\varphi \) be . We reduce the realizability problem of \(\varphi \) to the distributed realizability problem for \(\text {LTL}\). For every existential path quantifier \(\pi _i\), we introduce a copy of the atomic propositions, written \(a_{\pi _i}\) for \(a \in \text {AP}\). Intuitively, those select the paths in the strategy tree where the existential path quantifiers are evaluated. Thus, those propositions (1) have to encode an actual path in the strategy tree and (2) may not depend on the branching of the strategy tree. To ensure (1), we add the \(\text {LTL}\) constraint that asserts that if the inputs correspond to some path in the strategy tree, the outputs on those paths have to be the same. Property (2) is guaranteed by the distributed architecture, the processes generating the propositions \(a_{\pi _i}\) do not depend on the environment output. The resulting architecture \(A_\varphi \) is \(\langle \{{p_\textit{env}},p,p'\},{p_\textit{env}},\{ p \mapsto \emptyset , p' \mapsto I_{\pi '} \}, \{ {p_\textit{env}}\mapsto I_{\pi '}, p \mapsto \bigcup _{1 \le i \le n} O_{\pi _i} \cup I_{\pi _i}, p' \mapsto O_{\pi '}\}\rangle \). It is easy to verify that \(A_\varphi \) does not contain an information fork, thus the realizability problem is decidable. The \(\text {LTL}\) specification \(\theta \) is . The implementation of process \(p'\) (if it exists) is a model for the \(\text {HyperLTL}\) formula (process p producing witness for the \(\exists \) quantifier). Conversely, a model for \(\varphi \) can be used as an implementation of \(p'\). Thus, the distributed synthesis problem \({\langle A_\varphi ,\theta \rangle }\) has a solution if, and only if, \(\varphi \) is realizable.
\(\varvec{\forall ^* \exists ^ *}\)Fragment. The last fragment to consider are formulas in the \(\forall ^*\exists ^*\) fragment. Whereas the \(\exists ^*\forall ^1\) fragment remains decidable, the realizability problem of \(\forall ^*\exists ^*\) turns out to be undecidable even when restricted to only one quantifier of both sorts (\(\forall ^1\exists ^1\)).
Theorem 5
Realizability of \(\forall ^* \exists ^*\)HyperLTL is undecidable.
Proof
The proof is done via reduction from Post’s Correspondence Problem (PCP) [22]. The basic idea follows the proof in [9].
4 Bounded Realizability
We propose an algorithm to synthesize strategies from specifications given in universal \(\text {HyperLTL}\) by searching for finite generators of realizing strategies. We encode this search as a satisfiability problem for a decidable constraint system.
Transition Systems. A transition system\(\mathcal {S}\) is a tuple \({\langle S,s_0,\tau ,l \rangle }\) where S is a finite set of states, \(s_0 \in S\) is the designated initial state, \(\tau :S \times 2^{I} \rightarrow S\) is the transition function, and \(l :S \rightarrow 2^{O}\) is the state-labeling or output function. We generalize the transition function to sequences over \(2^{I}\) by defining \(\tau ^* :(2^{I})^* \rightarrow S\) recursively as \(\tau ^*(\epsilon ) = s_0\) and \(\tau ^*(w_0 \cdots w_{n-1} w_n) = \tau (\tau ^*(w_0 \cdots w_{n-1}), w_n)\) for \(w_0 \cdots w_{n-1} w_n \in (2^{I})^+\). A transition system \(\mathcal {S}\)generates the strategy f if \(f(w) = l(\tau ^*(w))\) for every \(w \in (2^{I})^*\). A strategy f is called finite-state if there exists a transition system that generates f.
Overview. We first sketch the synthesis procedure and then proceed with a description of the intermediate steps. Let \(\varphi \) be a universal \(\text {HyperLTL}\) formula . We build the automaton \(\mathcal {A}_\psi \) whose language is the set of tuples of traces that satisfy \(\psi \). We then define the acceptance of a transition system \(\mathcal {S}\) on \(\mathcal {A}_\psi \) by means of the self-composition of \(\mathcal {S}\). Lastly, we encode the existence of a transition system accepted by \(\mathcal {A}_\psi \) as an SMT constraint system.
Example 1
Throughout this section, we will use the following (simplified) running example. Assume we want to synthesize a system that keeps decisions secret until it is allowed to publish. Thus, our system has three input signals decision, indicating whether a decision was made, the secret value, and a signal to publish results. Furthermore, our system has two outputs, a high output internal that stores the value of the last decision, and a low output result that indicates the result. No information about decisions should be inferred until publication. To specify the functionality, we propose the \(\text {LTL}\) specification
(2)
The solution produced by the LTL synthesis tool BoSy [8], shown in Fig. 2, clearly violates our intention that results should be secret until publish: Whenever a decision is made, the output result changes as well.
We formalize the property that no information about the decision can be inferred from result until publication as the \(\text {HyperLTL}\) formula
(3)
It asserts that for every pair of traces, the result signals have to be the same until (if ever) there is a publish signal on either trace. A solution satisfying both, the functional specification and the hyperproperty, is shown in Fig. 2. The system switches states whenever there is a decision with a different value than before and only exposes the decision in case there is a prior publish command.
We proceed with introducing the necessary preliminaries for our algorithm.
Automata. A universal co-Büchi automaton \(\mathcal {A}\) over a finite alphabet \(\varSigma \) is a tuple \({\langle Q,q_0,\delta ,F \rangle }\), where Q is a finite set of states, \(q_0 \in Q\) is the designated initial state, \(\delta :Q \times 2^\varSigma \times Q\) is the transition relation, and \(F \subseteq Q\) is the set of rejecting states. Given an infinite word \(\sigma = \sigma _0 \sigma _1 \sigma _2 \cdots \in (2^\varSigma )^\omega \), a run of \(\sigma \) on \(\mathcal {A}\) is an infinite path \(q_0 q_1 q_2 \dots \in Q^\omega \) where for all \(i \ge 0\) it holds that \((q_i,\sigma _i,q_{i+1}) \in \delta \). A run is accepting, if it contains only finitely many rejecting states. \(\mathcal {A}\) accepts a word \(\sigma \), if all runs of \(\sigma \) on \(\mathcal {A}\) are accepting. The language of \(\mathcal {A}\), written \(\mathcal {L}(\mathcal {A})\), is the set \(\{\sigma \in (2^\varSigma )^\omega \mid \mathcal {A}\text { accepts } \sigma \}\). We represent automata as directed graphs with vertex set Q and a symbolic representation of the transition relation \(\delta \) as propositional boolean formulas \(\mathbb {B}(\varSigma )\). The rejecting states in F are marked by double lines. The automata for the \(\text {LTL}\) and \(\text {HyperLTL}\) specifications from Example 1 are depicted in Fig. 3.
Fig. 3.
Universal co-Büchi automata recognizing the languages from Example 1.
×
Run Graph. The run graph of a transition system \(\mathcal {S}= {\langle S,s_0,\tau ,l \rangle }\) on a universal co-Büchi automaton \(\mathcal {A}= {\langle Q,q_0,\delta ,F \rangle }\) is a directed graph \({\langle V,E \rangle }\) where \(V = S \times Q\) is the set of vertices and \(E \subseteq V \times V\) is the edge relation with
A run graph is accepting if every path (starting at the initial vertex \((s_0,q_0)\)) has only finitely many visits of rejecting states. To show acceptance, we annotate every reachable node in the run graph with a natural number m, such that any path, starting in the initial state, contains less than m visits of rejecting states. Such an annotation exists if, and only if, the run graph is accepting [14].
Self-composition. The model checking of universal \(\text {HyperLTL}\) formulas [12] is based on self-composition. Let \( prj _i\) be the projection to the i-th element of a tuple. Let \( zip \) denote the usual function that maps a n-tuple of sequences to a single sequence of n-tuples, for example, \(zip([1, 2, 3], [4, 5, 6]) = [(1, 4), (2, 5), (3, 6)]\), and let \( unzip \) denote its inverse. The transition system \(\mathcal {S}^n\) is the n-fold self-composition of \(\mathcal {S}= {\langle S,s_0,\tau ,l \rangle }\), if \(\mathcal {S}^n = {\langle S^n, s_0^n, \tau ', l^n \rangle }\) and for all \(s, s' \in S^n\), \(\alpha \in (2^{I})^n\), and \(\beta \in (2^{O})^n\) we have that \(\tau '(s,\alpha ) = s'\) and \(l^n(s) = \beta \) iff for all \(1 \le i \le n\), it hold that \(\tau ( prj _i(s), prj _i(\alpha )) = prj _i(s')\) and \(l( prj _i(s)) = prj _i(\beta )\). If T is the set of traces generated by \(\mathcal {S}\), then \(\{ zip (t_1,\dots ,t_n) \mid t_1,\dots ,t_n \in T \}\) is the set of traces generated by \(\mathcal {S}^n\).
We construct the universal co-Büchi automaton \(\mathcal {A}_\psi \) such that the language of \(\mathcal {A}_\psi \) is the set of words w such that \( unzip (w) = \varPi \) and \(\varPi \vDash _\emptyset \psi \), i.e., the tuple of traces that satisfy \(\psi \). We get this automaton by dualizing the non-deterministic Büchi automaton for \(\lnot \psi \) [4], i.e., changing the branching from non-deterministic to universal and the acceptance condition from Büchi to co-Büchi. Hence, \(\mathcal {S}\) satisfies a universal \(\text {HyperLTL}\) formula if the traces generated by self-composition \(\mathcal {S}^n\) are a subset of \(\mathcal {L}(\mathcal {A}_\psi )\).
Lemma 3
A transition system \(\mathcal {S}\) satisfies the universal \(\text {HyperLTL}\) formula , if the run graph of \(\mathcal {S}^n\) and \(\mathcal {A}_\psi \) is accepting.
Synthesis. Let \(\mathcal {S}= {\langle S,s_0,\tau ,l \rangle }\) and \(\mathcal {A}_\psi = {\langle Q,q_0,\delta ,F \rangle }\). We encode the synthesis problem as an SMT constraint system. Therefore, we use uninterpreted function symbols to encode the transition system and the annotation. For the transition system, those functions are the transition function \(\tau : S \times 2^{I} \rightarrow S\) and the labeling function \(l: S \rightarrow 2^{O}\). The annotation is split into two parts, a reachability constraint \(\lambda ^\mathbb {B}: S^n \times Q \rightarrow \mathbb {B}\) indicating whether a state in the run graph is reachable and a counter \(\lambda ^\# : S^n \times Q \rightarrow \mathbb {N}\) that maps every reachable vertex to the maximal number of rejecting states visited by any path starting in the initial vertex. The resulting constraint asserts that there is a transition system with accepting run graph.
where \(\trianglerighteq \) is > if \(q' \in F\) and \(\ge \) otherwise.
Theorem 6
The constraint system is satisfiable with bound b if, and only if, there is a transition system \(\mathcal {S}\) of size b that realizes the \(\text {HyperLTL}\) formula.
We extract a realizing implementation by asking the satisfiability solver to generate a model for the uninterpreted functions that encode the transition system.
5 Bounded Unrealizability
So far, we focused on the positive case, providing an algorithm for finding small solutions, if they exist. In this section, we shift to the case of detecting if a universal \(\text {HyperLTL}\) formula is unrealizable. We adapt the definition of counterexamples to realizability for \(\text {LTL}\) [15] to \(\text {HyperLTL}\) in the following. Let \(\varphi \) be a universal \(\text {HyperLTL}\) formula over inputs I and outputs O, a counterexample to realizability is a set of input traces \(\mathcal {P}\subseteq (2^I)^\omega \) such that for every strategy \(f: (2^{I})^* \rightarrow 2^{O}\) the labeled traces \(\mathcal {P}^f \subseteq (2^{I \cup O})^\omega \) satisfy .
Proposition 1
A universal \(\text {HyperLTL}\) formula is unrealizable if there is a counterexample \(\mathcal {P}\) to realizability.
Proof
For contradiction, we assume \(\varphi \) is realizable by a strategy f. As \(\mathcal {P}\) is a counterexample to realizability, we know . This means that there exists an assignment \(\varPi _\mathcal {P}\in \mathcal {V}\rightarrow \mathcal {P}^f\) with \(\varPi _\mathcal {P}\vDash _{\mathcal {P}^f} \lnot \psi \). Equivalently \(\varPi _\mathcal {P}\nvDash _{\mathcal {P}^f} \psi \). Therefore, not all assignments \(\varPi \in \mathcal {V}\rightarrow \mathcal {P}^f\) satisfy \(\varPi \vDash _{\mathcal {P}^f} \psi \). Which implies . Since \(\varphi \) is universal, we can defer \(f \nvDash \varphi \), which concludes the contradiction. Thus, \(\varphi \) is unrealizable.
Despite being independent of strategy trees, there are in many cases finite representations of \(\mathcal {P}\). Consider, for example, the unrealizable specification , where the set \(\mathcal {P}_1 = \{ \emptyset ^\omega , \{i\}^\omega \}\) is a counterexample to realizability. As a second example, consider with conflicting requirements on o. \(\mathcal {P}_1\) is a counterexample to realizability for \(\varphi _2\) as well: By choosing a different valuation of i in the first step, the system is forced to either react with different valuations of o (violating first conjunct), or not correctly repeating the initial value of i (violating second conjunct).
There are, however, already linear specifications where the set of counterexample paths is not finite and depends on the strategy tree [16]. For example, the specification is unrealizable as the system cannot predict future values of the environment. There is no finite set of traces witnessing this: For every finite set of traces, there is a strategy tree such that holds on every such trace. On the other hand, there is a simple counterexample strategy, that is a strategy that observes output sequences and produces inputs. In this example, the counterexample strategy inverts the outputs given by the system, thus it is guaranteed that for any system strategy.
We combine those two approaches, selecting counterexample paths and using strategic behavior. A k-counterexample strategy for \(\text {HyperLTL}\) observes k output sequences and produces k inputs, where k is a new parameter (\(k \ge n\)). The counterexample strategy is winning if (1) either the traces given by the system player do not correspond to a strategy, or (2) the body of the \(\text {HyperLTL}\) is violated for any n subset of the k traces. Regarding property (1), consider the two traces where the system player produces different outputs initially. Clearly, those two traces cannot be generated by any system strategy since the initial state (root labeling) is fixed.
The search for a k-counterexample strategy can be reduced to LTL synthesis using k-tuple input propositions \(O^k\), k-tuple output propositions \(I^k\), and the specification
where \(\psi [P]\) denotes the replacement of \(a_{\pi _i}\) by the \(P_i\)th position of the combined input/output k-tuple.
Theorem 7
A universal \(\text {HyperLTL}\) formula is unrealizable if there is a k-counterexample strategy for some \(k \ge n\).
6 Evaluation
We implemented a prototype synthesis tool, called \(\text {BoSyHyper}\)1, for universal \(\text {HyperLTL}\) based on the bounded synthesis algorithm described in Sect. 4. Furthermore, we implemented the search for counterexamples proposed in Sect. 5. Thus, \(\text {BoSyHyper}\) is able to characterize realizability and unrealizability of universal \(\text {HyperLTL}\) formulas.
We base our implementation on the LTL synthesis tool BoSy [8]. For efficiency, we split the specifications into two parts, a part containing the linear (LTL) specification, and a part containing the hyperproperty given as \(\text {HyperLTL}\) formula. Consequently, we build two constraint systems, one using the standard bounded synthesis approach [14] and one using the approach described in Sect. 4. Before solving, those constraints are combined into a single SMT query. This results in a much more concise constraint system compared to the one where the complete specification is interpreted as a \(\text {HyperLTL}\) formula. For solving the SMT queries, we use the Z3 solver [20]. We continue by describing the benchmarks used in our experiments.
Symmetric Mutual Exclusion. Our first example demonstrates the ability to specify symmetry in \(\text {HyperLTL}\) for a simple mutual exclusion protocol. Let \(r_1\) and \(r_2\) be input signals representing mutual exclusive requests to a critical section and \(g_1\)/\(g_2\) the respective grant to enter the section. Every request should be answered eventually for \(i \in \{1,2\}\), but not at the same time . The minimal LTL solution is depicted in Fig. 4a. It is well known that no mutex protocol can ensure perfect symmetry [19], thus when adding the symmetry constraint specified by the \(\text {HyperLTL}\) formula the formula becomes unrealizable. Our tool produces the counterexample shown in Fig. 4b. By adding another input signal tie that breaks the symmetry in case of simultaneous requests and modifying the symmetry constraint we obtain the solution depicted in Fig. 4c. We further evaluated the same properties on a version that forbids spurious grants, which are reported in Table 2 with prefix full.
Fig. 4.
Synthesized solution of the mutual exclusion protocols.
×
Distributed and Fault-Tolerant Systems. In Sect. 3 we presented a reduction of arbitrary distributed architectures to \(\text {HyperLTL}\). As an example for our evaluation, consider a setting with two processes, one for encoding input signals and one for decoding. Both processes can be synthesized simultaneously using a single \(\text {HyperLTL}\) specification. The (linear) correctness condition states that the decoded signal is always equal to the inputs given to the encoder. Furthermore, the encoder and decoder should solely depend on the inputs and the encoded signal, respectively. Additionally, we can specify desired properties about the encoding like fault-tolerance [16] or Hamming distance of code words [12]. The results are reported in Table 2 where i-j-x means i input bits, j encoded bits, and x represents the property. The property is either tolerance against a single Byzantine signal failure or a guaranteed Hamming distance of code words.
CAP Theorem. The CAP Theorem due to Brewer [2] states that it is impossible to design a distributed system that provides Consistency, Availability, and Partition tolerance (CAP) simultaneously. This example has been considered before [16] to evaluate a technique that could automatically detect unrealizability. However, when we drop either Consistency, Availability, or Partition tolerance, the corresponding instances (AP, CP, and CA) become realizable, which the previous work was not able to prove. We show that our implementation can show both, unrealizability of CAP and realizability of AP, CP, and CA. In contrast to the previous encoding [16] we are not limited to acyclic architectures.
Long-term Information-flow. Previous work on model-checking hyperproperties [12] found that an implementation for the commonly used I2C bus protocol could remember input values ad infinitum. For example, it could not be verified that information given to the implementation eventually leaves it, i.e., is forgotten. This is especially unfortunate in high security contexts. We consider a simple bus protocol which is inspired by the widely used I2C protocol. Our example protocol has the inputs send for initiating a transmission, in for the value that should be transferred, and an acknowledgment bit indicating successful transmission. The bus master waits in an idle state until a send is received. Afterwards, it transmits a header sequence, followed by the value of in, waits for an acknowledgement and then indicates success or failure to the sender before returning to the idle state. We specify the property that the input has no influence on the data that is send, which is obviously violated (instance NI1). As a second property, we check that this information leak cannot happen arbitrary long (NI2) for which there is a realizing implementation.
Dining Cryptographers. Recap the dining cryptographers problem introduced earlier. This benchmark is interesting as it contains two types of hyperproperties. First, there is information-flow between the three cryptographers, where some secrets (\(s_{ab}, s_{ac}, s_{bc}\)) are shared between pairs of cryptographers. In the formalization, we have 4 entities: three processes describing the 3 cryptographers (\(\textit{out}_i\)) and one process computing the result (\(p_g\)), i.e., whether the group has paid or not, from \(\textit{out}_i\). Second, the final result should only disclose whether one of the cryptographers has paid or the NSA. This can be formalized as a indistinguishability property between different executions. For example, when we compare the two traces \(\pi \) and \(\pi '\) where \(C_a\) has paid on \(\pi \) and \(C_b\) has paid on \(\pi '\). Then the outputs of both have to be the same, if their common secret \(s_{ab}\) is different on those two traces (while all other secrets \(s_{ac}\) and \(s_{bc}\) are the same). This ensures that from an outside observer, a flipped output can be either result of a different shared secret or due to the announcement. Lastly, the linear specification asserts that \(p_g \leftrightarrow \lnot p_\textit{NSA}\).
Results. Table 2 reports on the results of the benchmarks. We distinguish between state-labeled (Moore) and transition-labeled (Mealy) transition systems. Note that the counterexample strategies use the opposite transition system, i.e., a Mealy system strategy corresponds to a state-labeled (Moore) environment strategy. Typically, Mealy strategies are more compact, i.e., need smaller transition systems and this is confirmed by our experiments. BoSyHyper is able to solve most of the examples, providing realizing implementations or counterexamples. Regrading the unrealizable benchmarks we observe that usually two simultaneously generated paths (\(k=2\)) are enough with the exception of the encoder example. Overall the results are encouraging showing that we can solve a variety of instances with non-trivial information-flow.
Table 2.
Results of BoSyHyper on the benchmarks sets described in Sect. 6. They ran on a machine with a dual-core Core i7, 3.3 GHz, and 16 GB memory.
Benchmark
Instance
Result
States
Time[sec.]
Moore
Mealy
Moore
Mealy
Symmetric Mutex
non-sym
realizable
2
2
1.4
1.3
sym
unrealizable (\(k=2\))
1
1
1.9
2.0
tie
realizable
3
3
1.7
1.6
full-non-sym
realizable
4
4
1.4
1.4
full-sym
unrealizable (\(k=2\))
1
1
4.3
6.2
full-tie
realizable
9
5
1 802.7
5.2
Encoder/Decoder
1-2-hamming-2
realizable
4
1
1.6
1.3
1-2-fault-tolerant
unrealizable (\(k=2\))
1
-
54.9
-
1-3-fault-tolerant
realizable
4
1
151.7
1.7
2-2-hamming-2
unrealizable \((k=3)\)
-
1
-
10.6
2-3-hamming-2
realizable
16
1
>1 h
1.5
2-3-hamming-3
unrealizable \((k=3)\)
-
1
-
126.7
CAP Theorem
cap-2-linear
realizable
8
1
7.0
1.3
cap-2
unrealizable \((k=2)\)
1
-
1 823.9
-
ca-2
realizable
-
1
-
4.4
ca-3
realizable
-
1
-
15.0
cp-2
realizable
1
1
1.8
1.6
cp-3
realizable
1
1
3.2
10.6
ap-2
realizable
-
1
-
2.0
ap-3
realizable
-
1
-
43.4
Bus Protocol
NI1
unrealizable \((k=2)\)
1
1
75.2
69.6
NI2
realizable
8
8
24.1
33.9
Dining Cryptographers
secrecy
realizable
-
1
-
82.4
7 Conclusion
In this paper, we have considered the reactive realizability problem for specifications given in the temporal logic \(\text {HyperLTL}\). We gave a complete characterization of the decidable fragments based on the quantifier prefix and, additionally, identified a decidable fragment in the, in general undecidable, universal fragment of \(\text {HyperLTL}\). Furthermore, we presented two algorithms to detect realizable and unrealizable \(\text {HyperLTL}\) specifications, one based on bounding the system implementation and one based on bounding the number of counterexample paths. Our prototype implementation shows that our approach is able to synthesize systems with complex information-flow properties.
<SimplePara><Emphasis Type="Bold">Open Access</Emphasis>This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License(http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.</SimplePara><SimplePara>The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.</SimplePara>
stating that, for every pair of traces, if the observable inputs are the same, then the observable outputs must be same as well. While the satisfiability [9], model checking [4, 12], and runtime verification [1, 10] problem for \(\text {HyperLTL}\) has been studied, the reactive synthesis problem of \(\text {HyperLTL}\) is, so far, still open.
where \(a \in \text {AP}\) and \(\pi \in \mathcal {V}\). The alphabet of a \(\text {HyperLTL}\) formula is \(2^ AP \). We allow the standard boolean connectives \(\wedge \), \(\rightarrow \), \(\leftrightarrow \) as well as the derived \(\text {LTL}\) operators release
, eventually
, globally
, and weak until
.
if they have the same models.
This guarantees that every proposition \(c \in C\) solely depends on propositions A.
is satisfiable.
is transformed into an equivalent \(\forall ^1\) formula
. However, this transformation does not always produce equivalent formulas as
is not equivalent to its collapsed form
. Let \(\varphi \) be
. We define the collapsed formula of
where \(\psi [\pi _i \mapsto \pi ]\) replaces all occurrences of \(\pi _i\) in \(\psi \) with \(\pi \). Although the collapsed term is not always equivalent to the original formula, we can use it as an indicator whether it is possible at all to express a universal formula with only one quantifier as stated in the following lemma.
or \(\varphi \) has no equivalent \(\forall ^1\) formula.
. We show that
. Let T be an arbitrary set of traces. Let \(\mathcal {T} = \{\{w\} \mid w \in T \}\). Because \(\psi \in \forall ^1\), \(T \vDash \psi \) is equivalent to
, which is by assumption equivalent to
. Now, \(\varphi \) operates on singleton trace sets only. This means that all quantified paths have to be the same, which yields that we can use the same path variable for all of them. So
that is again equivalent to \(T \vDash collapse (\varphi )\). Because
and
it holds that
.
. This preserves realizability as strategies are input-deterministic.
and \(J_i \subseteq J_{i+1}\) for all i.
with \(I=\{a,b\}\) and \(O=\{c,d,e\}\). The corresponding formula asserting input-deterministism is \(\varphi _{det}=\varphi \wedge D_{I \mapsto O}\). One possible choice of J’s is \(\{a,b\}\) for c, \(\{a\}\) for d and \(\{a,b\}\) for e. Note, that one can use either \(\{a,b\}\) or \(\{a\}\) for c as \(D_{\{a\} \mapsto \{d\}} \wedge (c_\pi \leftrightarrow d_\pi )\) implies \(D_{\{a\} \mapsto \{c\}}\). However, the apparent alternative \(\{b\}\) for e would yield an undecidable architecture. It holds that \(\varphi _{det}\) and \( collapse (\varphi ) \wedge D_{\{a,b\} \mapsto \{c\}} \wedge D_{\{a\} \mapsto \{d\}} \wedge D_{\{a,b\} \mapsto \{e\}}\) are equivalent and, thus, that \(\varphi \) is in the linear fragment.
for some \(J_i\)’s. The \(\text {LTL}\) distributed realizability problem for \( collapse (\varphi )\) in the constructed architecture A is equivalent to the \(\text {HyperLTL}\) realizability of \(\varphi \) as the architecture \(A\) represents exactly the input-determinism represented by formula \(\bigwedge _{o_i \in O} D_{J_i \mapsto \{o_i\}}\). The architecture is linear and, thus, the realizability problem is decidable.
. We reduce the realizability problem of \(\varphi \) to the distributed realizability problem for \(\text {LTL}\). For every existential path quantifier \(\pi _i\), we introduce a copy of the atomic propositions, written \(a_{\pi _i}\) for \(a \in \text {AP}\). Intuitively, those select the paths in the strategy tree where the existential path quantifiers are evaluated. Thus, those propositions (1) have to encode an actual path in the strategy tree and (2) may not depend on the branching of the strategy tree. To ensure (1), we add the \(\text {LTL}\) constraint
that asserts that if the inputs correspond to some path in the strategy tree, the outputs on those paths have to be the same. Property (2) is guaranteed by the distributed architecture, the processes generating the propositions \(a_{\pi _i}\) do not depend on the environment output. The resulting architecture \(A_\varphi \) is \(\langle \{{p_\textit{env}},p,p'\},{p_\textit{env}},\{ p \mapsto \emptyset , p' \mapsto I_{\pi '} \}, \{ {p_\textit{env}}\mapsto I_{\pi '}, p \mapsto \bigcup _{1 \le i \le n} O_{\pi _i} \cup I_{\pi _i}, p' \mapsto O_{\pi '}\}\rangle \). It is easy to verify that \(A_\varphi \) does not contain an information fork, thus the realizability problem is decidable. The \(\text {LTL}\) specification \(\theta \) is
. The implementation of process \(p'\) (if it exists) is a model for the \(\text {HyperLTL}\) formula (process p producing witness for the \(\exists \) quantifier). Conversely, a model for \(\varphi \) can be used as an implementation of \(p'\). Thus, the distributed synthesis problem \({\langle A_\varphi ,\theta \rangle }\) has a solution if, and only if, \(\varphi \) is realizable.
. We build the automaton \(\mathcal {A}_\psi \) whose language is the set of tuples of traces that satisfy \(\psi \). We then define the acceptance of a transition system \(\mathcal {S}\) on \(\mathcal {A}_\psi \) by means of the self-composition of \(\mathcal {S}\). Lastly, we encode the existence of a transition system accepted by \(\mathcal {A}_\psi \) as an SMT constraint system.
The solution produced by the LTL synthesis tool BoSy [8], shown in Fig. 2, clearly violates our intention that results should be secret until publish: Whenever a decision is made, the output result changes as well.
It asserts that for every pair of traces, the result signals have to be the same until (if ever) there is a publish signal on either trace. A solution satisfying both, the functional specification and the hyperproperty, is shown in Fig. 2. The system switches states whenever there is a decision with a different value than before and only exposes the decision in case there is a prior publish command.
A run graph is accepting if every path (starting at the initial vertex \((s_0,q_0)\)) has only finitely many visits of rejecting states. To show acceptance, we annotate every reachable node in the run graph with a natural number m, such that any path, starting in the initial state, contains less than m visits of rejecting states. Such an annotation exists if, and only if, the run graph is accepting [14].
if the traces generated by self-composition \(\mathcal {S}^n\) are a subset of \(\mathcal {L}(\mathcal {A}_\psi )\).
, if the run graph of \(\mathcal {S}^n\) and \(\mathcal {A}_\psi \) is accepting.
where \(\trianglerighteq \) is > if \(q' \in F\) and \(\ge \) otherwise.
over inputs I and outputs O, a counterexample to realizability is a set of input traces \(\mathcal {P}\subseteq (2^I)^\omega \) such that for every strategy \(f: (2^{I})^* \rightarrow 2^{O}\) the labeled traces \(\mathcal {P}^f \subseteq (2^{I \cup O})^\omega \) satisfy
.
is unrealizable if there is a counterexample \(\mathcal {P}\) to realizability.
. This means that there exists an assignment \(\varPi _\mathcal {P}\in \mathcal {V}\rightarrow \mathcal {P}^f\) with \(\varPi _\mathcal {P}\vDash _{\mathcal {P}^f} \lnot \psi \). Equivalently \(\varPi _\mathcal {P}\nvDash _{\mathcal {P}^f} \psi \). Therefore, not all assignments \(\varPi \in \mathcal {V}\rightarrow \mathcal {P}^f\) satisfy \(\varPi \vDash _{\mathcal {P}^f} \psi \). Which implies
. Since \(\varphi \) is universal, we can defer \(f \nvDash \varphi \), which concludes the contradiction. Thus, \(\varphi \) is unrealizable.
, where the set \(\mathcal {P}_1 = \{ \emptyset ^\omega , \{i\}^\omega \}\) is a counterexample to realizability. As a second example, consider
with conflicting requirements on o. \(\mathcal {P}_1\) is a counterexample to realizability for \(\varphi _2\) as well: By choosing a different valuation of i in the first step, the system is forced to either react with different valuations of o (violating first conjunct), or not correctly repeating the initial value of i (violating second conjunct).
is unrealizable as the system cannot predict future values of the environment. There is no finite set of traces witnessing this: For every finite set of traces, there is a strategy tree such that
holds on every such trace. On the other hand, there is a simple counterexample strategy, that is a strategy that observes output sequences and produces inputs. In this example, the counterexample strategy inverts the outputs given by the system, thus it is guaranteed that
for any system strategy.
is unrealizable if there is a k-counterexample strategy for some \(k \ge n\).
for \(i \in \{1,2\}\), but not at the same time
. The minimal LTL solution is depicted in Fig. 4a. It is well known that no mutex protocol can ensure perfect symmetry [19], thus when adding the symmetry constraint specified by the \(\text {HyperLTL}\) formula
the formula becomes unrealizable. Our tool produces the counterexample shown in Fig. 4b. By adding another input signal tie that breaks the symmetry in case of simultaneous requests and modifying the symmetry constraint
we obtain the solution depicted in Fig. 4c. We further evaluated the same properties on a version that forbids spurious grants, which are reported in Table 2 with prefix full.