Verifying Hyperliveness
Norine Coenen
Hyperliveness describes the class of liveness hyperproperties. Just like for trace properties, that are expressible, e.g., in Linear-time Temporal Logic (LTL), liveness captures that something good eventually has to happen. Hyperproperties are a generalization of trace properties where relations between multiple execution traces can be expressed. This is necessary to formalize information-flow policies like generalized noninterference or the symmetry requirement. Hyperproperties can be expressed in the temporal logic HyperLTL which extends LTL by explicit quantification over trace variables. Verifying hyperproperties has been studied before. In particular, there is an automata-based algorithm for model checking HyperLTL. Unfortunately, its complexity increases exponentially with every quantifier alternation in the formula. Therefore, the only practical tool for model checking HyperLTL, MCHyper, is limited to alternation-free formulas. The alternation-free fragment, however, cannot express hyperliveness properties since these hyperproperties require, in general, a quantifier alternation in the formula. We present a proof technique for model checking HyperLTL that avoids the exponential increase in complexity by shifting the perspective to a game-theoretic view. In our approach, we consider the model-checking problem as a game between the forall-player and the exists-player. The moves of the exists-player are determined by an appropriate strategy, thereby fixing the existentially quantified traces. We have implemented this approach as an extension of the tool MCHyper such that it now can handle formulas with up to one quantifier alternation. Our experimental evaluation shows the practical applicability of the extended version of MCHyper by examining symmetry in mutual exclusion algorithms and checking the cleanness of emission control modules of cars.
Master Thesis.