File(s) not publicly available

Verifying Hyperliveness

conference contribution
posted on 2023-11-29, 18:11 authored by Norine CoenenNorine Coenen, Bernd FinkbeinerBernd Finkbeiner, Cesar Sanchez, Leander Tentrup
yperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can express information flow policies as well as properties like symmetry in mutual exclusion algorithms or Hamming distances in error-resistant transmission protocols. Previous work on HyperLTL model checking has focussed on the alternation-free fragment of HyperLTL, where verification reduces to checking a standard trace property over an appropriate self-composition of the system. The alternation-free fragment does, however, not cover general hyperliveness properties. Universal formulas, for example, cannot express the secrecy requirement that for every possible value of a secret variable there exists a computation where the value is different while the observations made by the external observer are the same. In this paper, we study the more difficult case of hyperliveness properties expressed as HyperLTL formulas with quantifier alternation. We reduce existential quantification to strategic choice and show that synthesis algorithms can be used to eliminate the existential quantifiers automatically. We furthermore show that this approach can be extended to reactive system synthesis, i.e., to automatically construct a reactive system that is guaranteed to satisfy a given HyperLTL formula.


Preferred Citation

Norine Coenen, Bernd Finkbeiner, Cesar Sanchez and Leander Tentrup. Verifying Hyperliveness. In: Computer Aided Verification (CAV). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date


Open Access Type

  • Unknown


@inproceedings{cispa_all_3076, title = "Verifying Hyperliveness", author = "Coenen, Norine and Finkbeiner, Bernd and Sanchez, Cesar and Tentrup, Leander", booktitle="{Computer Aided Verification (CAV)}", year="2019", }

Usage metrics


    No categories selected


    Ref. manager