A Proof System for HyperLTL
Norine Coenen
HyperLTL is a temporal logic defined as an extension of the well known Linear-time temporal logic (LTL). In LTL it is possible to express properties of single execution traces of a system. This is the reason why LTL is commonly used as the specification language for verification and synthesis tools. Synthesis describes the problem of finding a system that guarantees to satisfy the specification provided as an LTL formula whereas in verification it is checked whether every possible execution trace of a given system fulfills the specification. Both techniques aim to prove systems correct which is highly desirable especially in security relevant scenarios. Although LTL formulas do implicitly reference all paths of a system it is not possible to specify relations between multiple paths explicitly. However, there are some interesting properties like noninterference and observational determinism that are only expressible if several paths can be referenced independently. Properties requiring this additional power are also called hyperproperties. Many interesting information flow security policies belong for instance to the set of hyperproperties. HyperLTL is obtained from LTL by adding explicit path quantifiers. This already allows the expression of many interesting hyperproperties. In this thesis we will develop a deductive proof system for the forall-star, the exists-star and the forall-star exists-star fragments of HyperLTL based on the proof systems of CTL-star and ATL. This will make it possible to prove HyperLTL properties of general infinite-state systems, which are beyond the scope of current model checking techniques. Moreover, we will prove that the proof system is sound and for finite-state systems we will achieve relative completeness.
Bachelor Thesis.