Document

# The First-Order Logic of Hyperproperties

## File

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

## Cite As

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.
##### Keywords
• Hyperproperties
• Linear Temporal Logic
• First-order Logic

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## 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.
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.
8. Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical Logic (2. ed.). Undergraduate texts in mathematics. Springer, 1994.
9. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995.
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.
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.
19. Amir Pnueli. The Temporal Logic of Programs. In FOCS 1977, pages 46-57, 1977.
20. Markus N. Rabe. A Temporal Logic Approach to Information-flow Control. PhD thesis, Saarland University, 2016.
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.
X

Feedback for Dagstuhl Publishing

### Thanks for your feedback!

Feedback submitted

### Could not send message

Please try again later or send an E-mail