2026-08-04T06:27:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22203 2024-12-05T15:18:03Z ddc:004 open_access

Unifying Asynchronous Logics for Hyperproperties Bombardelli, Alberto Bozzelli, Laura Sánchez, César Tonetta, Stefano Asynchronous hyperproperties Temporal logics for hyperproperties Expressiveness Decidability Model checking We introduce and investigate a powerful hyper logical framework in the linear-time setting that we call generalized HyperLTL with stuttering and contexts (GHyperLTL_{S+C}} for short). GHyperLTL_{S+C} unifies the asynchronous extensions of HyperLTL called HyperLTL_S and HyperLTL_C, 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 GHyperLTL_{S+C}, that we call simple GHyperLTL_{S+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 GHyperLTL_{S+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 GHyperLTL_{S+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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alberto Bombardelli and Laura Bozzelli and César Sánchez and Stefano Tonetta 2024 Is Part Of LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2024.14 urn:nbn:de:0030-drops-222034 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.14 eng https://creativecommons.org/licenses/by/4.0/legalcode