1 Introduction
The introduction of temporal logics for the specification of information flow policies [DBLP:conf/post/ClarksonFKMRS14] was a significant milestone in the long and successful history of applying logics in computer science [journals/bsl/HalpernHIKVV01]
. Probably the most important representative of these logics is HyperLTL
[DBLP:conf/post/ClarksonFKMRS14], which extends Linear Temporal Logic (LTL) [Pnueli/1977/TheTemporalLogicOfPrograms] by trace quantifiers. This addition allows to express properties that relate multiple execution traces, which is typically necessary to capture the flow of information [Clarkson+Schneider/10/Hyperproperties]. In contrast, LTL, currently the most influential specification language for reactive systems, is only able to express properties of single traces.HyperLTL provides a uniform framework for expressing information flow policies in a formalism with intuitive syntax and semantics, and for the automated verification of these policies: A wide range of policies from the literature [DBLP:conf/sp/GoguenM82a, DBLP:conf/sp/McCullough88, DBLP:journals/tse/McCullough90, DBLP:conf/sp/McLean94, DBLP:journals/jcs/Millen95, DBLP:conf/csfw/ZdancewicM03] with specialized verification algorithms is expressible in HyperLTL, i.e., universal HyperLTL verification algorithms are applicable to all of them.
As an example, consider a system with a set of inputs, which contains a hidden input , and an output . Now, noninterference [DBLP:conf/sp/GoguenM82a] between and requires that no information about is leaked via , i.e., for all execution traces and , if the inputs in and only differ in , then they have the same output at all times. Formally, this is captured by the HyperLTL formula
Today, there are tools for model checking HyperLTL properties [hyperliveness, DBLP:conf/cav/FinkbeinerRS15], for checking satisfiability of HyperLTL properties [DBLP:conf/cav/FinkbeinerHS17], for synthesizing reactive systems from HyperLTL properties [DBLP:conf/cav/FinkbeinerHLST18], and for runtime monitoring of HyperLTL properties [DBLP:conf/rv/BonakdarpourF16, DBLP:conf/tacas/FinkbeinerHST18]. Furthermore, the extraordinary expressiveness of HyperLTL has been exhibited [DBLP:conf/stacs/Finkbeiner017] and connections to first and secondorder predicate logics have been established [hierarchy, DBLP:conf/stacs/Finkbeiner017].
The major drawback of HyperLTL is the usual price one has to pay for great expressiveness: prohibitively high worstcase complexity. In particular, model checking finite Kripke structures against HyperLTL formulas is nonelementary [DBLP:conf/post/ClarksonFKMRS14] and satisfiability is even undecidable [DBLP:conf/concur/FinkbeinerH16]. These results have to be contrasted with model checking and satisfiability being PSpacecomplete for LTL [Sistla:1985:CPL:3828.3837], problems routinely solved in reallife applications [Kurshan2018].
Due to the sobering state of affairs, it is imperative to find fragments of the logic with (more) tractable complexity. In this work, we focus on the satisfiability problem, the most fundamental decision problem for a logic. Nevertheless, it has many applications in verification, e.g., checking the equivalence and implication of specifications can be reduced to satisfiability. Finally, the question whether a property given by some HyperLTL formula is realizable by some system is also a satisfiability problem.
A classical attempt to overcome the undecidability of the satisfiability problem is to restrict the number of quantifier alternations of the formulas under consideration. In fact, the alternation depth is the measure underlying the nonelementary complexity of the HyperLTL model checking problem [DBLP:conf/post/ClarksonFKMRS14]. However, the situation is different for the satisfiability problem: It is undecidable even when restricted to formulas, i.e., formulas starting with one universal quantifier followed by existential ones [DBLP:conf/concur/FinkbeinerH16]. All remaining prefix classes are decidable by reductions to the LTL satisfiability problem, e.g., the satisfiability problem is PSpacecomplete for the alternationfree prefix classes and and ExpSpacecomplete for the class [DBLP:conf/concur/FinkbeinerH16].
However, there are more complexity measures beyond the alternation depth that can be restricted in order to obtain tractable satisfiability problems, both on formulas and on models. The latter case is of particular interest, since it is known that not every satisfiable HyperLTL has a “simple” model, for various formalizations of “simple” [DBLP:conf/stacs/Finkbeiner017]. Thus, for those formulas, such a restriction could make a significant difference. Furthermore, from a more practical point of view, one is often interested in whether there is a, say, finite model while the existence of an intricate infinite model may not be useful.
We study the satisfiability problem for formulas with restricted quantifier prefixes and restricted temporal depth [DBLP:journals/iandc/DemriS02], which measures the nesting of temporal operators. Our main result here shows that satisfiability is even undecidable for formulas of the form , where has temporal depth one and only uses eventually and always , i.e., it is a Boolean combination of formulas with propositional . Thereby, we strengthen the previous undecidability result for by bounding the temporal depth to one, but at the price of a second universal quantifier. Moreover, we clarify the border between decidability and undecidability at temporal depth two: Using only one universally quantified variable, temporal depth one, and only , , and nested applications of next leads to decidability. Finally, we show that every HyperLTL formula can be transformed into an equisatisfiable formula of temporal depth two, i.e., this fragment already captures the full complexity of the satisfiability problem.
Thus, the overall picture is still rather bleak: if one only restricts the formula then the islands of decidability are very small. Phrased differently, even very simple formulas are extremely expressive and allow to encode computations of Turingcomplete devices in their models. However, note that such models are necessarily complex, as they need to be able to encode an unbounded amount of information.
Thus, we also consider satisfiability problems for arbitrary formulas, but with respect to restricted models which do not allow to encode such computations. In particular, we consider three variants of increasing complexity: Checking whether a given HyperLTL formula has a model of a given cardinality is ExpSpacecomplete, whether it has a model containing only ultimately periodic traces of length at most is N2ExpTimecomplete, and checking whether it has a model induced by a Kripke structure with states is Towercomplete. The last result is even true for a fixed Kripke structure, which therefore has implications for the complexity of the model checking problem as well. Thus, the situation is more encouraging when checking for the existence of small models: satisfiability becomes decidable, even with (relatively) moderate complexity in the first two cases.
However, as argued above, all three approaches are (necessarily) incomplete: There are satisfiable formulas that have only infinite models, satisfiable formulas that have only nonultimately periodic models, and satisfiable formulas that have no regular models [DBLP:conf/stacs/Finkbeiner017], a class of models that includes all those that are induced by a finite Kripke structure.
All in all, our work shows that HyperLTL satisfiability remains a challenging problem, but we have provided a complete classification of the tractable cases in terms of alternation depth, temporal depth, and representation of the model (for formulas without until).
All proofs omitted due to space restrictions can be found in the appendix.
2 Definitions
Fix a finite set of atomic propositions. A valuation is a subset of . A trace over is a map , denoted by , i.e., an infinite sequence of valuations. The set of all traces over is denoted by . The projection of to is the trace over . A trace is ultimately periodic, if for some , i.e., there are with for all .
The formulas of HyperLTL are given by the grammar
where ranges over atomic propositions in and where ranges over a fixed countable set of trace variables. Conjunction, implication, equivalence, and exclusive disjunction , as well as the temporal operators eventually and always are derived as usual. A sentence is a closed formula, i.e., a formula without free trace variables. The size of a formula , denoted by , is its number of distinct subformulas.
The semantics of HyperLTL is defined with respect to a trace assignment, a partial mapping . The assignment with empty domain is denoted by . Given a trace assignment , a trace variable , and a trace we denote by the assignment that coincides with everywhere but at , which is mapped to . We also use shorthand notation like and for , if the are pairwise different. Furthermore, denotes the trace assignment mapping every in ’s domain to .
For sets of traces and trace assignments we define

