Deciding HyperLTL
Christopher Hahn
Information leakage of a system is an undesirable behaviour, since sensitive data might be open to the public. Building systems that satisfy certain secrecy constraints is a challenging task. To this end, one must be able to write formal specifications of information flow policies. Hyperproperties are a concept to express such policies, e.g. observational determinism. Trace properties, which are a set of possible execution traces, can be formalized in linear temporal logic (LTL). Hyperproperties are a set of trace properties and, hence, establish relations between possible execution traces of a system. HyperLTL is a recently introduced extension of LTL for expressing such hyperproperties in a consistent and compact manner. We consider two satisfiability problems, where the empty model is included and excluded respectively. This thesis solves these and determines every decidable fragment of HyperLTL. We give an algorithm for checking equivalence of formulae from the rich fragment of universally quantified HyperLTL. We also present the minimal fragments of HyperLTL for which these satisfiability problems are undecidable. To conclude this thesis, a prototype satisfiability checker is presented and evaluated, which solves the satisfiability problem for every decidable fragment of HyperLTL and can furthermore solve the question whether two universally quantified HyperLTL formulae are equivalent.
Bachelor Thesis.