Document Open Access Logo

Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity

Authors Jonni Virtema , Jana Hofmann , Bernd Finkbeiner , Juha Kontinen , Fan Yang

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.52.pdf
  • Filesize: 0.78 MB
  • 17 pages

Document Identifiers

Author Details

Jonni Virtema
  • Institute for Theoretical Computer Science, Leibniz Universität Hannover, Germany
  • Department of Computer Science, University of Sheffield, UK
Jana Hofmann
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Bernd Finkbeiner
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Juha Kontinen
  • Department of Mathematics and Statistics, University of Helsinki, Finland
Fan Yang
  • Department of Mathematics and Statistics, University of Helsinki, Finland

Funding

Jana Hofmann and Bernd Finkbeiner: Partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center "Foundations of Perspicuous Software Systems" (TRR 248, 389792660) and by the European Research Council (ERC) Grant OSARES (No. 683300).
  • Virtema, Jonni: Supported by the DFG grant VI 1045/1-1.
  • Kontinen, Juha: Supported by grant 308712 of the Academy of Finland.
  • Yang, Fan: Supported by grants 330525 and 308712 of Academy of Finland, and Research Funds of University of Helsinki.

Cite AsGet BibTex

Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 52:1-52:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.52

Abstract

We study the expressivity and complexity of model checking of linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL -extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
Keywords
  • Linear temporal logic
  • Hyperproperties
  • Model Checking
  • Expressivity

Metrics

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

Related Versions

References

  1. Erika Ábrahám and Borzoo Bonakdarpour. Hyperpctl: A temporal logic for probabilistic hyperproperties. In Annabelle McIver and András Horváth, editors, Quantitative Evaluation of Systems - 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings, volume 11024 of Lecture Notes in Computer Science, pages 20-35. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99154-2_2.
  2. Shreya Agrawal and Borzoo Bonakdarpour. Runtime verification of k-safety hyperproperties in hyperltl. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016, pages 239-252. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/CSF.2016.24.
  3. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. J. ACM, 41(1):181-204, 1994. URL: https://doi.org/10.1145/174644.174651.
  4. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of Lecture Notes in Computer Science, pages 694-717. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_33.
  5. Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In Proceedings of FoSSaCS, volume 9034 of LNCS, pages 167-182. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_11.
  6. Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A new symbolic model verifier. In Proc. International Conference on Computer Aided Verification, pages 495-499, July 1999. Google Scholar
  7. 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: https://doi.org/10.1007/978-3-642-54792-8_15.
  8. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  9. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785713.
  10. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Yannick Schillo. Runtime enforcement of hyperproperties. To appear at the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021), 2021. Google Scholar
  11. Byron Cook, Eric Koskinen, and Moshe Vardi. Temporal property verification as a program analysis task. In Proc. Computer Aided Verification, pages 333-348, July 2011. Google Scholar
  12. Jukka Corander, Antti Hyttinen, Juha Kontinen, Johan Pensar, and Jouko Väänänen. A logical approach to context-specific independence. Ann. Pure Appl. Logic, 170(9):975-992, 2019. URL: https://doi.org/10.1016/j.apal.2019.04.004.
  13. Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, and Jonni Virtema. Probabilistic team semantics. In FoIKS, volume 10833 of Lecture Notes in Computer Science, pages 186-206. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-90050-6_11.
  14. Bernd Finkbeiner, Lennart Haas, and Hazem Torfah. Canonical representations of k-safety hyperproperties. In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019, pages 17-31. IEEE, 2019. URL: https://doi.org/10.1109/CSF.2019.00009.
  15. Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  16. Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Leander Tentrup. Realizing ømega-regular hyperproperties. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 40-63. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_4.
  17. Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137-163, 2020. URL: https://doi.org/10.1007/s00236-019-00358-2.
  18. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods Syst. Des., 54(3):336-363, 2019. URL: https://doi.org/10.1007/s10703-019-00334-z.
  19. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking HyperLTL and HyperCTL^*. In Proceedings of CAV, volume 9206 of LNCS, pages 30-48. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_3.
  20. Pietro Galliani and Lauri Hella. Inclusion Logic and Fixed Point Logic. In CSL 2013, pages 281-295, 2013. Google Scholar
  21. Giuseppe De Giacomo, Paolo Felli, Marco Montali, and Giuseppe Perelli. Hyperldlf: a logic for checking properties of finite traces process logs. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 1859-1865. ijcai.org, 2021. URL: https://doi.org/10.24963/ijcai.2021/256.
  22. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434319.
  23. Miika Hannula and Juha Kontinen. A finite axiomatization of conditional independence and inclusion dependencies. Inf. Comput., 249:121-137, 2016. URL: https://doi.org/10.1016/j.ic.2016.04.001.
  24. Miika Hannula, Juha Kontinen, Jan Van den Bussche, and Jonni Virtema. Descriptive complexity of real computation and probabilistic independence logic. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 550-563. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394773.
  25. Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of propositional logics in team semantic. ACM Trans. Comput. Log., 19(1):2:1-2:14, 2018. URL: https://doi.org/10.1145/3157054.
  26. Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. Model checking and validity in propositional and modal inclusion logics. J. Log. Comput., 29(5):605-630, 2019. URL: https://doi.org/10.1093/logcom/exz008.
  27. Lauri Hella, Kerkko Luosto, Katsuhiko Sano, and Jonni Virtema. The expressive power of modal dependence logic. In Rajeev Goré, Barteld P. Kooi, and Agi Kurucz, editors, Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic," held in Groningen, The Netherlands, August 5-8, 2014, pages 294-312. College Publications, 2014. URL: http://www.aiml.net/volumes/volume10/Hella-Luosto-Sano-Virtema.pdf.
  28. Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones. On verifying timed hyperproperties. In Johann Gamper, Sophie Pinchinat, and Guido Sciavicco, editors, 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, October 16-19, 2019, Málaga, Spain, volume 147 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TIME.2019.20.
  29. Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23:279-295, 1997. Google Scholar
  30. Tapani Hyttinen, Gianluca Paolini, and Jouko Väänänen. A Logic for Arguing About Probabilities in Measure Teams. Arch. Math. Logic, 56(5-6):475-489, 2017. URL: https://doi.org/10.1007/s00153-017-0535-x.
  31. Jarmo Kontinen. Coherence and computational complexity of quantifier-free dependence logic formulas. Studia Logica, 101(2):267-291, 2013. URL: https://doi.org/10.1007/s11225-013-9481-8.
  32. Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. A van benthem theorem for modal team semantics. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 277-291. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.277.
  33. Andreas Krebs, Arne Meier, and Jonni Virtema. A team based variant of CTL. In Fabio Grandi, Martin Lange, and Alessio Lomuscio, editors, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel, Germany, September 23-25, 2015, pages 140-149. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/TIME.2015.11.
  34. Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In Igor Potapov, Paul Spirakis, and James Worrell, editors, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), volume 117 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.10.
  35. Martin Lück. On the complexity of linear temporal logic with team semantics. Theoretical Computer Science, 2020. URL: https://doi.org/10.1016/j.tcs.2020.04.019.
  36. Corto Mascle and Martin Zimmermann. The keys to decidable hyperltl satisfiability: Small models or very simple formulas. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 29:1-29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.29.
  37. John McLean. Proving noninterference and functional correctness using traces. Journal of Computer Security, 1(1):37-58, 1992. URL: https://doi.org/10.3233/JCS-1992-1103.
  38. Nir Piterman and Amir Pnueli. Temporal logic and fair discrete systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 27-73. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_2.
  39. Amir Pnueli. The Temporal Logic of Programs. In FOCS 1977, pages 46-57, 1977. Google Scholar
  40. Markus N. Rabe. A Temporal Logic Approach to Information-Flow Control. PhD thesis, Saarland University, 2016. Google Scholar
  41. 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: https://doi.org/10.1109/SECPRI.1995.398927.
  42. Katsuhiko Sano and Jonni Virtema. Characterising modal definability of team-based logics via the universal modality. Ann. Pure Appl. Log., 170(9):1100-1127, 2019. URL: https://doi.org/10.1016/j.apal.2019.04.009.
  43. Philippe Schnoebelen. Lossy counter machines decidability cheat sheet. In Antonín Kucera and Igor Potapov, editors, Reachability Problems, 4th International Workshop, RP 2010, Brno, Czech Republic, August 28-29, 2010. Proceedings, volume 6227 of Lecture Notes in Computer Science, pages 51-75. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15349-5_4.
  44. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  45. Jouko Väänänen. Dependence Logic. Cambridge University Press, 2007. Google Scholar
  46. Jouko Väänänen. Modal dependence logic. In New Perspectives on Games and Interaction, 2008. Google Scholar
  47. Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-time temporal logic with team semantics: Expressivity and complexity. arXiv preprint, 2020. URL: http://arxiv.org/abs/2010.03311.
  48. Fan Yang and Jouko Väänänen. Propositional team logics. Annals of Pure and Applied Logic, 168(7):1406-1441, 2017. URL: https://doi.org/10.1016/j.apal.2017.01.007.
  49. 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: https://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 Imprint Privacy Contact