Verifying hyperliveness

DOI10.1007/978-3-030-25540-4_7MaRDI QIDQ6154578zbMATH OpenFDO

Authors Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2005.07425

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Abstract: HyperLTL 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.

Recommendations

• AutoHyper: explicit-state model checking for HyperLTL
• Synthesis from hyperproperties
• Temporal hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL^*
• Synthesizing reactive systems from hyperproperties

Cited in

(21)

• Program Repair for Hyperproperties
• A temporal logic for asynchronous hyperproperties
• Constraint-based relational verification
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Model checking algorithms for hyperproperties (invited paper)
• Software Verification of Hyperproperties Beyond k-Safety
• Finite-word hyperlanguages
• Efficient loop conditions for bounded model checking hyperproperties
• Parameter synthesis for probabilistic hyperproperties
• Cartesian reachability logic: a language-parametric logic for verifying k-safety properties
• Model checking omega-regular hyperproperties with AutoHyperQ
• Explaining Hyperproperty Violations
• Runtime enforcement of hyperproperties
• AutoHyper: explicit-state model checking for HyperLTL
• Bounded model checking for asynchronous hyperproperties
• HyperPCTL model checking by probabilistic decomposition
• Stack-aware hyperproperties
• Asynchronous extensions of hyperLTL
• Symbolic execution for refuting hyperproperties
• Second-order hyperproperties
• Predicate abstraction for hyperliveness verification

This page was built for publication: Verifying hyperliveness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154578)