Unifying Asynchronous Logics for Hyperproperties
arxiv(2024)
摘要
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).
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要