Unifying Asynchronous Logics for Hyperproperties

Abstract

We introduce and investigate a powerful hyper logical framework in the linear-time setting that we call generalized HLTL with stuttering and contexts (GHLTL for short). GHLTL unifies the asynchronous extensions of HLTL called SHLTL and CHLTL, 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 GHLTL, that we call simple GHLTL, with a decidable model-checking problem, which is more expressive than HLTL and known fragments of asynchronous extensions of HLTL with a decidable model-checking problem. Simple GHLTL 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 GHLTL 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).

Publication
Proc. of the 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'24), pp. 14:1-14:18, LIPIcs vol 323, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2024
César Sánchez
César Sánchez
Professor

My research focuses on formal methods, in paricular logic, automata and game theory. Temporal logics for Hyperproperties. Reactive Synthesis Modulo Theories. Applications to Blockchain.