key: cord-0047717-rfh7qlu4
authors: Finkbeiner, Bernd; Hahn, Christopher; Hofmann, Jana; Tentrup, Leander
title: Realizing [Formula: see text]-regular Hyperproperties
date: 2020-06-16
journal: Computer Aided Verification
DOI: 10.1007/978-3-030-53291-8_4
sha: a4855c3296fb54a405f7f3a6c7cacee8a67de228
doc_id: 47717
cord_uid: rfh7qlu4

We study the expressiveness and reactive synthesis problem of HyperQPTL, a logic that specifies [Formula: see text]-regular hyperproperties. HyperQPTL is an extension of linear-time temporal logic (LTL) with explicit trace and propositional quantification and therefore truly combines trace relations and [Formula: see text]-regularity. As such, HyperQPTL can express promptness, which states that there is a common bound on the number of steps up to which an event must have happened. We demonstrate how the HyperQPTL formulation of promptness differs from the type of promptness expressible in the logic Prompt-LTL. Furthermore, we study the realizability problem of HyperQPTL by identifying decidable fragments, where one decidable fragment contains formulas for promptness. We show that, in contrast to the satisfiability problem of HyperQPTL, propositional quantification has an immediate impact on the decidability of the realizability problem. We present a reduction to the realizability problem of HyperLTL, which immediately yields a bounded synthesis procedure. We implemented the synthesis procedure for HyperQPTL in the bounded synthesis tool BoSy. Our experimental results show that a range of arbiter satisfying promptness can be synthesized.

Hyperproperties [5] , which are mainly studied in the area of secure information flow control, are a generalization from trace properties to sets of trace properties. That is, they relate multiple execution traces with each other. Examples are noninterference [20] , observational determinism [34] , symmetry [16] , or promptness [24] , i.e., properties whose satisfaction cannot be determined by analyzing each execution trace in isolation.

A number of logics have been introduced to express hyperproperties (examples are [4, 19, 25] ). They either add explicit trace quantification to a temporal logic or build on monadic first-order or second-order logics and add an equallevel predicate, which connects traces with each other. A comprehensive study comparing such hyperlogics has been initiated in [6] .

The most prominent hyperlogic is HyperLTL [4] , which extends classic linear-time temporal logic (LTL) [26] with trace variables and explicit trace quantification. HyperLTL has been successfully applied in (runtime) verification, (e.g., [15, 21, 32] ), specification analysis [11, 14] , synthesis [12, 13] , and program repair [1] of hyperproperties. As an example specification, the following HyperLTL formula expresses observational determinism by stating that for every pair of traces, if the observable inputs I are the same on both traces, then also the observable outputs O have to agree

Thus, hyperlogics can not only specify functional correctness, but may also enforce the absence of information leaks or presence of information propagation. There is a great practical interest in information flow control, which makes synthesizing implementations that satisfy hyperproperties highly desirable. Recently [12] , it was shown that the synthesis problem of HyperLTL, although undecidable in general, remains decidable for many fragments, such as the ∃ * ∀ fragment. Furthermore, a bounded synthesis procedure was developed, for which a prototype implementation based on BoSy [7, 9, 12] showed promising results. HyperLTL is, however, intrinsically limited in expressiveness. For example, promptness is not expressible in HyperLTL. Promptness is a property stating that there is a bound b, common for all traces, on the number of steps up to which an event e must have happened. Additionally, just like LTL, HyperLTL can express neither ω-regular nor epistemic properties [2, 29] . Epistemic properties are statements about the transfer of knowledge between several components. An exemplary epistemic specification is described by the dining cryptographers problem [3] : three cryptographers sit at a table in a restaurant. Either one of the cryptographers or, alternatively, the NSA must pay for their meal. The question is whether there is a protocol where each cryptographer can find out whether the NSA or one of the cryptographers paid the bill, without revealing the identity of the paying cryptographer.

In this paper, we explore HyperQPTL [6, 29] , a hyperlogic that is more expressive than HyperLTL. Specifically, we study its expressiveness and reactive synthesis problem. HyperQPTL extends HyperLTL with quantification over sequences of new propositions. What makes the logic particularly expressive is the fact that the trace quantifiers and propositional quantifiers can be freely interleaved. With this mechanism, HyperQPTL can not only express all ωregular properties over a sequences of n-tuples; it truly interweaves trace quantification and ω-regularity. For example, promptness can be stated as the following HyperQPTL formula:

