{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:21:34Z","timestamp":1770290494139,"version":"3.49.0"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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 \u2013 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 \u03c9-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 \u03c9-automata.<\/jats:p>","DOI":"10.29007\/1xjt","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:10Z","timestamp":1685830210000},"page":"23-9","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Omega-Regular Hyperproperties with AutoHyperQ"],"prefix":"10.29007","volume":"94","author":[{"given":"Raven","family":"Beutner","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:13Z","timestamp":1685830213000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/d1VW"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/1xjt","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}