一句话：提出一种表达力更强的异步超属性逻辑，并在有限状态与下推模型上研究其模型检测复杂度。
超属性模型检测通常需要同时推理多条执行轨迹，而递归程序带来的下推行为与异步观察使问题更难。本文提出一种新的异步超属性逻辑，通过识别轨迹上相关位置的新机制来刻画异步关系。该逻辑比 Bozzelli 等人近期提出的相关逻辑更具表达力，但在有限状态模型上的模型检测复杂度与之相同。作者进一步研究该逻辑在下推模型上的模型检测问题，并论证异步性与非正则模型类的结合是面向递归程序进行超属性模型检测的首个合适途径。
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.
@article{paperbot2662,
title = {Deciding Asynchronous Hyperproperties for Recursive Programs},
author = {Jens Oliver Gutsfeld and Markus Müller-Olm and Christoph Ohrem},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632844}
}