The formula states that there exists a sequence s ∈ (2 {q} ) ω , such that event e holds on all traces before the first occurrence of b in s. In this paper, we argue that the type of promptness expressible in HyperQPTL is incomparable to the expressiveness of Prompt-LTL [24] , a logic introduced to express promptness properties. It is further known that HyperQPTL also subsumes epistemic extensions of temporal logics such as LTL K [22] , as well as the first-order hyperlogic FO[<, E] [6, 19, 29] . Its expressiveness makes HyperQPTL particularly interesting. The model checking problem of HyperQPTL is, despite the logic being quite expressive, decidable [29] . We also explore an alternative definition of HyperQPTL that would result in an even more expressive logic. However, we show that the logic would have an undecidable model checking problem, which constitutes a major drawback in the context of computer-aided verification. Furthermore, satisfiability is decidable for large fragments of the logic [6] . Decidable HyperQPTL fragments can be described solely in terms of their trace quantifier prefix. This indicates that propositional quantification has no negative impact on the decidability, although it greatly increases the expressiveness. We establish that propositional quantification, in contrast to the satisfiability problem, has an impact on the realizability problem: it becomes undecidable when combining a propositional ∀∃ quantifier alternation with a single universal trace quantifier. However, we show that the synthesis problem of large HyperQPTL fragments remains decidable, where one of these fragments contains promptness properties. We partially obtain these results by reducing the HyperQPTL realizability problem to the HyperLTL realizability problem. Based on this reduction, we extended the BoSy bounded synthesis tool to also synthesize systems respecting HyperQPTL specifications. We provide promising experimental results of our prototype implementation: using BoSy and HyperQPTL specifications, we were able to synthesize arbiters that respect promptness. This paper is structured as follows. In Sect. 2, we give necessary preliminaries. In Sect. 3, we define HyperQPTL. We discuss an alternative approach to define a logic expressing ω-regular hyperproperties, before pointing out that its model checking problem is undecidable. Subsequently, we give examples for the expressiveness of HyperQPTL, namely by characterizing the type of promptness properties HyperQPTL can express. Additionally, we recapitulate how HyperQPTL also subsumes epistemic properties. Section 4 discusses the realizability problem of HyperQPTL. We describe HyperQPTL fragments in terms of their quantifier prefixes. To present our results, we use the following notation. We write ∀ π and ∀ q for a single universal trace and propositional quantifier, respectively. To denote a sequence of universal trace and propositional quantifiers, we write ∀ * π and ∀ * q . Furthermore, we use ∀ * π/q for a sequence of mixed universal quantification. We use the analogous notation for existential quantifiers. Lastly, Q * π and Q * q denote a sequence of mixed universal and existential trace and propositional quantifiers, respectively. As an example, the ∀ * π Q * q fragment denotes all formulas of the form ∀π 1 . . . . ∀π m . ∃/∀q 1 . . . . ∃/∀q n . ϕ, where ϕ is quantifier free. Figure 1 summarizes our results. We establish that a major factor for the decidability of the realizability problem consists in the number of universal trace occurring in a formula. Realizability of HyperQPTL formulas without ∀π quantifiers is decidable (Sect. 4.1). Formulas with a single ∀π are decidable if they belong to the ∃ * q/π ∀ * q ∀ π Q * q fragment. This fragment also contains promptness. For more than one universal trace quantifier, we show that decidability can be guaranteed for a fragment that we call the linear ∀ * π Q * q fragment. We also show that all the above fragments are tight, i.e., realizability of all other formulas is in general undecidable. Lastly, Sect. 5 presents experiments for the prototype implementation of our bounded synthesis algorithm for HyperQPTL.

We use AP for a set of atomic propositions. A trace over AP is an infinite sequence t ∈ (2 AP ) ω . For i ∈ N, we write t[i] for the ith element of t and t[i, ∞] for the suffix of t starting from position i. For two traces t, t over AP and a set AP' ⊆ AP, we write t = AP' t to indicate that t and t agree on all a ∈ AP', and respectively T = AP' T for two sets of traces T and T . Furthermore, we define a replacement function t[q → t q ] that given a trace t and a trace t q ∈ (2 {q} ) ω , replaces the occurrences of q in t according to t q , such that t[q → t q ] = {q} t q and t[q → t q ] = AP\{q} t. We also lift this notation to sets of traces and define

QPTL [31] extends Linear Temporal Logic (LTL) with quantification over propositions. QPTL formulas ϕ are defined as follows.

where q ∈ AP and AP is a set of atomic propositions. For simplicity, we assume that variable names in formulas are cleared of double occurrences. The semantics of ϕ over AP is defined with respect to a trace t ∈ (2 AP ) ω .

We did not define the until operator U as native part of the logic. It can be derived using propositional quantification [23] . The boolean connectives ∧, →, ↔ and the temporal operators globally and release R are derived as usually.

Just like LTL, HyperLTL cannot express ω-regular languages [29] . LTL can be extended to QPTL by adding quantification over atomic propositions. In QPTL, ω-regular languages become expressible. We therefore study HyperQPTL [6, 29] , the extension of HyperLTL with propositional quantification, to express ω-regular hyperproperties. Given a set AP of atomic propositions and a set V of trace variables, the syntax of HyperQPTL is defined as follows

where a, q ∈ AP and π ∈ V. As for QPTL, we assume that formulas are cleared of double occurrences of variable names. We require that in well-defined HyperQPTL formulas, each a π is in the scope of a trace quantifier binding π and each q is in the scope of a propositional quantifier binding q. Note that atomic propositions a π refer to a quantified trace π, whereas quantified propositional variables q are independent of the traces. The semantics of a welldefined HyperQPTL formula over AP is defined with respect to a set of traces T ⊆ (2 AP ) ω and an assignment function Π : V → T . We define the satisfaction relation Π, i |= T ϕ as follows:

Note that the semantics of propositional quantification is defined in such a way that in the scope of a quantifier binding q, all traces agree on their q-sequence. We say that a set of traces T satisfies a HyperQPTL formula ϕ if ∅, 0 |= T ϕ, where ∅ is the empty trace assignment. QPTL formulas can be expressed in HyperQPTL using a single universal trace quantifier. Furthermore, HyperLTL [4] is the syntactic subset of HyperQPTL that does not contain propositional quantification. While HyperQPTL can express a wide range of properties (see Sect. 3.1), its model checking problem is still decidable [29] . Furthermore, the syntactic fragments for which satisfiability is decidable can be expressed solely in terms of the occurring trace quantifiers: Just like for HyperLTL, satisfiability of a HyperQPTL formula is decidable if no ∀π is followed by an ∃π [6] .

The definition of HyperQPTL is straightforward, however, one could argue that it is not the only way to extend QPTL to a hyperlogic. The original idea of QPTL is to "color" the trace by introducing additional atomic propositions. The way HyperQPTL is defined, that idea is translated to sets of traces by coloring the traces uniformly. An alternative approach could be to color every trace individually by introducing a full atomic proposition for every propositional quantification. This resembles full second-order quantification and would therefore result in a considerably more expressive logic. In particular, we show that the model checking problem would become undecidable, which is, especially in the context of automatic verification, unfavorable. For the remainder of this section, we call the logic resulting from the alternative definition HyperQPTL + . The syntax of HyperQPTL + is similar to the one of HyperQPTL, just without the rule q for the evaluation of the propositional variables. This accounts for the idea that the propositional quantification can freely reassign atomic propositions; thus, there is no need to distinguish between free atomic propositions and quantified atomic propositions:

Semantically, only the rules for the quantification of the propositional quantifiers change:

Lemma 1. The HyperQPTL + model checking problem is undecidable.

Proof. Given a finite Kripke structure K and a HyperQPTL + formula ϕ, the model checking problem asks whether the trace set T produced by K satisfies ϕ. The proof follows the undecidability proof for the model checking problem of S1S[E] [6] , a logic which lifts S1S to the level of hyperlogics. We describe a reduction from the halting problem of 2-counter machines (which are Turing complete) to the HyperQPTL + model checking problem. A 2-counter machine (2CM) consists of a finite set of serially numbered instructions that modify two counters. A configuration of a 2CM is a triple (n, v 1 , v 2 ) ∈ N 3 , where n determines the next instruction to be executed, and v 1 and v 2 assign the counter values. Each instruction can either increase or decrease one of the counters; or test either of the counters for zero and, depending on the outcome, jump to another instruction. Furthermore, we assume a special instruction i halt , which indicates that the machine has reached a halting state. A 2CM halts from initial configuration s 0 if there is a finite sequence s 0 , . . . , s n of configurations such that s n is a halting configuration and s i+1 is a result of applying the instruction in s i to configuration s i . Let M be a 2CM. We describe T and ϕ such that T |= ϕ iff M halts. We choose AP = {i, c 1 , c 2 } and T is the set of all traces where each atomic proposition holds exactly once. That way, a trace t encodes a configuration of the machine:

. It is easy to see that T can be produced by a finite Kripke structure. To describe ϕ, we make two helpful observations. First, using propositional quantification, we can quantify a trace set T q ⊆ T : a trace t is in T q iff the quantified proposition q eventually occurs on t. Second, for two traces t, t ∈ T , we can state that t encodes a configuration which is the successor of the configuration encoded by t. Using these observations, we define ϕ = ∃q. ϕ , where q encodes a set T q ⊆ T that is supposed to describe a halting computation.

To ensure that T q describes a halting computation, ϕ is a conjunction of the following requirements: T q must 1. be finite, 2. contain a halting configuration and the initial configuration, 3. be predecessor closed with respect to the encoded configurations it contains (except for the initial configuration).

Finiteness of T q can be expressed by stating that there is an upper bound on the values of i, c 1 , and c 2 on the traces in T q . With the observations made before, stating the above requirements in HyperQPTL + now remains a straightforward exercise.

Since the model checking problem of HyperQPTL + is undecidable, we focus on HyperQPTL to express ω-regular hyperproperties. In particular, we show that HyperQPTL can express a range of relevant properties that are neither expressible in HyperLTL, nor in QPTL.

HyperQPTL combines trace quantification with ω-regularity. The interplay between the two features enables HyperQPTL to express a variety of properties. In Sect. 1, we showed how HyperQPTL can express a form of promptness.

In this section, we further elaborate on the type of properties HyperQPTL can express. In particular, we compare it to Prompt-LTL, a logic that extends LTL with bounded eventualities. Furthermore, HyperQPTL is also able to express epistemic properties by emulating the knowledge operator known from LTL K . A straightforward class of properties HyperQPTL can express are ω-regular properties over n-tuples of quantified traces. Formulas expressing this type of properties first have a trace quantifier prefix followed by a QPTL formula, i.e., they lie in the Q * π Q * q fragment. This fragment of HyperQPTL corresponds to the extension of QPTL with prenex trace quantification. However, the true expressive power of HyperQPTL originates from the fact that we allow the trace quantifiers and propositional quantifiers to alternate.

Promptness Properties. Promptness properties are an example for HyperQPTL's interplay between trace quantification and propositional quantification. Promptness expresses that eventualities are fulfilled within a bounded number of steps. One way to express promptness properties is the logic Prompt-LTL, which extends LTL with the promptness operator p . A system satisfies a Prompt-LTL formula ϕ if there is a bound k such that all traces of the system fulfill the formula where each p in ϕ is replaced by ≤k , i.e., the system must fulfill all prompt eventualities within k steps. For example, ϕ = p ψ holds in a system if there is a bound k such that all traces of the system at all times satisfy ψ within k steps. HyperQPTL can express a different type of promptness properties. In Sect. 1, Formula 2, we showed how one can state in HyperQPTL that there is a bound, common for all traces, until which an eventuality has to be fulfilled. The idea is to quantify a new proposition b, such that the first position in which b is true serves as the bound. Compared to Prompt-LTL, HyperQPTL thus expresses a weaker form of promptness, while still being stronger than pure eventuality. This type of promptness only becomes meaningful when comparing several traces of the system: HyperQPTL can enforce that there is a common bound for all traces (the system cannot starve), but it does not make the bound explicit. The following example shows a more involved promptness property expressible in HyperQPTL.

Example 1. HyperQPTL can express bounded waiting for a grant. It states that if the system requests access to a shared resource at point in time t, then it will be granted access within a bounded amount of time. The bound may depend on the point in time t where access to the resource was requested. However, it may not depend on the current trace. We express this property in HyperQPTL as follows, also adding that the system will not request access twice without being granted access in between.

∀π. (r π → (¬r π W g π ))

(1)

Formula 1 states that no second request is posed before being given a grant. Formula 2 expresses the bounded waiting property by universally quantifying a trace, then existentially quantifying a sequence of bounds b. Now, for every trace π , whenever π and π pose a request at the same point in time, both have to get access to the resource before b holds next. Therefore, for each point in time, there is a bound such that all traces posing a request at that point in time get access within a bounded number of steps. Note that this property differs from saying "all traces are eventually granted access", where the bound may also depend on the trace under consideration. In this scenario, each of the infinitely many traces could wait arbitrarily long for the grant. In particular, it could happen that with each trace the waiting time is longer than before.

The above example shows how the interplay of trace quantifiers and propositional quantifiers can be leveraged to express a new class of promptness properties. We finally note that compared to Prompt-LTL, HyperQPTL cannot express that all eventualities must be fulfilled within a fixed k number of steps.

Epistemic Properties. Another interesting class of properties that are not expressible in HyperLTL are epistemic properties. Epistemic properties describe the knowledge of agents that interact with each other in a system. Logics that express epistemic properties are often equipped with a so-called knowledge operator, e.g., LTL K , which is LTL extended with the knowledge operator K A ϕ. The operator denotes that an agent A ⊆ AP knows ϕ. An agent A is characterized in terms of the atomic propositions he can observe. The semantics of the operator is described with the following rule

The formula is evaluated with respect to a trace t and a position i. We omit the semantic definition for the rest of the logic, which corresponds to plain LTL. The semantic definition of the operator captures the idea that an agent knows some fact ϕ if ϕ holds on all traces that are indistinguishable for the agent.

Example 2 (Dining Cryptographers). The dining cryptographers problem [3] is an interesting example of how epistemic properties can characterize non-trivial protocols. The problem describes the following situation (see Fig. 2 ): three cryptographers C 1 , C 2 , and C 3 sit at a table in a restaurant and either one of cryptographers or, alternatively, the NSA paid for their meal. The task for the cryptographers is to figure out whether the NSA or one of the cryptographers paid. However, if one of the cryptographers paid, then the others must not be able to infer who it was. Each cryptographer C i receives several bits of information: paid i indicating whether or not he pays the bill, and two secrets, each shared with one of the other cryptographers. The secrets can be used to encode the information they share as output out i . By combining the outputs of all cryptographers, it must become clear whether the NSA or one of the group paid. The specification of the protocol can be easily formalized in LTL K . The following formula describes the desired behavior of agent C 1 :

The knowledge operator can also be defined for hyperlogics [29] . It receives an additional parameter π, indicating the trace the knowledge refers to. When added to HyperQPTL, it has the following semantics:

The knowledge operator, however, can be encoded in HyperQPTL using propositional quantification. Epistemic problems, such as the dining cryptographers problem, can thus be expressed in HyperQPTL.

Proof. We recap the proof from [29] : Let ϕ = Q π/q . . . Q π/q . ϕ be a HyperQPTL formula, equipped with the knowledge operator as defined above. We assume that ϕ is given in negated normal form, i.e. each K A,π occurs either in positive position or in negated form. Let u and t be fresh propositions and let π be a fresh trace variable. Recursively, we replace each knowledge operator K A,π occurring in ϕ in positive position with the following formula

and each K A,π occurring negatively with the following formula

where we use ϕ [K A,π ψ → u] to denote that in ϕ , a single occurrence of the knowledge operator is replaced by u, and ψ[π → π ] to denote the formula where π is replaced by π . The existentially quantified proposition u indicates the points in time where the knowledge operator is supposed to hold/not hold. The universally quantified proposition r is assumed to change once from r to ¬r and thereby point at one of the points in time picked by u. It is then used to compare the prefix of the old trace π and an alternative trace quantified by the trace variable π .

In reactive synthesis, the task is, given a specification ϕ, to construct a system that satisfies the specification. More precisely, the system is assumed to receive some inputs from an environment and has to react with outputs such that the specification is fulfilled. The realizability problem asks for the existence of a so-called strategy tree, where the edges are labeled with all possible inputs and the task is to find a function f that labels the nodes with the corresponding outputs. Figure 3 shows a strategy tree for a single input bit i. We define strategies following [12] . Let a set AP = I∪ O be given. A strategy f : (2 I ) * → 2 O maps sequences of input valuations 2 I to an output valuation 2 O . For an infinite word w = w 0 w 1 w 2 · · · ∈ (2 I ) ω , the trace corresponding to a strategy f is defined as

For any trace w = w 0 w 1 w 2 . . . ∈ (2 I∪O ) ω and strategy f :

We say that a strategy f satisfies a HyperQPTL formula ϕ over AP

With the definition of a strategy at hand, we can define the realizability problem of HyperQPTL formally. Fig. 3 . A strategy tree for the reactive realizability problem.

For technical reasons, we assume (without loss of generality) that quantified atomic propositions are classified as outputs, not inputs. This complies with the intuition that propositional quantifiers should be a means for additional expressiveness; they should not overwrite the inputs received from the environment. The definition of realizability of QPTL and HyperLTL specifications is inherited from the definition for HyperQPTL. Compared to the standard realizability problem, the distributed realizability problem is defined over an architecture, containing a number of processes interacting with each other. The goal is to find a strategy for each of the processes. In the following proofs, we will make use of the distributed realizability problem of QPTL, which we therefore also define formally.

A distributed architecture [17, 27] A over atomic propositions AP is a tuple P, p env , I, O , where P is a finite set of processes and p env ∈ P is a designated environment process. The functions I : P → 2 AP and O : P → 2 AP define the inputs and outputs of processes. The output of one process can be the input of another process. The output of the processes must be pairwise disjoint, i.e., for all p = p ∈ P it holds that O(p) ∩ O(p ) = ∅. We assume that the environment process forwards inputs to the processes and has no input of its own, i.e., I(p env ) = ∅.

such that the combination of all f p satisfies ϕ.

The distributed realizability problem for QPTL is (inherited from LTL) in general undecidable [27] . However, we will use the result that the problem remains decidable for architectures without information forks [17] . The notion of information forks captures the flow of data in the system. Intuitively, an architecture contains an information fork if the processes cannot be ordered linearly according to their informedness. Formally, an information fork in an architecture A = P, p env , I, O is defined as a tuple (P , V , p, p ), where p, p are two different processes, P ⊆ P , and V ⊆ AP is disjoint from I(p) ∪ I(p ). (P , V , p, p ) is an information fork if P together with the edges that are labeled with at least one variable from V forms a subgraph rooted in the environment and there exist two nodes q, q ∈ P that have edges to p, p , respectively, such that

The definition formalizes the intuition that p and p receive incomparable input bits, i.e., they have incomparable information.

Example 3. Two example architectures are depicted in Fig. 4 [12] . The processes in Fig. 4a receive distinct inputs and thus neither process is more informed than the other. The architecture therefore contains an information fork with P = {env , p, p }, V = {i, i }, q = env , q = env . The processes in Fig. 4b can be ordered linearly according to the subset relation on the inputs and thus the architecture contains no information fork.

In the following sections, we identify tight syntactic fragments of HyperQPTL for which the standard realizability problem is decidable. We give decidability proofs and show that formulas outside the decidable fragments are in general undecidable. An important aspect for decidability is the number of universal trace quantifiers that appear in the formula. We thus present our findings in three categories, depending on the number of universal trace quantifiers a formula has.

We show that the realizability problem of any HyperQPTL formula without a ∀ π quantifier is decidable. The problem is reduced to QPTL realizability.

Realizability of the (∃ * π Q * q ) * fragment of HyperQPTL is decidable.

Proof. Let a (∃ * π Q * q ) * HyperQPTL formula ϕ over AP = I∪ O = {a 0 , . . . , a k } with trace quantifiers π 0 , . . . π n be given. We reduce the problem to the realizability problem of QPTL, which is known to be decidable (since QPTL formulas can be translated to Büchi automata). The idea is to replace each existential trace quantifier ∃π i with quantification of propositions a 0 πi , a 1 πi , . . . , a k πi , one for each a j ∈ AP, thereby mimicking the quantification of a trace. To make sure that only traces from an actual strategy tree are chosen, we add a dependency formula which forces the outputs to be dependent on the inputs. The following QPTL formula implements the idea.

