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 $\forall^*\exists^*$ 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.

翻译：超性质是关联多个执行轨迹的系统性质，在描述信息流和安全策略时普遍存在。诸如HyperLTL的逻辑通过对执行轨迹进行显式量化，以表达反应式系统中的时序超性质——即关于无限执行过程中时序行为的超性质。这类逻辑常伴有一个不受欢迎的副作用：它们以同步方式比较被量化的轨迹，从而无法表达对多条轨迹进行异步比较的性质，例如Zdancewic和Myers的观测确定性、McLean的非推断性质或停顿精化。我们研究异步HyperLTL变体（A-HLTL）的模型检测问题，该时序逻辑能够表达跨时间步比较多条轨迹的超性质。除了对系统轨迹进行量化外，A-HLTL还具备对这些轨迹的停顿进行二次量化的特性。因此，A-HLTL可以简洁地描述许多广泛使用的异步超性质。检测A-HLTL模型需要寻找合适的停顿方式，而迄今为止这仅适用于高度受限的片段或终止系统。本文提出一种基于博弈的新方法，用于验证反应式系统中任意的$\forall^*\exists^*$ A-HLTL公式。在我们的方法中，将验证过程视为验证者与反驳者之间的博弈，双方通过控制底层轨迹和停顿的部分参数相互挑战。验证者的必胜策略对应于存在量化轨迹的具体见证，以及存在量化停顿的异步对齐方案。我们识别了该博弈解释具有完备性的逻辑片段，从而构建出有限状态决策过程。