一句话：系统研究 ∀*∃* HyperLTL 的可满足性片段，并分析其与 LTL 功能规约组合后的可判定性与复杂度。
本文研究具有 ∀*∃* 量词前缀的 HyperLTL 可满足性问题；该问题一般高度不可判定。HyperLTL 可表达关联多条轨迹的超性质，而实际系统性质常与描述单条轨迹功能行为的迹性质结合。作者首先定义 ∀*∃* HyperLTL 的若干安全性与活性片段，并刻画其可满足性问题的复杂度，这些片段通常容易得多。随后将 LTL 迹性质作为功能规约加入；虽然许多情形仍（高度）不可判定，这种将简单 HyperLTL 与任意 LTL 组合的方式也产生了一些新的可判定片段。最后给出一个针对 ∀∃*-HyperLTL 可满足性的新的不完整算法，作为对 ∀*∃* 片段系统研究的补充。
We study satisfiability for HyperLTL with a ∀*∃* quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of ∀*∃* HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining “simple” HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of ∀*∃* fragments is complemented by a new (incomplete) algorithm for ∀∃*-HyperLTL satisfiability.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2205-15138,
title = {Deciding Hyperproperties Combined with Functional Specifications},
author = {Raven Beutner and David Carral and Bernd Finkbeiner and Jana Hofmann and Markus Krötzsch},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533369}
}