We use the notation [i ≤ n : ∃π i → ∃a 0 πi . . . . ∃a k πi . ] to indicate that each π i for 0 ≤ i ≤ n is replaced with the respective series of existential propositional quantification. Furthermore, we write I πi = I πj as syntactic sugar for a∈I a πi a πj (and similarly for O πi = O πj ). We show that ϕ and ϕ QPTL are equirealizable. For the first direction, assume that ϕ is realizable by a strategy f . Notice that all atomic propositions in ϕ QPTL are bound by a propositional quantifier. Therefore, if the witness sequences for the quantified propositions can be chosen correctly, any strategy realizes ϕ QPTL . Propositions a j πi are chosen according to the witness traces of f |= ϕ. Witnesses for the remaining atomic propositions are also chosen according to their witnesses from f |= ϕ. Now, the first conjunct of ϕ QPTL is fulfilled since f |= ϕ holds. The second conjunct is fulfilled since any two traces π i , π j of a strategy tree fulfill by construction (I πi = I πj ) R(O πi = O πj ). For the other direction, assume that ϕ QPTL is realizable (by construction independently from the strategy). Let t a 0 π 0 , . . . , t a k πn be the witness sequences for the respective quantified atomic propositions. The following strategy realizes ϕ.

Strategy f chooses the outputs according to the witnesses for the propositions encoding the traces. Note that because of the second conjunct in ϕ QPTL , the output is always unique, even if several encoded traces start with the same input sequence. Now, f |= ϕ holds because of the first conjunct of ϕ QPTL .

In this fragment, we allow exactly one universal trace quantifier. It is particularly interesting as it contains many promptness properties. For example, the following promptness formulation mentioned in the introduction lies within the fragment:

Theorem 3. Realizability of the ∃ * q/π ∀ * q ∀ π Q * q fragment is decidable. We show the theorem in two steps. First, we generalize a proof from [12] , showing that realizability of the ∃ * π ∀ π Q * q fragment is decidable. Second, we show that we can reduce the realizability problem of any HyperQPTL formula to a formula where some propositional quantifiers are replaced with trace quantifiers. 

Realizability of the ∃ * π ∀ π Q * q fragment is decidable.

Proof. The reasoning generalizes the proof in [12] showing that realizability ∃ * π ∀ π HyperLTL formulas is decidable. We reduce the problem to the distributed realizability problem of QPTL without information forks, which issince QPTL is subsumed by the μ-calculus-decidable [17] . Let a HyperQPTL formula ϕ = ∃π 1 The architecture is displayed in Fig. 5 . The idea is that process p 1 sets the values of all i πj and o πj (for j ≤ n) and thereby determines the choice for the existentially quantified traces. Process p 1 receives no input and therefore needs to make a deterministic choice. Process p 2 then solves the realizability of formula ∀π. ψ. The following QPTL formula ϕ encodes the idea.

where ψ is defined as ψ, where all a π are replaced by a (but atomic propositions a πj are still part of ψ !). Note that QPTL formulas implicitly quantify over all traces universally. Similarly to the proof in Theorem 2, the second conjunct ensures that process p 1 encodes actual paths from the strategy tree of process p 2 (which is also the strategy tree for formula ϕ). Thus, ϕ is realizable for the distributed architecture A iff ϕ is realizable.

To state the second lemma, we need to define what it means to replace quantifiers in a formula. Let ϕ = Q π/q , . . . , Q π/q . ψ be a HyperQPTL formula, and J be a set of indices such that for all j ∈ J, there exists a propositional quantifier ∃q j or ∀q j in ϕ. Furthermore, assume that no π j with j ∈ J occurs in ϕ and that a ∈ AP. We denote by ϕ[J → a π] the formula where each propositional quantifier ∃q j (or ∀q j , respectively) with j ∈ J is replaced with the corresponding trace quantifier ∃π j (or ∀π j , respectively); and each q j in ψ is replaced by a πj . Lemma 3. Let any HyperQPTL formula ϕ over AP = I∪O and a set of indices J be given. If ϕ[J → i π] is realizable, then so is ϕ, where i ∈ I is an arbitrary input, assuming w.l.o.g., that I is non-empty.

Proof. Let ϕ and J be given. Formula ϕ[J → i π] replaces the quantification over sequences (2 {q} ) ω with trace quantification, where the trace is only used for statements about a single input i. We thus exploit the fact that in the realizability problem, there is a trace for every input sequence. Therefore, the transformed formula is equirealizable. Now, we have everything we need to prove Theorem 3.

Let ϕ be a HyperQPTL formula of the ∃ * q/π ∀ * q ∀ π Q * q fragment. First, observe that in the quantifier prefix of ϕ, the ∀ * q quantifiers and the ∀ π can be swapped. The resulting formula belongs to the ∃ * q/π ∀ π Q * q fragment. By Lemma 3, the formula can be transformed to a equirealizable formula of the ∃ * π ∀ π Q * q fragment, for which realizability is decidable by Lemma 2.

Lemma 3 allows us to decide realizability of a HyperQPTL formula by replacing propositional quantifiers with trace quantifiers. Thus, we can reduce HyperQPTL realizability to HyperLTL realizability, a fact that we use in Sect. 5 to describe a bounded synthesis algorithm for HyperQPTL.

The realizability problem of HyperQPTL can be soundly reduced to the realizability problem of HyperLTL.

Lastly, we show that the decidable fragment is tight in the class of formulas with a single universal trace quantifier. We do so by showing that a propositional ∀ * q ∃ * q quantifier alternation followed by a single trace quantifier ∀ π leads to an undecidable realizability problem. The proof is carried out by a reduction from Post's Correspondence Problem.

