Deciding Hyperproperties Combined with Functional Specifications

(2022) Deciding Hyperproperties Combined with Functional Specifications. (In Press)

Text main_lics.pdf Restricted to Registered users only Download (711kB) | Request a copy

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 algorithm for ∀∃ ∗ -HyperLTL satisfiability, which is incomplete but often successful.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Bernd Finkbeiner (Reactive Systems Group, RSG)
Conference:	LICS IEEE Symposium on Logic in Computer Science
Depositing User:	Jana Hofmann
Date Deposited:	09 May 2022 16:13
Last Modified:	09 May 2022 16:13
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/3666

Actions

Actions (login required)

View Item