, if ,

, if ,

, if or ,

, if ,

, if there is a such that and for all : ,

, if there is a trace such that , and

, if for all traces : .
We say that satisfies a sentence if . In this case, we write and say that is a model of . Conversely, satisfaction of quantifierfree formulas does not depend on . Hence, we say that satisfies a quantifierfree if and write (assuming is defined on all trace variables that appear in ).
The alternation depth of a HyperLTL formula , denoted by , is defined as its number of quantifier alternations. Its temporal depth, denoted by , is defined as the maximal depth of the nesting of temporal operators in the formula. Formally, and are defined as follows :



,

,

,


.

for quantifierfree

for quantifierfree


Although HyperLTL sentences are required to be in prenex normal form, they are closed under Boolean combinations, which can easily be seen by transforming such formulas into prenex normal form. Note that this transformation can be implemented such that it changes neither the temporal nor alternation depth, and can be performed in polynomial time.
The fragment HyperLTL contains formulas of temporal depth one using only and as temporal operators, and HyperLTL contains formulas using only , , and as temporal operators and of temporal depth one, however we allow iterations of the operator. Formally, HyperLTL formulas are generated by the grammar
where ranges over the natural numbers. The grammar for HyperLTL is obtained by removing from the grammar above.
Also, we use standard notation for classes of formulas with restricted quantifier prefixes, e.g., denotes the set of HyperLTL formulas in prenex normal form with two universal quantifiers followed by an arbitrary number of existential quantifiers, but no other quantifiers.
Finally, we encounter various complexity classes, classical ones from NP to N2ExpTime, as well as Tower (see, e.g., [DBLP:journals/toct/Schmitz16]). Intuitively, Tower
is the set of problems that can be solved by a Turing machine that, on an input of size
, stops in time , with the height of the tower of exponents bounded by , where is a fixed elementary function. The reductions presented in this work are polynomial time reductions unless otherwise stated.3 Satisfiability for Restricted Classes of Models
As the satisfiability problem “Given a HyperLTL sentence , does have a nonempty model?” is undecidable, even when restricted to finite models [DBLP:conf/concur/FinkbeinerH16]. Hence, one has to consider simpler problems to regain decidability. In this section, we simplify the problem by checking only for the existence of simple models, for the following three formalizations of simplicity, where the bound is always part of the input:

