Deciding Hyperproperties Combined with Functional Specifications

Raven BeutnerRaven Beutner, David CarralDavid Carral, Bernd FinkbeinerBernd Finkbeiner, Jana HofmannJana Hofmann, Markus KrötzschMarkus Krötzsch

Raven Beutner, David Carral, Bernd Finkbeiner, Jana Hofmann, Markus Krötzsch
Deciding Hyperproperties Combined with Functional Specifications
In Christel Baier and Dana Fisman, eds., Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), 56:1--56:13, 2022. ACM

Details
Bibtex

KurzfassungAbstract
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 algorithm for ∀∃*-HyperLTL satisfiability, which is incomplete but often successful.
Weitere Informationen unter:Further Information: Link
Projekt:Project: CPEC
Forschungsgruppe:Research Group: Wissensbasierte SystemeKnowledge-Based Systems

@inproceedings{BCFHK2022,
  author    = {Raven Beutner and David Carral and Bernd Finkbeiner and Jana
               Hofmann and Markus Kr{\"{o}}tzsch},
  title     = {Deciding Hyperproperties Combined with Functional Specifications},
  editor    = {Christel Baier and Dana Fisman},
  booktitle = {Proceedings of the 37th Annual {ACM/IEEE} Symposium on Logic in
               Computer Science (LICS 2022)},
  publisher = {ACM},
  year      = {2022},
  pages     = {56:1--56:13},
  doi       = {10.1145/3531130.3533369}
}