Deciding Hyperproperties Combined with Functional Specifications

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

  • Raven Beutner - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • David Carral - , Université de Montpellier (Autor:in)
  • Bernd Finkbeiner - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Jana Hofmann - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Markus Krötzsch - , Professur für Wissensbasierte Systeme (cfaed) (Autor:in)

Abstract

We study satisfability for HyperLTL with a ?*?* quantifer prefx, 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 frst defne several safety and liveness fragments of ?*?* HyperLTL, and characterize the complexity of their (often much easier) satisfability problem. We then add LTL trace properties as functional specifcations. 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 satisfability.

Details

OriginalspracheEnglisch
TitelProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)
Redakteure/-innenChristel Baier, Dana Fisman
Herausgeber (Verlag)ACM Press
Seiten56:1–56:13
ISBN (elektronisch)9781450393515
ISBN (Print)978-1-4503-9351-5
PublikationsstatusVeröffentlicht - 2 Aug. 2022
Peer-Review-StatusJa

Externe IDs

Scopus 85132141560

Schlagworte

ASJC Scopus Sachgebiete

Schlagwörter

  • HyperLTL, Hyperproperties, Satisfability