Proof. Inherited from HyperLTL, realizability of formulas with a ∀ π quantifier followed by an ∃ π quantifier is undecidable [12] . It remains to show that realizability of formulas from the ∀ * q ∃ * q ∀ π fragment is in general undecidable. We give a reduction from Post's Correspondence Problem (PCP) [28] to a HyperQPTL formula from the ∀ * q ∃ * q ∀ π fragment. In PCP, we are given two equally long lists α and β consisting of finite words from some alphabet Σ of size n. PCP is the problem to find an index sequence (i k ) 1≤k≤K with K ≥ 1 and 1 ≤ i k ≤ n, such that α i1 . . . α iK = β i1 . . . β iK . Intuitively, PCP is the problem of choosing an infinite sequence of domino stones (with finitely many different stones), where each stone We writeã to denote either a orȧ. The single input i spans a binary strategy tree. We encode the PCP instance into a HyperQPTL formula that is realizable if and only if the PCP instance has a solution:

where q and p are sequences of universally and existentially quantified propositional variables, such that for each (o, o ) ∈ O, there is a q (o,o ) ∈ q and a p (o,o ) ∈ p. Together with q i and p i for the input i, they simulate a universally and an existentially quantified trace from the model. The notation π = q denotes that for every q a ∈ q, it holds that a π ↔ q a . As seen before, the premise ( π = (q i , q)) and the conjunct ( π = p i ) → ( π = p) ensure that the propositions (q i , q) and (p i , p) are chosen to represent actual traces from the model. The universal quantification π thus only ensures that (q i , q) and (p i , p), which are used for the main reduction, are chosen correctly. The reduction is implemented in the formula ϕ reduc and follows the construction in [10] , where it is shown that the satisfiability and realizability problem of HyperLTL are undecidable for a ∀∃ trace quantifier prefix.

-ϕ rel (q i ) := ¬q i U q i defines the set of relevant traces trough the binary strategy tree (see Fig. 6 ).

defines that a relevant trace is the direct successor trace of another relevant trace.

