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）。该框架统一了HyperLTL的已知异步扩展，以及LTL在同步与异步完美回忆语义下带有知识模态的著名扩展KLTL。作为主要贡献，我们识别出GHyperLTL_SC的一个有意义片段——称为简单GHyperLTL_SC，其模型检测问题是可判定的，且表达能力超越HyperLTL及已知具有可判定模型检测问题的HyperLTL异步扩展片段。简单GHyperLTL_SC在同步语义下包含KLTL，在异步语义下包含KLTL的单智能体片段；据我们所知，这是唯一能在单轨迹集上表达强大非正则轨迹性质且具有可判定模型检测问题的超逻辑。我们通过证明简单GHyperLTL_SC能表达可诊断性性质、同步与异步设定下的重要信息流安全策略类，以及有界终止性（更广义地说，Prompt LTL风格的全局即时性），论证了该片段的实际意义。