论文标题
确定递归程序的异步超专业
Deciding Asynchronous Hyperproperties for Recursive Programs
论文作者
论文摘要
我们引入了一种新型的逻辑，该逻辑具有异步性超代理，其新机制可以识别痕迹上的相关位置。尽管新逻辑比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.
