Unifying Asynchronous Logics for Hyperproperties
Alberto Bombardelli, Laura Bozzelli, César Sánchez, Stefano Tonetta
TL;DR
The paper introduces $\text{GHyperLTL}_{\textsf{S}+\textsf{C}}$, a generalized linear-time hyperlogic that unifies asynchronous HyperLTL extensions with KLTL-style knowledge modalities and supports past temporal operators and unbounded trace quantification. It defines a decidable fragment, simple $\text{GHyperLTL}_{\textsf{S}+\textsf{C}}$, which strictly extends prior HyperLTL fragments and can express non-regular trace properties on singleton traces; it also embeds KLTL and its single-agent fragment, highlighting broad applicability to diagnosability and information-flow policies. The framework relies on Gamma-relativized stuttering and context modalities, with a precise semantics for pointed trace assignments, enabling expressive specifications under both synchronous and asynchronous perfect recall semantics. The work demonstrates practical relevance through diagnosability and global promptness examples and positions the fragment as a powerful tool for verifying complex hyperproperties in reactive systems. Overall, it advances the theory and practice of asynchronous hyperproperties and epistemic extensions by providing decidable model-checking for a broad, expressive fragment and bridging several existing logics under a common framework.
Abstract
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).