The first-order logic of hyperproperties

DOI10.4230/LIPICS.STACS.2017.30MaRDI QIDQ4636628zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Martín G. Zimmermann

Publication date 19 April 2018

Full work available at URL https://arxiv.org/abs/1610.04388

zbMATH Keywords

first-order logichyperpropertieslinear temporal logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Temporal logic (03B44) Logic in computer science (03B70)

Abstract: We investigate the logical foundations of hyperproperties. Hyperproperties generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. In this paper, we establish the first connection between temporal logics for hyperproperties and first-order logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that linear-time temporal logic (LTL) is expressively equivalent to first-order logic over the natural numbers with order. We introduce first-order logic over sets of traces and prove that HyperLTL, the extension of LTL to hyperproperties, is strictly subsumed by this logic. We furthermore exhibit a fragment that is expressively equivalent to HyperLTL, thereby establishing Kamp's theorem for hyperproperties.

Recommendations

• Temporal hyperproperties
• A temporal logic for asynchronous hyperproperties
• Flavors of sequential information flow
• Model checking algorithms for hyperproperties (invited paper)
• Synthesis from hyperproperties

Cited in

(28)

• On the expressive power of TeamLTL and first-order team logic over hyperproperties
• Flavors of sequential information flow
• On the complexity of linear temporal logic with team semantics
• Model checking algorithms for hyperproperties (invited paper)
• Compositional model checking for multi-properties
• Whither specifications as programs
• Synthesis from hyperproperties
• Unifying hyper and epistemic temporal logics
• Temporal hyperproperties
• Team semantics for the specification and verification of hyperproperties
• Good-for-Game QPTL: An Alternating Hodges Semantics
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Realizable and context-free hyperlanguages
• Explaining Hyperproperty Violations
• Second-order hyperproperties
• A remark on the expressivity of asynchronous TeamLTL and HyperLTL
• Temporal team semantics revisited
• Deciding hyperproperties combined with functional specifications
• The hierarchy of hyperlogics
• The complexity of second-order HyperLTL
• Centralized vs. decentralized monitors for hyperproperties
• Explainability requirements as hyperproperties
• HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder
• The complexity of second-order HyperLTL
• Unifying asynchronous logics for hyperproperties
• Expressivity of asynchronous TeamLTL and HyperLTL
• Extensions of HyperLTL for asynchronous hyperproperties
• A temporal logic for asynchronous hyperproperties

This page was built for publication: The first-order logic of hyperproperties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4636628)