Model_Checking_Omega-Regular_Hyperproperties_with_AutoHyperQ.pdf (558.28 kB)

Model Checking Omega-Regular Hyperproperties with AutoHyperQ

Download (558.28 kB)
conference contribution
posted on 2024-04-24, 13:01 authored by Raven BeutnerRaven Beutner, Bernd FinkbeinerBernd Finkbeiner
Hyperproperties are commonly used to define information-flow policies and other re- quirements that reason about the relationship between multiple traces in a system. We consider HyperQPTL – a temporal logic for hyperproperties that combines explicit quan- tification over traces with propositional quantification as, e.g., found in quantified proposi- tional temporal logic (QPTL). HyperQPTL therefore truly captures ω-regular relations on multiple traces within a system. As such, HyperQPTL can, e.g., express promptness prop- erties, 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 ω-automata.


Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)


EPiC series in computing



Page Range




Open Access Type

  • Unknown


@inproceedings{Beutner:Finkbeiner:2023, title = "Model Checking Omega-Regular Hyperproperties with AutoHyperQ", author = "Beutner, Raven" AND "Finkbeiner, Bernd", year = 2023, month = 6, journal = "EPiC series in computing", pages = "23--29", publisher = "EasyChair", issn = "2398-7340", doi = "10.29007/1xjt" }