Models of cardinality at most (Theorem 3.1).

Models containing only ultimately periodic traces with (Theorem 3.2).

Models induced by a finitestate system with at most states (Theorem 3.3).
In every case, we allow arbitrary HyperLTL formulas as input and encode in binary.
With the following result, we determine the complexity of checking satisfiability with respect to models of bounded size. The algorithm uses a technique introduced by Finkbeiner and Hahn [DBLP:conf/concur/FinkbeinerH16, Theorem 3] that allows us to replace existential and universal quantification by disjunctions and conjunctions, if the model is finite. Similarly, the lower bound also follows from Finkbeiner and Hahn.
Theorem 3.1
The following problem is ExpSpacecomplete: Given a HyperLTL sentence and (in binary), does have a model with at most traces?
Proof
For the ExpSpace upper bound, one can check, given and , satisfiability of the sentence where is defined inductively as follows:

if is quantifierfree.

.

.
Here, is obtained from by replacing every occurrence of by . This sentence states the existence of at most traces satisfying by replacing every quantifier by an explicit conjunction or disjunction over the possible assignments.
The resulting sentence is of size at most , which is exponential in the size of the input and its satisfiability can be checked in polynomial space in the size of the resulting formula [DBLP:conf/concur/FinkbeinerH16]. As a result, the problem is in ExpSpace as well.
Finkbeiner and Hahn showed that satisfiability is ExpSpacecomplete for sentences of the form [DBLP:conf/concur/FinkbeinerH16]. This implies ExpSpacehardness of our problem, as if such a sentence, say with existential quantifiers, is satisfiable then it has a model with at most traces. ∎
As the algorithm proceeds by a reduction to the satisfiability problem for formulas, which in turn is reduced to LTL satisfiability, one can show that a HyperLTL sentence has a model with traces if and only if it has a model with ultimately periodic traces.
Next, we consider another variant of the satisfiability problem, where we directly restrict the space of possible models to ultimately periodic ones of the form with . As we encode in binary, the length of those traces is exponential in the input and the cardinality of the model is bounded doublyexponentially. This explains the increase in complexity in the following theorem in comparison to Theorem 3.1.
Theorem 3.2
The following problem is N2ExpTimecomplete: Given a HyperLTL sentence and (in binary), does have a model whose elements are of the form with ?
Proof
For the upper bound, given a HyperLTL sentence and in binary we start by guessing a model . Let be the size of the input. We have (as we can assume all atomic propositions appear in the formula, ), i.e., is doublyexponential in .
Then, we apply to a similar transformation as the one used in the proof of Theorem 3.1, i.e., we create a variable for each trace , and we replace in the sentence every universal (existential) quantifier by a conjunction (disjunction) over every possible trace assignment of the quantified variable over . Formally, we define as follows:

