Logics for Context-free Hyperproperties

Abstract

We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively, the logic extends visibly pushdown automata by quantification over traces, just like HyperLTL, the most important logic for regular hyperproperties, extends LTL by quantification over traces. We show that model-checking is decidable, provided the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the initial quantifier block. Complementarily, we show that model-checking is undecidable for formulas with a single quantifier alternation, if the stack behavior of the visibly pushdown automaton may depend on the second quantifier block. This also implies that model-checking is undecidable for all fragments with more than one quantifier alternation, provided the stack behavior of the visibly pushdown automaton may depend on a non-initial quantifier block. Finally, we show, using a game-based approach, how to compute explanations for the satisfaction of a formula with one quantifier alternation by a given transition system.