Unifying Asynchronous Logics for Hyperproperties

We introduce and investigate a powerful hyper logical framework in the linear-time setting that we call generalized HyperLTL with stuttering and contexts (GHyperLTLS+C for short). GHyperLTLS+C unifies the asynchronous extensions of HyperLTL called HyperLTLS and HyperLTLC, 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 identify a meaningful fragment of GHyperLTLS+C, that we call simple GHyperLTLS+C, 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 GHyperLTLS+C 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 GHyperLTLS+C 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).