if is quantifierfree


The size of the formula is multiplied by at each new quantifier. In the end, the size of is at most . Define .
Observe that as , for all , for every . Thus, every quantifierfree formula evaluated over is satisfied at some index if and only if it is satisfied at some index less than . Therefore, one can evaluate over by recursively computing for each subformula the set of indices such that this subformula is satisfied by . This procedure is polynomial in the size of , and , all three being doublyexponential in , i.e., it is doublyexponential in the size of the input.
To prove the lower bound, we reduce from the following bounded variant of Post’s correspondence problem (PCP): Given two lists and of words, does there exist a word with and ? Here is the homomorphism induced by for every and is defined analogously. We refer to such a word as a solution. This variant is N2ExpTimehard, which can be shown by adapting the proof of undecidability of PCP as presented by Hopcroft and Ullman [DBLP:books/lib/HopcroftU69]. The same construction allows to reduce from the problem of deciding, given a nondeterministic Turing machine and a word , if halts on in at most steps.
Now, given an instance of this problem over an alphabet , we construct a sentence and a in polynomial time in such that has a model if and only if the instance has a solution.
Let be the maximal length of a word of the instance. For all , let and , i.e., for all . For every , let be a fresh letter and let . For all and let
be the word where the letter at position is replaced by its associated letter in . Analogously, we define .
Further, for all , let be the binary representation of , with the least significant bit at the beginning and without trailing zeros. Finally, for all let be the unique word over such that for all . If and
are not of the same length, then we pad the shorter one with
’s at the end.In the following, we work with the set
of atomic propositions. In the construction, we ensure that on every trace of the model exactly one proposition is satisfied at any moment in time. Thus, we treat traces as words over
without making a distinction between a proposition and the singleton .We define two types of traces:

Traces of type one are of the form for some and some , which is called the rank of the trace.

Traces of type two are of the form with , , and . Note that we allow .
A trace of type one and a trace of type two are compatible if and and compatible if and .
Fix a trace of type two. It is final if , and . If it is not final, then a trace of type two is a successor of , if one of the following holds:

and and .

and and for some .

and and for some .

and (which implies , as is not final) and for some .
Now, we construct . It is the conjunction of sentences expressing the following statements, which can be brought into prenex normal form. In order to improve readability, the construction of the sentences expressing each requirement is left to the reader.

Exactly one atomic proposition is satisfied at each position of each trace.

Every trace is either of type one or of type two.

No two distinct type one traces have the same rank.

For every type one trace of positive rank there exists a type one trace of rank .

There exists a type two trace of the form for some .

For every type two trace there exists a type two trace such that either is final or is a successor of .

For every type two trace there exist two type one traces and such that and are compatible and and are compatible.

