Document Open Access Logo

The First-Order Logic of Hyperproperties

Authors Bernd Finkbeiner, Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.STACS.2017.30.pdf
  • Filesize: 467 kB
  • 14 pages

Document Identifiers

Author Details

Bernd Finkbeiner
Martin Zimmermann

Cite As Get BibTex

Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 30:1-30:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.STACS.2017.30

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.

Subject Classification

Keywords
  • Hyperproperties
  • Linear Temporal Logic
  • First-order Logic

Metrics

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

References

  1. Shreya Agrawal and Borzoo Bonakdarpour. Runtime verification of k-safety hyperproperties in HyperLTL. In CSF 2016, pages 239-252. IEEE Computer Society, 2016. URL: http://dx.doi.org/10.1109/CSF.2016.24.
  2. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  3. Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In A. M. Pitts, editor, FoSSaCS 2015, volume 9034 of Lecture Notes in Computer Science, pages 167-182. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_11.
  4. 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, POST 2014, 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.
  5. 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.
  6. Rina S. Cohen and Arie Y. Gold. Theory of omega-languages. I. characterizations of omega-context-free languages. Journal of Computer and System Sciences, 15(2):169-184, 1977. URL: http://dx.doi.org/10.1016/S0022-0000(77)80004-4.
  7. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science. Cambridge University Press, 2016. Google Scholar
  8. Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical Logic (2. ed.). Undergraduate texts in mathematics. Springer, 1994. Google Scholar
  9. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. Google Scholar
  10. Bernd Finkbeiner. Synthesis of reactive systems. In Javier Esparza, Orna Grumberg, and Salomon Sickert, editors, Dependable Software Systems Engineering, volume 45 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 72-98. IOS Press, 2016. URL: http://dx.doi.org/10.3233/978-1-61499-627-9-72.
  11. Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In Josée Desharnais and Radha Jagadeesan, editors, CONCUR 2016, volume 59 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  12. 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, CAV 2015 (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.
  13. Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. arXiv, 1610.04388, 2016. URL: http://arxiv.org/abs/1610.04388.
  14. Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal basis of fairness. In Paul W. Abrahams, Richard J. Lipton, and Stephen R. Bourne, editors, POPL 1980, pages 163-173. ACM Press, 1980. URL: http://dx.doi.org/10.1145/567446.567462.
  15. Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. Finite Model Theory and Its Applications. Springer, 2005. Google Scholar
  16. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, and Victor Vianu. On the unusual effectiveness of logic in computer science. Bulletin of Symbolic Logic, 7(2):213-236, 2001. URL: http://dx.doi.org/10.2307/2687775.
  17. Klaus Havelund and Grigore Rosu. Efficient monitoring of safety properties. International Journal on Software Tools for Technology Transfer, 6(2):158-173, 2004. URL: http://dx.doi.org/10.1007/s10009-003-0117-6.
  18. Hans W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los Angeles, USA, 1968. Google Scholar
  19. Amir Pnueli. The Temporal Logic of Programs. In FOCS 1977, pages 46-57, 1977. Google Scholar
  20. Markus N. Rabe. A Temporal Logic Approach to Information-flow Control. PhD thesis, Saarland University, 2016. Google Scholar
  21. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. URL: http://dx.doi.org/10.1145/3828.3837.
  22. Wolfgang Thomas. Languages, automata, and logic. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Vol. 3, pages 389-455. Springer, 1997. URL: http://dx.doi.org/10.1007/978-3-642-59126-6.
  23. Wolfgang Thomas. Path logics with synchronization. In Kamal Lodaya, Madhavan Mukund, and R. Ramanujam, editors, Perspectives in Concurrency Theory, pages 469-481. IARCS-Universities, Universities Press, 2009. Google Scholar
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