We study satisfiability for HyperLTL with a ∀*∃* quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of ∀*∃* HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining “simple” HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of ∀*∃* fragments is complemented by a new (incomplete) algorithm for ∀∃*-HyperLTL satisfiability.
%0 Conference Paper
%1 Beutner2022
%A Beutner, Raven
%A Carral, David
%A Finkbeiner, Bernd
%A Hofmann, Jana
%A Krötzsch, Markus
%B Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
%C New York, NY, USA
%D 2022
%I Association for Computing Machinery
%K imported xack
%P 1–13
%R 10.1145/3531130.3533369
%T Deciding Hyperproperties Combined with Functional Specifications
%U https://doi.org/10.1145/3531130.3533369
%X We study satisfiability for HyperLTL with a ∀*∃* quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of ∀*∃* HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining “simple” HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of ∀*∃* fragments is complemented by a new (incomplete) algorithm for ∀∃*-HyperLTL satisfiability.
%@ 9781450393515
@inproceedings{Beutner2022,
abstract = {We study satisfiability for HyperLTL with a ∀*∃* quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of ∀*∃* HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining “simple” HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of ∀*∃* fragments is complemented by a new (incomplete) algorithm for ∀∃*-HyperLTL satisfiability.},
added-at = {2025-01-06T12:49:52.000+0100},
address = {New York, NY, USA},
author = {Beutner, Raven and Carral, David and Finkbeiner, Bernd and Hofmann, Jana and Krötzsch, Markus},
biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/20d3455354bb4e11ee4537fba6c940b2b/scadsfct},
booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
day = 4,
doi = {10.1145/3531130.3533369},
interhash = {d33ff28c53e1d3dba6a5e62cb184f561},
intrahash = {0d3455354bb4e11ee4537fba6c940b2b},
isbn = {9781450393515},
keywords = {imported xack},
location = {Haifa, Israel},
month = {8},
pages = {1–13},
publisher = {Association for Computing Machinery},
series = {LICS '22},
timestamp = {2025-02-05T15:11:48.000+0100},
title = {Deciding Hyperproperties Combined with Functional Specifications},
url = {https://doi.org/10.1145/3531130.3533369},
year = 2022
}
