CISPA
Browse

AutoHyper: Explicit-State Model Checking for HyperLTL

Download (25.49 MB)
conference contribution
posted on 2024-03-25, 13:13 authored by Raven BeutnerRaven Beutner, Bernd FinkbeinerBernd Finkbeiner
HyperLTL is a temporal logic that can express hyperproperties, i.e., properties that relate multiple execution traces of a system. Such properties are becoming increasingly important and naturally occur, e.g., in information-flow control, robustness, mutation testing, path planning, and causality checking. Thus far, complete model checking tools for HyperLTL have been limited to alternation-free formulas, i.e., formulas that use only universal or only existential trace quantification. Properties involving quantifier alternations could only be handled in an incomplete way, i.e., the verification might fail even though the property holds. In this paper, we present AutoHyper, an explicit-state automata-based model checker that supports full HyperLTL and is complete for properties with arbitrary quantifier alternations. We show that language inclusion checks can be integrated into HyperLTL verification, which allows AutoHyper to benefit from a range of existing inclusion-checking tools. We evaluate AutoHyper on a broad set of benchmarks drawn from different areas in the literature and compare it with existing (incomplete) methods for HyperLTL verification.

History

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Tools and Algorithms for Construction and Analysis of Systems (TACAS)

Journal

CoRR

Volume

13993

Page Range

145-163

Publisher

Springer Nature

Open Access Type

  • Hybrid

BibTeX

@inproceedings{Beutner:Finkbeiner:2023, title = "AutoHyper: Explicit-State Model Checking for HyperLTL", author = "Beutner, Raven" AND "Finkbeiner, Bernd", year = 2023, month = 4, journal = "CoRR", pages = "145--163", publisher = "Springer Nature", issn = "1611-3349", doi = "10.1007/978-3-031-30823-9_8" }