Document Open Access Logo

Deciding Hyperproperties

Authors Bernd Finkbeiner, Christopher Hahn

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.13.pdf
  • Filesize: 477 kB
  • 14 pages

Document Identifiers

Author Details

Bernd Finkbeiner
Christopher Hahn

Cite As Get BibTex

Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.13

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.

Subject Classification

Keywords
  • temporal logics
  • satisfiability
  • hyperproperties
  • complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Rajeev Alur, Pavol Cerný, and Steve Zdancewic. Preserving secrecy under refinement. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, volume 4052 of Lecture Notes in Computer Science, pages 107-118. Springer, 2006. URL: http://dx.doi.org/10.1007/11787006_10.
  2. Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. Secure information flow by self-composition. In 17th IEEE Computer Security Foundations Workshop, CSFW-17 2004, 28-30 June 2004, Pacific Grove, CA, USA, pages 100-114. IEEE Computer Society, 2004. URL: http://dx.doi.org/10.1109/CSFW.2004.17.
  3. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8414 of Lecture Notes in Computer Science, pages 265-284. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54792-8_15.
  4. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: http://dx.doi.org/10.3233/JCS-2009-0393.
  5. Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. CoRR, abs/1606.07047, 2016. URL: http://arxiv.org/abs/1606.07047.
  6. Bernd Finkbeiner and Markus N. Rabe. The linear-hyper-branching spectrum of temporal logics. it - Information Technology, 56(6):273-279, 2014. URL: http://www.degruyter.com/view/j/itit.2014.56.issue-6/itit-2014-1067/itit-2014-1067.xml.
  7. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking HyperLTL and HyperCTL^*. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 30-48. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21690-4_3.
  8. Orna Kupferman and Moshe Vardi. Synthesis with incomplete informatio. In Advances in Temporal Logic, pages 109-127. Springer, 2000. Google Scholar
  9. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  10. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II, pages 746-757. IEEE Computer Society, 1990. URL: http://dx.doi.org/10.1109/FSCS.1990.89597.
  11. Emil L Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52(4):264-268, 1946. Google Scholar
  12. Markus N. Rabe. A Temporal Logic Approach to Information-flow Control. PhD thesis, Saarland University, 2016. Google Scholar
  13. A. W. Roscoe. CSP and determinism in security modelling. In Proceedings of the 1995 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 8-10, 1995, pages 114-127. IEEE Computer Society, 1995. URL: http://dx.doi.org/10.1109/SECPRI.1995.398927.
  14. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: http://dx.doi.org/10.1145/3828.3837.
  15. Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1092.
  16. Steve Zdancewic and Andrew C. Myers. Observational determinism for concurrent program security. In 16th IEEE Computer Security Foundations Workshop, CSFW-16 2003, 30 June - 2 July 2003, Pacific Grove, CA, USA, page 29. IEEE Computer Society, 2003. URL: http://dx.doi.org/10.1109/CSFW.2003.1212703.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact