We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs.

翻译：我们提出了一种用于异步超性质的新型逻辑，该逻辑采用新机制来识别迹上的相关位置。尽管新逻辑比Bozzelli等人近期提出的相关逻辑更具表达能力，但我们在有限状态模型上获得了相同的模型检测问题复杂度。在此基础上，我们进一步研究了该逻辑对下推模型的模型检测问题。本文论证了异步性与非正则模型类相结合的研究路径，首次为递归程序的超性质模型检测提供了切实可行的方案。