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.CONCUR.2016.13
URN: urn:nbn:de:0030-drops-61706
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6170/
Go to the corresponding LIPIcs Volume Portal

Finkbeiner, Bernd ; Hahn, Christopher

Deciding Hyperproperties

pdf-format:
LIPIcs-CONCUR-2016-13.pdf (0.5 MB)

Abstract

Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. In this paper, we study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall-formulas, and undecidable for forall-exists-formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.

BibTeX - Entry

@InProceedings{finkbeiner_et_al:LIPIcs:2016:6170,
  author =	{Bernd Finkbeiner and Christopher Hahn},
  title =	{{Deciding Hyperproperties}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{13:1--13:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Jos{\'e}e Desharnais and Radha Jagadeesan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6170},
  URN =		{urn:nbn:de:0030-drops-61706},
  doi =		{10.4230/LIPIcs.CONCUR.2016.13},
  annote =	{Keywords: temporal logics, satisfiability, hyperproperties, complexity}
}

Keywords: temporal logics, satisfiability, hyperproperties, complexity
Collection: 27th International Conference on Concurrency Theory (CONCUR 2016)
Issue Date: 2016
Date of publication: 24.08.2016

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