Asynchronous Extensions of HyperLTL
Laura Bozzelli, Adriano Peron, Cesar Sanchez

TL;DR
This paper introduces two asynchronous extensions of HyperLTL, expanding its expressiveness for asynchronous hyperproperties, and identifies decidable fragments with known complexity, advancing formal verification methods.
Contribution
The paper proposes HyperLTLS and HyperLTLC, two asynchronous extensions of HyperLTL, and characterizes their decidable fragments and computational complexity.
Findings
Model checking for the extensions is generally undecidable.
Decidable fragments subsume HyperLTL and are practically expressive.
HyperLTLS fragment has the same complexity as HyperLTL.
Abstract
Hyperproperties are a modern specification paradigm that extends trace properties to express properties of sets of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this paper, we introduce two asynchronous and orthogonal extensions of HyperLTL, namely Stuttering HyperLTL (HyperLTLS) and Context HyperLTL (HyperLTLC). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
