We introduce and investigate a powerful hyper logical framework in the linear-time setting, we call generalized HyperLTL with stuttering and contexts (GHyperLTL_SC for short). GHyperLTL_SC unifies known asynchronous extensions of HyperLTL and the well-known extension KLTL of LTL with knowledge modalities under both the synchronous and asynchronous perfect recall semantics. As a main contribution, we individuate a meaningful fragment of GHyperLTL_SC, we call simple GHyperLTL_SC, with a decidable model-checking problem, which is more expressive than HyperLTL and known fragments of asynchronous extensions of HyperLTL with a decidable model-checking problem. Simple GHyperLTL_SC subsumes KLTL under the synchronous semantics and the one-agent fragment of KLTL under the asynchronous semantics, and to the best of our knowledge, it represents the unique hyper logic with a decidable model-checking problem which can express powerful non-regular trace properties when interpreted on singleton sets of traces. We justify the relevance of simple GHyperLTL_SC by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt LTL).

翻译：我们提出并研究了一种在线性时态设置下的强大超逻辑框架，称为带停顿与上下文的广义HyperLTL（简称GHyperLTL_SC）。GHyperLTL_SC统一了HyperLTL的已知异步扩展，以及经典的一阶时态逻辑KLTL（带知识模态的LTL扩展）在同步与异步完美回忆语义下的表述。作为主要贡献，我们识别出GHyperLTL_SC的一个有意义片段，称为简单GHyperLTL_SC，其模型检测问题可判定，且表达能力超越HyperLTL及已知可判定模型检测问题的HyperLTL异步扩展片段。简单GHyperLTL_SC包含了同步语义下的完整KLTL以及异步语义下的单智能体KLTL片段；据我们所知，它是唯一能表达强大非正则迹属性且在单迹集上解释时仍保持模型检测可判定性的超逻辑。我们通过展示简单GHyperLTL_SC可表达同步与异步场景下的可诊断性属性、有趣的信息流安全策略类，以及有界终止性（更一般地，Prompt LTL风格的全局即时性），论证了其实际相关性。