In every trace of type two, the letters from in and are equal.
As an example, consider the following instance of PCP
with solution . We encode the solution by the set depicted below (where we drop the suffixes for readability).
Note that contains type one traces while contains type two traces. We claim that satisfies all eight requirement listed above. Requirements 1, 2, 3, and 8 are straightforward to verify. The relation between type one traces specified by Requirement 4 is given by the arrows between the type one traces in . The initial trace as in Requirement 5 is the left most type two trace in and the successor relation on type two traces as in Requirement 6 is indicated by the arrows between the type two traces. The compatible type one traces as in Requirement 7 are given by the arrows from to with the solid arrows denoting the compatible type one traces and the dashed arrows denoting the compatible ones.
After this example, we prove that has the desired properties in general. To this end, fix , which can be encoded in binary with polynomially many bits in .
First, assume there is a solution , i.e., we have , where and are the homomorphisms induced by mapping to and , respectively. We define
and
where
where are the unique indices such that , , and
and, similarly, are the unique indices such that , , and
Intuitively, for every , we pick the pair of words of the instance the th letter of is in, and mark its position correctly in those words.
Traces of are of type one and traces of are of type two. It is then easy to check that Requirements 1 to 8 are satisfied by . Furthermore, as , the size of the is at most . Thus, all words of are of the form with , as required.
Conversely, assume is satisfied by a set of traces. Then, by Requirement 2, we have where is a set of type one traces and is a set of type two traces. Let be the maximal rank of a trace in (which is welldefined as is finite). Then, by Requirements 3 and 4, there exists exactly one trace such that is of rank , for all . Let be such that for all , . Note that as , we must have . Thus, , and .
By Requirements 5 and 6, there exists a sequence of traces such that is a successor of for all , such that for some , and such that is final.
An induction over , using Requirements 6 and 7, shows that the first letter with a bar in is the th letter of and the second one is the th letter of . Requirement 8 ensures that those two letters are always equal. As is final, there exists a prefix of such that and for all , i.e., the two words are equal. As , we therefore obtain a solution to the PCP instance. ∎
As expected, the complexity of the satisfiability problem increases the more traces one has at hand to encode computations. In Theorem 3.1, we have exponentially many; in Theorem 3.2, we have doublyexponentially many. In our last theorem, we consider infinite sets of traces that are finitely representable by finitestate systems. Here, satisfiability becomes intractable, yet still decidable, even when restricted to formulas of temporal depth one.
Formally, a Kripke structure consists of a finite set of states, an initial state , a transition function for all , and a labelling function . A run of is an infinite sequence of states starting with and such that for all . A trace of is the sequence of labels associated to a run of . The set of traces of is denoted by .
Theorem 3.3
The following problem is Towercomplete: Given a HyperLTL sentence and (in binary), does have a model for some Kripke structure with at most states?
Proof
Clarkson et al. presented a modelchecking algorithm for HyperCTL (and thus for HyperLTL, which is a fragment of HyperCTL), and showed that its complexity is a tower of exponentials whose height is the alternation depth of the input sentence [DBLP:conf/post/ClarksonFKMRS14]. Thus, one can enumerate all Kripke structures with at most states (up to isomorphism) and modelcheck them one by one in Tower. This yields the desired upper bound, as there are “only” exponentially many (in ) Kripke structures with states.
The lower bound is obtained by a reduction from the universality problem for starfree regular expressions with complementation. The equivalence problem for those expressions is Towercomplete (under elementary reductions, which is standard for Towercomplete problems), even for twoletter alphabets [DBLP:journals/toct/Schmitz16, DBLP:conf/stoc/StockmeyerM73]. As those expressions are closed by complementation and union, the universality problem is Towercomplete as well.
Starfree expressions with complementation over are generated by the grammar
and have the obvious semantics inducing a language over , denoted by as well.
Let be such an expression. We construct a HyperLTL sentence and a Kripke structure such that is a model of if and only if is universal. does not depend on and is shown in Figure 1. As all sets of variables in are singletons, we indifferently use the notation for the letter and the singleton . The set of traces induced by this Kripke structure is
Given an expression and a trace variable , we inductively define a formula which expresses that when is mapped by a trace assignment to a trace of of the form with , then if and only if .

