MGHyper: Checking Satisfiability of HyperLTL Formulas beyond the ∃*∀*-Fragment
Tobias Hans
Trace properties are sets of possible execution traces and have been used to describe properties of systems for a long time. But important security policies, like information-flow specifications, which describe how information spreads from inputs to outputs, refer to multiple execution traces of a system and are not expressible as a trace property. Hyperproperties instead are set of trace properties and allow to specify the relation of multiple execution traces. They can be formalized in HyperLTL, an extension of Linear-Time Temporal Logic (LTL) with trace variables and quantification over traces. This thesis considers HyperLTL-Sat, the problem to decide if a given HyperLTL formula is satisfiable by a trace set. It is especially interesting, because it includes checking implications and of HyperLTL formulas. A tool, EAHyper, for checking satisfiability of formulas in the ∃*∀*-fragment, the largest decidable fragment, of HyperLTL already exists. The ∃*∀*-fragment of HyperLTL consists of all formulas with at most one quantifier alternation from existential to universal quantifiers. For all fragments beyond HyperLTL-Sat is in general undecidable. In this thesis we introduce the first semi-decision procedure for all fragments of HyperLTL and prove that deciding HyperLTL formulas is complete for the class of recursive enumerable problems. We also develop a new approach to check satisfiability of formulas in the ∃*∀*-fragment by reducing the problem of deciding HyperLTL formulas to the satisfiability problem for quantified boolean formulas (QBF). We implemented our approach in the tool MGHyper, a model generator for arbitrary HyperLTL formulas and test his performance against different benchmarks. An important application of MGHyper is the construction of counterexamples for claimed implications and equivalences of Hyperproperties formalized in HyperLTL.
Bachelor Thesis.