一句话：提出博弈式方法验证反应式系统中的任意 ∀*∃* 异步 HyperLTL 公式，并给出有限状态判定片段与原型实现。
HyperLTL 等超属性逻辑对量化迹进行同步比较，因而无法表达需要跨时间步异步比较的异步超属性，如 observational determinism、non-inference 和 stuttering refinement。A-HLTL 通过额外量化迹的 stuttering 来简洁描述这类性质，但其模型检测需寻找合适 stuttering，此前仅对很受限片段或终止系统可行。本文针对反应式系统中的任意 ∀*∃* A-HLTL 公式提出博弈式验证方法：verifier 与 refuter 分别控制迹和 stuttering 的部分，verifier 的获胜策略对应存在量化迹的见证及异步对齐。作者识别出博弈解释完备的片段，从而得到有限状态判定过程；并实现有限状态原型，实验结果表明方法有效。
Hyperproperties are system properties that relate multiple execution traces and commonly occur when specifying information-flow and security policies. Logics like HyperLTL utilize explicit quantification over execution traces to express temporal hyperproperties in reactive systems, i.e., hyperproperties that reason about the temporal behavior along infinite executions. An often unwanted side-effect of such logics is that they compare the quantified traces synchronously . This prohibits the logics from expressing properties that compare multiple traces asynchronously, such as Zdancewic and Myers’s observational determinism , McLean’s non-inference , or stuttering refinement . We study the model-checking problem for a variant of asynchronous HyperLTL (A-HLTL), a temporal logic that can express hyperproperties where multiple traces are compared across timesteps. In addition to quantifying over system traces, A-HLTL features secondary quantification over stutterings of these traces. Consequently, A-HLTL allows for a succinct specification of many widely used asynchronous hyperproperties. Model-checking A-HLTL requires finding suitable stutterings, which, thus far, has been only possible for very restricted fragments or terminating systems. In this paper, we propose a novel game-based approach for the verification of arbitrary ∀ ∗ ∃ ∗ A-HLTL formulas in reactive systems. In our method, we consider the verification as a game played between a verifier and a refuter, who challenge each other by controlling parts of the underlying traces and stutterings. A winning strategy for the verifier then corresponds to concrete witnesses for existentially quantified traces and asynchronous alignments for existentially quantified stutterings. We identify fragments for which our game-based interpretation is complete and thus constitutes a finite-state decision procedure. We contribute a prototype implementation for finite-state systems and report on encouraging experimental results.
@article{paperbot2942,
title = {Verifying Asynchronous Hyperproperties in Reactive Systems},
author = {Raven Beutner and Bernd Finkbeiner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763130}
}