HyperLTL Synthesis

Philip Lukert

Ensuring secure information flow in privacy critical systems is an important aspect in system design. An example of such an information flow policy is observational determinism, which ensures that two traces with the same observable input have the same observable output. The temporal logic HyperLTL is designed to specify such properties by extending LTL with explicit trace quantification. Therefore, a HyperLTL formula defines a set of sets of traces instead of a single set of traces. Current work focuses on monitoring and model checking of a HyperLTL formula on a given system. In this work, we study the synthesis problem of HyperLTL. Synthesis is to directly generate a system from a given specification with no need for manual implementation, monitoring or model checking. In general, the synthesis problem of HyperLTL is undecidable. In this thesis, we show that the synthesis problem of the existential fragment (using solely existential quantifiers) is equivalent to the satisfiability problem of HyperLTL and is, therefore, fully decidable. We also give a decidable sub-fragment of the universal fragment as the whole universal fragment turns out to be undecidable. Further, we give a undecidability proof for universal formulas in general. Furthermore, we proof the undecidability of the synthesis problem for formulas with a quantifier alternation from universal to existential by a reduction from Post’s Correspondence Problem (PCP).

Bachelor Thesis.

(pdf)