: No trace assignment satisfies , just as the language of does not contain any word.

: with satisfies if and only if .

: The traces of with an occurrence of are the traces of the form . Thus, with satisfies if and only if is a copy of such a trace with replaced by , i.e., if and only if .

: Similarly to .

.

with
expressing that and are of the form and with and , and with
expressing that and that , where . Thus, satisfies if and only if there exist such that .

.
Although this inductive definition does not necessarily give a formula in prenex normal form, one can easily check that no quantifier is in the scope of a temporal operator, thus the resulting formula can be turned into a HyperLTL formula.
To conclude, consider the sentence , which can again be brought into prenex normal form. Further, note that no temporal operator is in the scope of another one, thus has temporal depth one. The set is a model of if and only if all its traces are in , in , or of the form with . This is the case if and only if all words are in the language of , i.e., if and only if is universal. ∎
As the Kripke structure in the lower bound proof above is fixed, we also obtain a novel hardness result for modelchecking.
Corollary 1
HyperLTL modelchecking a fixed Kripke structure with five states is Towercomplete, even for sentences of temporal depth one.
Note that one could already infer the Towercompleteness of the modelchecking problem by carefully examining the proof of Theorem 5 of [DBLP:conf/post/ClarksonFKMRS14] concerning HyperCTL modelchecking. The reduction from the satisfiability problem for QPTL presented there also works for HyperLTL, albeit with temporal depth larger than one. Interestingly, both reductions use a fixed Kripke structure, meaning in particular that the encoding of has no impact on the asymptotic complexity.
4 Satisfiability for Restricted Classes of Formulas
After studying the HyperLTL satisfiability problem for classes of restricted models, but arbitrary formulas, we now consider restrictions on formulas, but arbitrary models. Recall that Finkbeiner and Hahn presented a complete picture in terms of quantifier prefixes: Satisfiability is PSpacecomplete for the alternationfree fragments and as well as ExpSpacecomplete for . In all other cases, the problem is undecidable, i.e., as soon as there is a single universal quantifier in front of existential ones.
In a sense, the decidable fragments are variants of LTL: Both alternationfree fragments can easily be reduced to LTL satisfiability while the one is easily reducible to the fragment, with an exponential blowup. Thus, the decidable fragments barely exceed the realm of LTL.
In this section, we consider another dimension to measure the complexity of formulas, temporal depth, i.e., we restrict the nesting of temporal operators. The hope is that in this setting, we can obtain decidability for larger quantifier prefix classes. However, a slight adaptation of Finkbeiner and Hahn’s undecidability result for , along with an application of Lemma 1 proven below, already shows undecidability for formulas of temporal depth two and without untils.
Thus, we have to restrict our search to fragments of temporal depth one, which contain most of the information flow policies expressible in HyperLTL [DBLP:conf/post/ClarksonFKMRS14]. And indeed, we prove satisfiability decidable for HyperLTL formulas. Thus, if the temporal depth is one and untils are excluded, then one can allow a universal quantifier in front of existential ones without losing decidability. This fragment includes, for example, the noninference property [DBLP:conf/sp/McLean94].
However, even allowing the smallest possible extension, i.e., adding a second universal quantifier, leads again to undecidability: HyperLTL satisfiability is undecidable for formulas of temporal depth one using only as temporal operator. Thus, satisfiability remains hard, even when severely restricting the temporal depth of formulas. Our results for temporal depth one are summarized in Table 1.
temporal depth one  arbitrary temporal depth  

/  NPcomplete ([DBLP:journals/iandc/DemriS02]+[DBLP:conf/concur/FinkbeinerH16])  PSpacecomplete ([DBLP:conf/concur/FinkbeinerH16]+[Sistla:1985:CPL:3828.3837]) 
NExpTimecomplete (Thm. 4.4)  ExpSpacecomplete ([DBLP:conf/concur/FinkbeinerH16])  
in N2ExpTime (Thm. 
Comments
There are no comments yet.