q (ãi,ãi) )) U q (#,#) ensures that the path on which globally i holds is a "solution" trace, i.e., encodes the PCP solution sequence.

-ϕ start (ϕ, q i ) := ¬q i U(ϕ ∧ q i ) cuts off an irrelevant prefix until ϕ starts.

-ϕ stone&shift (q, p) encodes that the trace simulated by q starts with a valid encoding of a stone from the PCP instance and that the trace simulated by p encodes the same trace but with the first stone removed (see [10] ).

For example, let α with α 1 = a, α 2 = ab, α 3 = bba, and β with β 1 = baa, β 2 = aa and β 3 = bb be given. A possible solution for this PCP instance is be (3, 2, 3, 1), since bbaabbbaa = i α = i β . The full sequence at the trace i represents the solution with the outputs The relevant traces verify the solution provided on the i trace by removing one stone after the other. Thus, the formula is realizable iff the PCP instance has a solution.

When considering multiple universal trace quantifiers ∀ * π , the problem becomes undecidable. This is because in HyperLTL, one can encode distributed architectures -for which the problem is undecidable -directly into the formula without using any propositional quantification [12] .

Realizability of the ∀ * π fragment is in general undecidable. However, we show that the realizability problem for formulas with more than one universal trace quantifier is decidable if we restrict ourselves to formulas in the so-called linear fragment, i.e., that does not allow an encoding of a distributed architecture. We define the linear fragment of HyperQPTL, where the definitions are adopted from [12] .

Let A, C ⊆ AP. We define that atomic propositions c ∈ C do solely depend on propositions a ∈ A as the HyperQPTL formula benchmarks sets, shown in Table 1 . The first column indicates the parameterized benchmark name. The second and third columns indicate the bounds given to the bounded synthesis procedure. The second column is the bound on the size of the system. The newest version of BoSy also bounds the size of the strategy for the existential player, this bound is given in column three. For a detailed explanation of how existential strategies are bounded in BoSy, we refer to [7] . We synthesized a range of resource arbiters. Our benchmark set is parametric in the number of clients that can request access to the shared resource (written arbiter-k-prompt where k is the number of clients in Table 1 ). Unlike normal arbiters, we require the arbiter to fulfill promptness for some of the clients, i.e., requests must be answered within a bounded number of steps [33] . We state the promptness requirement in HyperQPTL by applying the alternating-color technique from [24] . Intuitively, the alternating-color technique works as follows:

We quantify a q-sequence that "changes color" between q and ¬q. Each change of color is used as a potential bound. Once a request occurs, the grant must be given withing two changes of color. Thus, the HyperQPTL formulation amounts to the following specifications, here exemplary for 2 clients, where we require promptness only for client 1.

∀π. ¬(g 1 π ∧ g 2 π ) (1)

∧ (r 1 π → (q → (q U(¬q U g 1 π ))) ∧ (¬q → (¬q U(q U g 1 π )))) ∀π.(¬g 1 π W r 1 π ) ∧ (¬g 2 π W r 2 π ) (4) Formula 1 states mutual exclusion. Formula 2 states that client 2 must be served eventually (but not within a bounded number of steps). Formula 3 states the promptness requirement for client 1. It quantifies an alternating q-sequence, which serves as a sequence of global bounds that must be respected on all traces π. Then, if client 1 poses a request, the grant must be given within two changes of the value of q. Formula 4 is only added in benchmarks named arbiter-k-fullprompt. It specifies that no spurious grants should be given. BoSy successfully synthesizes prompt arbiter of up to 3 states. For a 4-state prompt arbiter BoSy did not return in reasonable time.

We studied the hyperlogic HyperQPTL, which combines the concepts of trace relations and ω-regularity. We showed that HyperQPTL is very expressive, it can express properties like promptness, bounded waiting for a grant, epistemic properties, and, in particular, any ω-regular property. Those properties are not expressible in previously studied hyperlogics like HyperLTL. At the same time, we argued that the expressiveness of HyperQPTL is optimal in a sense that a more expressive logic for ω-regular hyperproperties would have an undecidable model checking problem. We furthermore studied the realizability problem of HyperQPTL. We showed that realizability is decidable for HyperQPTL fragments that contain properties like promptness. But still, in contrast to the satisfiability problem, propositional quantification does make the realizability problem of hyperlogics harder. More specifically, the HyperQPTL fragment of formulas with a universal-existential propositional quantifier alternation followed by a single trace quantifier is undecidable in general, even though the projection of the fragment to HyperLTL has a decidable realizability problem. Lastly, we implemented the bounded synthesis problem for HyperQPTL in the prototype tool BoSy. Using BoSy with HyperQPTL specifications, we have been able to synthesize several resource arbiters. The synthesis problem of non-linear-time hyperlogics is still open. For example, it is not yet known how to synthesize systems from specifications given in branching-time hyperlogics like HyperCTL * .

Program repair for hyperproperties

Unifying hyper and epistemic temporal logics

Security without identification: transaction systems to make big brother obsolete

Temporal logics for hyperproperties

The hierarchy of hyperlogics

Verifying hyperliveness

Z3: an efficient SMT solver

BoSy: an experimentation framework for bounded synthesis

Deciding hyperproperties

MGHyper: checking satisfiability of hyperltl formulas beyond the ∃ * ∀ * fragment

Synthesizing reactive systems from hyperproperties

EAHyper: satisfiability, implication, and equivalence checking of hyperproperties

Model checking quantitative hyperproperties

Algorithms for model checking hyperLTL and hyperCTL *

Uniform distributed synthesis

Bounded synthesis

The first-order logic of hyperproperties

Security policies and security models

Algorithms for monitoring hyperproperties

The complexity of reasoning about knowledge and time. i. lower bounds

Using automata to characterise fixed point temporal logics

From liveness to promptness. Formal Methods Syst

Hyperproperties of real-valued signals

The temporal logic of programs

Distributed reactive systems are hard to synthesize

A variant of a recursively unsolvable problem

A temporal logic approach to information-flow control

The complementation problem for Büchi automata with applications to temporal logic

Theoretical issues in the design and verification of distributed systems

Gray-box monitoring of hyperproperties

Approximating optimal bounds in prompt-ltl realizability in doubly-exponential time

Observational determinism for concurrent program security

Open Access This chapter is licensed under the terms of the Creative Commons

We define a collapse function, which collapses a HyperQPTL formula with a ∀ * π universal quantifier prefix into a formula with a single ∀ π quantifier. Propositional quantifiers are preserved by the operation. Let ϕ be ∀π 1 · · · ∀π n . Q * q . ψ. We define the collapsed formula of ϕ as collapse(ϕ)replaces all occurrences of π i in ψ with π.Proof. The collapse function solely works on the trace quantification mechanism of the HyperQPTL formula, by reducing them to a single universal quantification. The theorem has been proven for ∀ * HyperLTL formulas in [12] . Inner propositional quantification does not interfere with this mechanism, hence, the proof can be carried out identically.Now we can formally define the linear ∀ * π fragment. Intuitively, we require that every input-output dependency can be ordered linearly, i.e., we are restricted to linear architectures without information forks (see Example 3).This results in the following corollary. Since the universal quantifiers can be collapsed, the resulting problem is the realizability problem of QPTL in a linear architecture, which is decidable [17] .

Remark on Complexities. Our aim was to work out the largest possible fragments for which the realizability problem of HyperQPTL remains decidable. The three fragments for which we could prove decidability all subsume the logic QPTL, for which the realizability problem is known to be non-elementary (already its satisfiability problem is non-elementary [30] ). Hence, realizability of the discussed HyperQPTL fragments has a non-elementary lower bound. Finding interesting fragments for which the problem has a more feasible complexity therefore remains an open challenge.

We have implemented a prototype tool that can solve the HyperQPTL realizability problem using the bounded synthesis approach [18] . More concretely, we extended the HyperLTL synthesis tool BoSy [7, 9, 12] . Bosy reduces the HyperLTL synthesis problem to a SMT constraint system which is then solved by z3 [8] (for more see [12] ). We implemented the reduction of HyperQPTL synthesis to HyperLTL synthesis (Corollary 2) in BoSy, such that the tool can also handle HyperQPTL formulas. We evaluated the tool against a range of