Model Checking Omega-Regular Hyperproperties with AutoHyperQ
Raven Beutner, Bernd Finkbeiner
Hyperproperties are commonly used to define information-flow policies and other requirements that reason about the relationship between multiple traces in a system. We consider HyperQPTL — a temporal logic for hyperproperties that combines explicit quantification over traces with propositional quantification as, e.g., found in quantified propositional temporal logic (QPTL). HyperQPTL therefore truly captures omega-regular relations on multiple traces within a system. As such, HyperQPTL can, e.g., express promptness properties, which state that there exists a common bound on the number of steps up to which an event must have happened. While HyperQPTL has been studied and used in various prior works, thus far, no model-checking tool for it exists. This paper presents AutoHyperQ, a fully-automatic automata-based model checker for HyperQPTL that can cope with arbitrary combinations of trace and propositional quantification. We evaluate AutoHyperQ on a range of benchmarks and, e.g., use it to analyze promptness requirements in a diverse collection of reactive systems. Moreover, we demonstrate that the core of AutoHyperQ can be reused as an effective tool to translate QPTL formulas into omega-automata.