License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2017.30
URN: urn:nbn:de:0030-drops-70031
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7003/
Go to the corresponding LIPIcs Volume Portal

Finkbeiner, Bernd ; Zimmermann, Martin

The First-Order Logic of Hyperproperties

pdf-format:
LIPIcs-STACS-2017-30.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{finkbeiner_et_al:LIPIcs:2017:7003,
  author =	{Bernd Finkbeiner and Martin Zimmermann},
  title =	{{The First-Order Logic of Hyperproperties}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{30:1--30:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Heribert Vollmer and Brigitte ValleĢe},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7003},
  URN =		{urn:nbn:de:0030-drops-70031},
  doi =		{10.4230/LIPIcs.STACS.2017.30},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, First-order Logic}
}

Keywords: Hyperproperties, Linear Temporal Logic, First-order Logic
Collection: 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)
Issue Date: 2017
Date of publication: 06.03.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI