Document Open Access Logo

Team Semantics for the Specification and Verification of Hyperproperties

Authors Andreas Krebs, Arne Meier , Jonni Virtema , Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2018.10.pdf
  • Filesize: 477 kB
  • 16 pages

Document Identifiers

Author Details

Andreas Krebs
  • Universität Tübingen, Wilhelm-Schickard-Institut für Informatik, Tübingen, Germany
Arne Meier
  • Leibniz Universität Hannover, Institut für Theoretische Informatik, Hannover, Germany
Jonni Virtema
  • Hasselt University, Databases and Theoretical Computer Science Group, Diepenbeek, Belgium
Martin Zimmermann
  • Saarland University, Reactive Systems Group, Saarbrücken, Germany

Funding

  • Meier, Arne: Funded by the German Research Foundation DFG, project ME 4279/1-2.
  • Zimmermann, Martin: Funded by the German Research Foundation DFG, project "TriCS" (ZI 1516/1-1).

Cite As Get BibTex

Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.MFCS.2018.10

Abstract

We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • LTL
  • Hyperproperties
  • Team Semantics
  • Model Checking
  • Satisfiability

Metrics

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

Related Versions

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  2. Borzoo Bonakdarpour and Bernd Finkbeiner. Runtime verification for HyperLTL. In Yliès Falcone and César Sánchez, editors, RV 2016, volume 10012 of LNCS, pages 41-45. Springer, 2016. Google Scholar
  3. Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In Andrew M. Pitts, editor, FoSSaCS 2015, volume 9034 of LNCS, pages 167-182. Springer, 2015. Google Scholar
  4. Julian Bradfield. On the structure of events in boolean games. In Logics for Dependence and Independence. Dagstuhl Reports, 2015. Google Scholar
  5. 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 LNCS, pages 265-284. Springer, 2014. Google Scholar
  6. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. Google Scholar
  7. Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, and Holger Hermanns. Is your software on dope? - formal analysis of surreptitiously "enhanced" programs. In Hongseok Yang, editor, ESOP 2017, volume 10201 of LNCS, pages 83-110. Springer, 2017. Google Scholar
  8. Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, and Jonni Virtema. Approximation and dependence via multiteam semantics. In FoIKS 2016, pages 271-291, 2016. Google Scholar
  9. Arnaud Durand, Juha Kontinen, and Heribert Vollmer. Expressivity and complexity of dependence logic. In Dependence Logic: Theory and Applications, pages 5-32. Birkhäuser, 2016. Google Scholar
  10. 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, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  11. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. In Shuvendu K. Lahiri and Giles Reger, editors, RV 2017, volume 10548 of LNCS, pages 190-207. Springer, 2017. Google Scholar
  12. Bernd Finkbeiner, Christian Müller, Helmut Seidl, and Eugen Zalinescu. Verifying security policies in multi-agent workflows with loops. In Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu, editors, CCS 2017, pages 633-645. ACM, 2017. URL: http://dx.doi.org/10.1145/3133956.
  13. 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 LNCS, pages 30-48. Springer, 2015. Google Scholar
  14. Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. In Heribert Vollmer and Brigitte Vallée, editors, STACS 2017, volume 66 of LIPIcs, pages 30:1-30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  15. Pietro Galliani. Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Ann. Pure Appl. Logic, 163(1):68-84, 2012. Google Scholar
  16. Erich Grädel, Juha Kontinen, Jouko Väänänen, and Heribert Vollmer. Logics for dependence and independence (Dagstuhl seminar 15261). Dagstuhl Reports, 5(6):70-85, 2015. Google Scholar
  17. Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399-410, 2013. Google Scholar
  18. Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of propositional logics in team semantic. ACM Trans. Comput. Logic, 19(1):2:1-2:14, 2018. Google Scholar
  19. Wilfrid Hodges. Compositional semantics for a language of imperfect information. Logic Journal of the IGPL, 5(4):539-563, 1997. Google Scholar
  20. Andreas Krebs, Arne Meier, and Jonni Virtema. A team based variant of CTL. In Fabio Grandi, Martin Lange, and Alessio Lomuscio, editors, TIME 2015, pages 140-149. IEEE Computer Society, 2015. Google Scholar
  21. Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team semantics for the specification and verification of hyperproperties. CoRR, abs/1709.08510, 2017. URL: http://arxiv.org/abs/1709.08510.
  22. Lars Kuhtz. Model checking finite paths and trees. PhD thesis, Saarland University, 2010. Google Scholar
  23. Lars Kuhtz and Bernd Finkbeiner. LTL path checking is efficiently parallelizable. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, ICALP 2009 (Part II), volume 5556 of LNCS, pages 235-246. Springer, 2009. Google Scholar
  24. Antti Kuusisto. A Double Team Semantics for Generalized Quantifiers. Journal of Logic, Language and Information, 24(2):149-191, 2015. Google Scholar
  25. Richard Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6(3):467-480, 1977. Google Scholar
  26. Nicolas Markey and Philippe Schnoebelen. Model checking a path. In Roberto M. Amadio and Denis Lugiez, editors, CONCUR 2003, volume 2761 of LNCS, pages 248-262. Springer, 2003. Google Scholar
  27. Julian-Steffen Müller. Satisfiability and Model Checking in Team Based Logics. PhD thesis, Leibniz University of Hannover, 2014. Google Scholar
  28. Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE Computer Society, 1977. Google Scholar
  29. Markus N. Rabe. A Temporal Logic Approach to Information-flow Control. PhD thesis, Saarland University, 2016. Google Scholar
  30. Ilya Shpitser. Causal inference and logics of dependence and independence. In Logics for Dependence and Independence. Dagstuhl Reports, 2015. Google Scholar
  31. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. Google Scholar
  32. Jouko Väänänen. Dependence Logic. Cambridge University Press, 2007. Google Scholar
  33. Jouko Väänänen. Modal Dependence Logic. In New Perspectives on Games and Interaction. Amsterdam University Press, Amsterdam, 2008. Google Scholar
  34. Jonni Virtema. Complexity of validity for propositional dependence logics. Inf. Comput., 253:224-236, 2017. URL: http://dx.doi.org/10.1016/j.ic.2016.07.008.
  35. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. An EATCS Series. Springer, 1999. 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