\SetWatermarkText
\SetWatermarkAngle0
11institutetext: Reactive Systems Group
Saarland University
11email: [email protected]
Synthesizing Reactive Systems from Hyperproperties††thanks: Supported by the European Research Council (ERC) Grant OSARES (No. 683300).
Bernd Finkbeiner
Christopher Hahn
Philip Lukert
Marvin Stenger
Leander Tentrup
Abstract
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 ∃∗, ∃∗∀1, and the
linear∀∗ 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.
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.
HyperLTL [4] is a logic for expressing
temporal hyperproperties, by extending linear-time temporal logic
(LTL) with explicit quantification over traces. 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 HyperLTL
formula
∀π∀π′.\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(Iπ=Iπ′)→\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(Oπ=Oπ′),
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 HyperLTL has been studied, the
reactive synthesis problem of 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.
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 Ca,Cb, and
Cc 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 [14, 7], 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
∃∗, ∃∗∀1, and the
linear∀∗ 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 ∀∗ fragment, which includes
observational determinism, is undecidable.
We answer the second question by studying the bounded version
of the synthesis problem for the ∀∗ fragment. In order to detect realizability, we ask
whether, for a universal HyperLTL formula φ 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 φ. 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.
1.0.1 Related Work.
HyperLTL [4] is a successor of the temporal logic 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 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 ω-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].
HyperLTL subsumes logics that reason over knowledge [4].
Information-flow in distributed systems is another example of hyperproperties, and the HyperLTL realizability problem subsumes both the distributed synthesis problem [21, 13] 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.
HyperLTL [4] is a temporal logic for specifying hyperproperties.
It extends LTL by quantification over trace variables π and a method to link atomic propositions to specific traces.
The set of trace variables is V.
Formulas in HyperLTL are given by the grammar
[TABLE]
where a∈AP and π∈V.
The alphabet of a HyperLTL formula is 2AP.
We allow the standard boolean connectives ∧, →, ↔ as well as the derived LTL operators release φ\mathltlRψ≡¬(¬φ\mathltlU¬ψ), eventually \leavevmodeto8.7pt\vboxto8.7pt\pgfpicture\makeatletter\lower-1.76527ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@lineto4.09026pt6.67358pt\pgfsys@lineto8.18053pt2.58333pt\pgfsys@lineto4.09026pt-1.50694pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureφ≡true\mathltlUφ, globally \leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureφ≡¬\leavevmodeto8.7pt\vboxto8.7pt\pgfpicture\makeatletter\lower-1.76527ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@lineto4.09026pt6.67358pt\pgfsys@lineto8.18053pt2.58333pt\pgfsys@lineto4.09026pt-1.50694pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture¬φ, and weak until φ\mathltlWψ≡\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureφ∨(φ\mathltlUψ).
The semantics is given by the satisfaction relation ⊨T over a set of traces T⊆(2AP)ω.
We define an assignment Π:V→(2AP)ω that maps trace variables to traces. Π[i,∞] is the trace assignment that is equal to Π(π)[i,∞] for all π and denotes the assignment where the first i items are removed from each trace.
\begin{array}[]{ll}\Pi\vDash_{T}a_{\pi}&\text{if }a\in\Pi(\pi)[0]\\
\Pi\vDash_{T}\neg\varphi&\text{if }\Pi\nvDash_{T}\varphi\\
\Pi\vDash_{T}\varphi\lor\psi&\text{if }\Pi\vDash_{T}\varphi\text{ or }\Pi\vDash_{T}\psi\\
\Pi\vDash_{T}\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ }
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi&\text{if }\Pi[1,\infty]\vDash_{T}\varphi\\
\Pi\vDash_{T}\varphi\mathbin{\mathltl{U}\kern-1.00006pt}\psi&\text{if }\exists i\geq 0\mathpunct{.}\Pi[i,\infty]\vDash_{T}\psi\land\forall 0\leq j<i\mathpunct{.}\Pi[j,\infty]\vDash_{T}\varphi\\
\Pi\vDash_{T}\exists\pi\mathpunct{.}\varphi&\text{if there is some }t\in T\text{ such that }\Pi[\pi\mapsto t]\vDash_{T}\varphi\\
\Pi\vDash_{T}\forall\pi\mathpunct{.}\varphi&\text{if for all }t\in T\text{ holds that }\Pi[\pi\mapsto t]\vDash_{T}\varphi\end{array}
We write T⊨φ for {}⊨Tφ where {} denotes the empty assignment.
Two HyperLTL formulas φ and ψ 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⊆AP and A⊆AP, we define independence as the following HyperLTL formula
[TABLE]
This guarantees that every proposition c∈C solely depends on propositions A.
Strategies.
A strategy f:(2I)∗→2O maps sequences of input valuations 2I to an output valuation 2O.
The behavior of a strategy f:(2I)∗→2O is characterized by an infinite tree that branches by the valuations of I and whose nodes w∈(2I)∗ are labeled with the strategic choice f(w).
For an infinite word w=w0w1w2⋯∈(2I)ω, the corresponding labeled path is defined as (f(ϵ)∪w0)(f(w0)∪w1)(f(w0w1)∪w2)⋯∈(2I∪O)ω.
We lift the set containment operator ∈ to the containment of a labeled path w=w0w1w2⋯∈(2I∪O)ω in a strategy tree induced by f:(2I)∗→2O, i.e., w∈f if, and only if, f(ϵ)=w0∩O and f((w0∩I)⋯(wi∩I))=wi+1∩O for all i≥0.
We define the satisfaction of a HyperLTL formula φ (over propositions I∪O) on strategy f, written f⊨φ, as {w∣w∈f}⊨φ.
Thus, a strategy f is a model of φ if the set of labeled paths of f is a model of φ.
3 HyperLTL Synthesis
In this section, we identify fragments of HyperLTL for which the realizability problem is decidable.
Our findings are summarized in Table 1.
Definition 1 (HyperLTL Realizability)
A HyperLTL formula φ over atomic propositions AP=I∪˙O is realizable if there is a strategy f:(2I)∗→2O that satisfies φ.
We base our investigation on the structure of the quantifier prefix of the HyperLTL formulas. We call a HyperLTL formula φ (quantifier) alternation-free if the quantifier prefix consists solely of either universal or existential quantifiers. We denote the corresponding fragments as the (universal) ∀∗ and the (existential) ∃∗ fragment, respectively.
A HyperLTL formula is in the ∃∗∀∗ fragment, if it starts with arbitrarily many existential quantifiers, followed by arbitrarily many universal quantifiers.
Respectively for the ∀∗∃∗ fragment.
For a given natural number n, we refer to a bounded number of quantifiers with ∀n, respectively ∃n.
The ∀1 realizability problem is equivalent to the LTL realizability problem.
3.0.1 ∃∗ Fragment.
We show that the realizability problem for existential HyperLTL is PSpace-complete.
We reduce the realizability problem to the satisfiability problem for bounded one-alternating ∃∗∀2HyperLTL [9], i.e., finding a trace set T such that T⊨φ.
Lemma 1
An existential HyperLTL formula φ is realizable if, and only if,
ψ:=φ∧DI↦O
is satisfiable.
Proof
Assume f:(2I)∗→2O realizes φ, that is f⊨φ.
Let T={w∣w∈f} be the set of traces generated by f.
It holds that T⊨φ and T⊨DI↦O.
Therefore, ψ is satisfiable.
Assume ψ is satisfiable.
Let S be a set of traces that satisfies ψ.
We construct a strategy f:(2I)∗→2O as
[TABLE]
Where w∣I denotes the trace restricted to I, formally wi∩I for all i≥0.
Note that if there are multiple candidates w∈S, then w∣σ∣∩O is the same for all of them because of the required non-determinism DI↦O.
By construction, all traces in S are contained in f and with S⊨φ it holds that f⊨φ as φ is an existential formula.
Theorem 3.1
Realizability of existential HyperLTL specifications is decidable.
Proof
The formula ψ from Lemma 1 is in the ∃∗∀2 fragment, for which satisfiability is decidable [9].
Corollary 1
Realizability of ∃∗HyperLTL specifications is PSpace-complete.
Proof
Given an existential HyperLTL formula, we gave a linear reduction to the satisfiability of the ∃∗∀2 fragment in Lemma 1.
The satisfiability problem for a bounded number of universal quantifiers is in PSpace [9].
Hardness follows from LTL satisfiability, which is equivalent to the ∃1 fragment.
3.0.2 ∀∗ 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 LTL formula.
Formally, a distributed architecture A is a tuple ⟨P,penv,I,O⟩ where
P is a finite set of processes with distinguished environment process penv∈P. The functions I:P→2AP and O:P→2AP 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=p′∈P it holds that O(p)∩O(p′)=∅.
W.l.o.g. we assume that I(penv)=∅.
The distributed synthesis problem for architectures without information forks [13] is decidable.
Example architectures are depicted in Fig. 1.
The architecture in Fig. 1(a) contains an information fork while the architecture in Fig. 1(b) does not.
Furthermore, the processes in Fig. 1(b) can be ordered linearly according to the subset relation on the inputs.
Theorem 3.2
The synthesis problem for universal HyperLTL is undecidable.
Proof
In the ∀∗ fragment (and thus in the ∃∗∀∗ fragment), we can encode a distributed architecture [13], for which LTL synthesis is undecidable. In particular, we can encode the architecture shown in Fig. 1(a). This architecture basically specifies c to depend only on a and analogously d on b. That can be encoded by D{a}↦{c} and D{b}↦{d}. The LTL synthesis problem for this architecture is already shown to be undecidable [13], i.e., given an LTL formula over I={a,b} and O={c,d}, we cannot automatically construct processes p1 and p2 that realize the formula.
3.0.3 Linear ∀∗ 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, ∀π1∀π2.\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureaπ1∨\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureaπ2 is transformed into an equivalent ∀1 formula ∀π.\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureaπ∨\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureaπ.
However, this transformation does not always produce equivalent formulas as ∀π1∀π2.\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(aπ1↔aπ2) is not equivalent to its collapsed form ∀π.\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(aπ↔aπ).
Let φ be ∀π1⋯∀πn.ψ.
We define the collapsed formula of φ as collapse(φ):=∀π.ψ[π1↦π][π2↦π]…[πn↦π] where ψ[πi↦π] replaces all occurrences of πi in ψ with π.
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 φ≡collapse(φ) or φ has no equivalent ∀1 formula.
Proof
Suppose there is some ψ∈∀1 with ψ≡φ.
We show that ψ≡collapse(φ).
Let T be an arbitrary set of traces.
Let T={{w}∣w∈T}.
Because ψ∈∀1, T⊨ψ is equivalent to ∀T′∈T.T′⊨ψ, which is by assumption equivalent to ∀T′∈T.T′⊨φ.
Now, φ 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 ∀T′∈T.T′⊨φ↔T′⊨collapse(φ) that is again equivalent to T⊨collapse(φ).
Because ψ≡collapse(φ) and ψ≡φ it holds that φ≡collapse(φ).
The 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 HyperLTL addresses exactly these architectures.
In the following, we sketch the characterization of the linear fragment of HyperLTL.
Given a formula φ, we seek for variable dependencies of the form DJ↦{o} with J⊆I and o∈O in the formula.
If the part of the formula φ that relates multiple paths consists only of such constraints DJ↦{o} with the rest being an LTL property, we can interpret φ as a description of a distributed architecture.
If furthermore, the DJi↦{oi} constraints can be ordered such that Ji⊆Ji+1 for all i, the architecture is linear.
There are three steps to check whether φ is in the linear fragment:
-
First, we have to add input-determinism to the formula φdet:=φ∧DI↦O.
This preserves realizability as strategies are input-deterministic.
2. 2.
Find for each output variable oi∈O possible sets of variables Ji, oi depends on, such that Ji⊆Ji+1.
To check whether the choice of J’s is correct, we test if collapse(φ)∧⋀oi∈ODJi↦{oi} is equivalent to φdet.
This equivalence check is decidable as both formulas are in the universal fragment [9].
3. 3.
Finally, we construct the corresponding distributed realizability problem with linear architecture.
Formally, we define the distributed architecture A=⟨P,penv,I,O⟩ with P={pi∣oi∈O}∪{penv}, I(pi)=Ji, O(pi)={oi}, and O(penv)=I. The LTL specification for the distributed synthesis problem is collapse(φ)
Definition 2 (linear fragment of ∀∗)
A formula φ is in the linear fragment of ∀∗ iff for all oi∈O there is a Ji⊆I such that φ∧DI↦O≡collapse(φ)∧⋀oi∈ODJi↦{oi} and Ji⊆Ji+1 for all i.
Note, that each ∀1 formula φ (or φ is collapsible to a ∀1 formula) is in the linear fragment because we can set all Ji=I and additionally collapse(φ)=φ holds.
As an example of a formula in the linear fragment of ∀∗, consider φ=∀π,π′.D{a}↦{c}∧\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(cπ↔dπ)∧\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(bπ↔\leavevmodeto7.41pt\vboxto7.41pt\pgfpicture\makeatletter\lower-1.11943ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@moveto3.44443pt2.58333pt\pgfsys@curveto3.44443pt4.48566pt1.90233pt6.02776pt0.0pt6.02776pt\pgfsys@curveto-1.90233pt6.02776pt-3.44443pt4.48566pt-3.44443pt2.58333pt\pgfsys@curveto-3.44443pt0.681pt-1.90233pt-0.8611pt0.0pt-0.8611pt\pgfsys@curveto1.90233pt-0.8611pt3.44443pt0.681pt3.44443pt2.58333pt\pgfsys@closepath\pgfsys@moveto0.0pt2.58333pt\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureeπ) with I={a,b} and O={c,d,e}.
The corresponding formula asserting input-deterministism is φdet=φ∧DI↦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}↦{d}∧(cπ↔dπ) implies D{a}↦{c}.
However, the apparent alternative {b} for e would yield an undecidable architecture.
It holds that φdet and collapse(φ)∧D{a,b}↦{c}∧D{a}↦{d}∧D{a,b}↦{e} are equivalent and, thus, that φ is in the linear fragment.
Theorem 3.3
The linear fragment of universal HyperLTL is decidable.
Proof
It holds that φ≡collapse(φ)∧⋀oi∈ODJi↦{oi} for some Ji’s.
The LTL distributed realizability problem for collapse(φ) in the constructed architecture A is equivalent to the HyperLTL realizability of φ as the architecture A represents exactly the input-determinism represented by formula ⋀oi∈ODJi↦{oi}.
The architecture is linear and, thus, the realizability problem is decidable.
3.0.4 ∃∗∀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 3.4
Realizability of ∃∗∀1HyperLTL specifications is decidable.
Proof
Let φ be ∃π1…∃πn∀π′.ψ.
We reduce the realizability problem of φ to the distributed realizability problem for LTL.
For every existential path quantifier πi, we introduce a copy of the atomic propositions, written aπi for a∈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 LTL constraint \leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(Iπi=Iπ′)→\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(Oπi=Oπ′) 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πi do not depend on the environment output.
The resulting architecture Aφ is ⟨{penv,p,p′},penv,{p↦∅,p′↦Iπ′},{penv↦Iπ′,p↦⋃1≤i≤nOπi∪Iπi,p′↦Oπ′}⟩.
It is easy to verify that Aφ does not contain an information fork, thus the realizability problem is decidable.
The LTL specification θ is ψ∧⋀1≤i≤n\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(Iπi=Iπ′)→\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(Oπi=Oπ′).
The implementation of process p′ (if it exists) is a model for the HyperLTL formula (process p producing witness for the ∃ quantifier).
Conversely, a model for φ can be used as an implementation of p′.
Thus, the distributed synthesis problem ⟨Aφ,θ⟩ has a solution if, and only if, φ is realizable.
3.0.5 ∀∗∃∗ Fragment.
The last fragment to consider are formulas in the ∀∗∃∗ fragment.
Whereas the ∃∗∀1 fragment remains decidable, the realizability problem of ∀∗∃∗ turns out to be undecidable even when restricted to only one quantifier of both sorts (∀1∃1).
Theorem 3.5
Realizability of ∀∗∃∗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
In this section, we propose an algorithm to synthesize strategies from specifications given in universal 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 S is a tuple ⟨S,s0,τ,l⟩ where
S is a finite set of states,
s0∈S is the designated initial state,
τ:S×2I→S is the transition function, and
l:S→2O is the state-labeling or output function.
We generalize the transition function to sequences over 2I by defining τ∗:(2I)∗→S recursively as τ∗(ϵ)=s0 and τ∗(w0⋯wn−1wn)=τ(τ∗(w0⋯wn−1),wn) for w0⋯wn−1wn∈(2I)+.
A transition system S generates the strategy f if f(w)=l(τ∗(w)) for every w∈(2I)∗.
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 φ be a universal HyperLTL formula ∀π1⋯∀πn.ψ.
We build the automaton Aψ whose language is the set of tuples of traces that satisfy ψ.
We then define the acceptance of a transition system S on Aψ by means of the self-composition of S.
Lastly, we encode the existence of a transition system accepted by Aψ 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 LTL specification
[TABLE]
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 result output is changed as well.
We formalize the property that no information about the decision can be inferred from result until publication as the HyperLTL formula
[TABLE]
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 A over a finite alphabet Σ is a tuple ⟨Q,q0,δ,F⟩, where
Q is a finite set of states,
q0∈Q is the designated initial state,
δ:Q×2Σ×Q is the transition relation, and
F⊆Q is the set of rejecting states.
Given an infinite word σ=σ0σ1σ2⋯∈(2Σ)ω, a run of σ on A is an infinite path q0q1q2⋯∈Qω where for all i≥0 it holds that (qi,σi,qi+1)∈δ.
A run is accepting, if it contains only finitely many rejecting states.
A accepts a word σ, if all runs of σ on A are accepting.
The language of A, written L(A), is the set {σ∈(2Σ)ω∣A accepts σ}.
We represent automata as directed graphs with vertex set Q and a symbolic representation of the transition relation δ as propositional boolean formulas B(Σ). The rejecting states in F are marked by double lines.
The automata for the LTL and HyperLTL specifications from Example 1 are depicted in Fig. 3.
Run graph.
The run graph of a transition system S=⟨S,s0,τ,l⟩ on a universal co-Büchi automaton A=⟨Q,q0,δ,F⟩ is a directed graph ⟨V,E⟩ where
V=S×Q is the set of vertices and
E⊆V×V is the edge relation with
[TABLE]
A run graph is accepting if every path (starting at the initial vertex (s0,q0)) 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 HyperLTL formulas [12] is based on self-composition.
Let prji 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 Sn is the n-fold self-composition of S=⟨S,s0,τ,l⟩, if Sn=⟨Sn,s0n,τ′,ln⟩ and for all s,s′∈Sn, α∈(2I)n, and β∈(2O)n we have that τ′(s,α)=s′ and ln(s)=β iff for all 1≤i≤n, it hold that τ(prji(s),prji(α))=prji(s′) and l(prji(s))=prji(β).
If T is the set of traces generated by S, then {zip(t1,…,tn)∣t1,…,tn∈T} is the set of traces generated by Sn.
We construct the universal co-Büchi automaton Aψ such that the language of Aψ is the set of words w such that unzip(w)=Π and Π⊨∅ψ, i.e., the tuple of traces that satisfy ψ.
We get this automaton by dualizing the non-deterministic Büchi automaton for ¬ψ [4], i.e., changing the branching from non-deterministic to universal and the acceptance condition from Büchi to co-Büchi.
Hence, S satisfies a universal HyperLTL formula φ=∀π1…∀πk.ψ if the traces generated by self-composition Sn are a subset of L(Aψ).
Lemma 3
A transition system S satisfies the universal HyperLTL formula φ=∀π1⋯∀πn.ψ, if the run graph of Sn and Aψ is accepting.
Synthesis.
Let S=⟨S,s0,τ,l⟩ and Aψ=⟨Q,q0,δ,F⟩.
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 τ:S×2I→S and the labeling function l:S→2O.
The annotation is split into two parts, a reachability constraint λB:Sn×Q→B indicating whether a state in the run graph is reachable and a counter λ#:Sn×Q→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.
[TABLE]
where ⊵ is > if q′∈F and ≥ otherwise.
Theorem 4.1
The constraint system is satisfiable with bound b if, and only if, there is a transition system S of size b that realizes the 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 HyperLTL formula is unrealizable.
We adapt the definition of counterexamples to realizability for LTL [15] to HyperLTL in the following.
Let φ be a universal HyperLTL formula ∀π1⋯∀πn.ψ over inputs I and outputs O, a counterexample to realizability is a set of input traces P⊆(2I)ω such that for every strategy f:(2I)∗→2O the labeled traces Pf⊆(2I∪O)ω satisfy ¬φ=∃π1⋯∃πn.¬ψ.
Proposition 1
A universal HyperLTL formula φ=∀π1⋯∀πn.ψ is unrealizable if there is a counterexample P to realizability.
Proof
For contradiction, we assume φ is realizable by a strategy f.
As P is a counterexample to realizability, we know Pf⊨∃π1⋯∃πn.¬ψ.
This means that there exists an assignment ΠP∈V→Pf with ΠP⊨Pf¬ψ.
Equivalently ΠP⊭Pfψ.
Therefore, not all assignments Π∈V→Pf satisfy Π⊨Pfψ.
Which implies Pf⊭∀π1⋯∀πn.ψ=φ.
Since φ is universal, we can defer f⊭φ, which concludes the contradiction.
Thus, φ is unrealizable.
Despite being independent of strategy trees, there are in many cases finite representations of P.
Consider, for example, the unrealizable specification φ1=∀π∀π′.\leavevmodeto8.7pt\vboxto8.7pt\pgfpicture\makeatletter\lower-1.76527ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@lineto4.09026pt6.67358pt\pgfsys@lineto8.18053pt2.58333pt\pgfsys@lineto4.09026pt-1.50694pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(iπ↔iπ′), where the set P1={∅ω,{i}ω} is a counterexample to realizability.
As a second example, consider φ2=∀π∀π′.\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(oπ↔oπ′)∧\leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(iπ↔\leavevmodeto7.41pt\vboxto7.41pt\pgfpicture\makeatletter\lower-1.11943ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@moveto3.44443pt2.58333pt\pgfsys@curveto3.44443pt4.48566pt1.90233pt6.02776pt0.0pt6.02776pt\pgfsys@curveto-1.90233pt6.02776pt-3.44443pt4.48566pt-3.44443pt2.58333pt\pgfsys@curveto-3.44443pt0.681pt-1.90233pt-0.8611pt0.0pt-0.8611pt\pgfsys@curveto1.90233pt-0.8611pt3.44443pt0.681pt3.44443pt2.58333pt\pgfsys@closepath\pgfsys@moveto0.0pt2.58333pt\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpictureoπ) with conflicting requirements on o.
P1 is a counterexample to realizability for φ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 ∀π.\leavevmodeto8.7pt\vboxto8.7pt\pgfpicture\makeatletter\lower-1.76527ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@lineto4.09026pt6.67358pt\pgfsys@lineto8.18053pt2.58333pt\pgfsys@lineto4.09026pt-1.50694pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(iπ↔oπ) 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 \leavevmodeto8.7pt\vboxto8.7pt\pgfpicture\makeatletter\lower-1.76527ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@lineto4.09026pt6.67358pt\pgfsys@lineto8.18053pt2.58333pt\pgfsys@lineto4.09026pt-1.50694pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(iπ↔oπ) 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 \leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(i↮o) for any system strategy.
We combine those two approaches, selecting counterexample paths and using strategic behavior.
A k-counterexample strategy for HyperLTL observes k output sequences and produces k inputs, where k is a new parameter (k≥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 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 Ok, k-tuple output propositions Ik, and the specification
[TABLE]
where ψ[P] denotes the replacement of aπi by the Pith position of the combined input/output k-tuple.
Theorem 5.1
A universal HyperLTL formula φ=∀π1⋯∀πn.ψ is unrealizable if there is a k-counterexample strategy for some k≥n.
6 Evaluation
We implemented a prototype synthesis tool, called BoSyHyper111BoSyHyper is available at https://www.react.uni-saarland.de/tools/bosy/, for universal HyperLTL based on the bounded synthesis algorithm described in Sec. 4.
Furthermore, we implemented the search for counterexamples proposed in Sec. 5.
Thus, BoSyHyper is able to characterize realizability and unrealizability of universal 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 HyperLTL formula.
Consequently, we build two constraint systems, one using the standard bounded synthesis approach [14] and one using the approach described in Sec. 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 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 HyperLTL for a simple mutual exclusion protocol.
Let r1 and r2 be input signals representing mutual exclusive requests to a critical section and g1/g2 the respective grant to enter the section.
Every request should be answered eventually \leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture(ri→\leavevmodeto8.7pt\vboxto8.7pt\pgfpicture\makeatletter\lower-1.76527ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt2.58333pt\pgfsys@lineto4.09026pt6.67358pt\pgfsys@lineto8.18053pt2.58333pt\pgfsys@lineto4.09026pt-1.50694pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicturegi) for i∈{1,2}, but not at the same time \leavevmodeto6.97pt\vboxto6.97pt\pgfpicture\makeatletter\lower-1.11945ptto0.0pt\pgfsys@beginscope\pgfsys@invoke \definecolorpgfstrokecolorrgb0,0,0\pgfsys@color@rgb@stroke000\pgfsys@invoke \pgfsys@color@rgb@fill000\pgfsys@invoke \pgfsys@setlinewidth0.4pt\pgfsys@invoke \nullfontto0.0pt\pgfsys@beginscope\pgfsys@invoke \pgfsys@beginscope\pgfsys@invoke \pgfsys@setlinewidth0.51666pt\pgfsys@invoke \pgfsys@roundjoin\pgfsys@invoke \pgfsys@moveto0.0pt-0.86111pt\pgfsys@lineto0.0pt5.5972pt\pgfsys@lineto6.45831pt5.5972pt\pgfsys@lineto6.45831pt-0.86111pt\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope \pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\pgfsys@discardpath\pgfsys@invoke\lxSVG@closescope\pgfsys@endscope\hss\lxSVG@closescope\endpgfpicture¬(g1∧g2).
The minimal LTL solution is depicted in Fig. 4(a).
It is well known that no mutex protocol can ensure perfect symmetry [19], thus when adding the symmetry constraint specified by the HyperLTL formula ∀π∀π′.(r1π↮r2π′)\mathltlR(g1π↔g2π′) the formula becomes unrealizable.
Our tool produces the counterexample shown in Fig. 4(b).
By adding another input signal tie that breaks the symmetry in case of simultaneous requests and modifying the symmetry constraint ∀π∀π′.((r1π↮r2π′)∨(tieπ↮¬tieπ′))\mathltlR(g1π↔g2π′) we obtain the solution depicted in Fig. 4(c).
We further evaluated the same properties on a version that forbids spurious grants, which are reported in Table 2 with prefix full.
Distributed and fault-tolerant systems.
In Sec. 3 we have shown how to encode arbitrary distributed architectures in HyperLTL.
As an example for our evaluation, consider a setting with two processes, one for encoding input signals and one for decoding the encoded signals.
Both processes can be synthesized simultaneously using a single 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 (sab,sac,sbc) are shared between pairs of cryptographers.
In the formalization, we have 4 entities: three processes describing the 3 cryptographers (outi) and one process computing the result (pg), i.e., whether the group has paid or not, from outi.
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 π and π′ where Ca has paid on π and Cb has paid on π′.
Then the outputs of both have to be the same, if their common secret sab is different on those two traces (while all other secrets sac and sbc 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 pg↔¬pNSA.
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.
7 Conclusion
In this paper, we have considered the reactive realizability problem for specifications given in the temporal logic 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 HyperLTL.
Furthermore, we presented two algorithms to detect realizable and unrealizable 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.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6