File(s) not publicly available

A Temporal Logic for Asynchronous Hyperproperties

conference contribution
posted on 2023-11-29, 18:17 authored by Jan BaumeisterJan Baumeister, Norine CoenenNorine Coenen, Borzoo Bonakdarpour, Bernd FinkbeinerBernd Finkbeiner, César Sánchez
Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.


Preferred Citation

Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner and César Sánchez. A Temporal Logic for Asynchronous Hyperproperties. In: Computer Aided Verification (CAV). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date


Open Access Type

  • Green


@inproceedings{cispa_all_3480, title = "A Temporal Logic for Asynchronous Hyperproperties", author = "Baumeister, Jan and Coenen, Norine and Bonakdarpour, Borzoo and Finkbeiner, Bernd and Sánchez, César", booktitle="{Computer Aided Verification (CAV)}", year="2021", }

Usage metrics


    No categories selected



    Ref. manager