Document Open Access Logo

Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

Authors Juha Kontinen , Max Sandström , Jonni Virtema

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2023.60.pdf
  • Filesize: 0.7 MB
  • 14 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Hyperproperties
  • Linear Temporal Logic
  • Team Semantics

Metrics

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

Abstract

We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We relate the new semantics with the original semantics based on multisets and establish one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics.

Cite As Get BibTex

Juha Kontinen, Max Sandström, and Jonni Virtema. Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.60

Author Details

Juha Kontinen
  • University of Helsinki, Finland
Max Sandström
  • University of Sheffield, UK
  • University of Helsinki, Finland
Jonni Virtema
  • University of Sheffield, UK
  • University of Helsinki, Finland

Funding

  • Kontinen, Juha: Supported by the Academy of Finland grant 345634.
  • Sandström, Max: Supported by the Academy of Finland grant 322795.
  • Virtema, Jonni: Supported by the Academy of Finland grant 345634 and the DFG grant VI 1045/1-1.

References

  1. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. In CAV (1), volume 12759 of Lecture Notes in Computer Science, pages 694-717. Springer, 2021. Google Scholar
  2. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In POST 2014, pages 265-284, 2014. Google Scholar
  3. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. Google Scholar
  4. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In LICS 2019, pages 1-13. IEEE, 2019. Google Scholar
  5. 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.
  6. Pietro Galliani. Inclusion and exclusion dependencies in team semantics: On some logics of imperfect information. Annals of Pure and Applied Logic, 163(1):68-84, 2012. Google Scholar
  7. Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, and Jonni Virtema. Temporal team semantics revisited. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2-5, 2022, pages 44:1-44:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533360.
  8. 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.
  9. 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. Google Scholar
  10. 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.
  11. Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. Modal independence 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 353-372. College Publications, 2014. URL: http://www.aiml.net/volumes/volume10/Kontinen-Mueller-Schnoor-Vollmer.pdf.
  12. Juha Kontinen and Max Sandström. On the expressive power of TeamLTL and first-order team logic over hyperproperties. In WoLLIC, volume 13038 of Lecture Notes in Computer Science, pages 302-318. Springer, 2021. Google Scholar
  13. Juha Kontinen, Max Sandström, and Jonni Virtema. Set semantics for asynchronous TeamLTL: Expressivity and complexity. CoRR, abs/2304.10915, 2023. URL: https://doi.org/10.48550/arXiv.2304.10915.
  14. 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.
  15. 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, MFCS 2018, volume 117, pages 10:1-10:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  16. Martin Lück. Axiomatizations of team logics. Ann. Pure Appl. Log., 169(9):928-969, 2018. Google Scholar
  17. Martin Lück. On the complexity of team logic and its two-variable fragment. In MFCS, volume 117 of LIPIcs, pages 27:1-27:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  18. Martin Lück. On the complexity of linear temporal logic with team semantics. Theoretical Computer Science, 2020. Google Scholar
  19. Martin Lück. Team logic: axioms, expressiveness, complexity. PhD thesis, University of Hanover, Hannover, Germany, 2020. URL: https://www.repo.uni-hannover.de/handle/123456789/9430.
  20. 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.
  21. 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.
  22. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, pages 46-57. IEEE Computer Society, 1977. Google Scholar
  23. Markus N. Rabe. A Temporal Logic Approach to Information-Flow Control. PhD thesis, Saarland University, 2016. Google Scholar
  24. 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.
  25. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, July 1985. URL: https://doi.org/10.1145/3828.3837.
  26. Jouko Väänänen. Dependence Logic. Cambridge University Press, 2007. Google Scholar
  27. Jonni Virtema. Complexity of validity for propositional dependence logics. Inf. Comput., 253:224-236, 2017. URL: https://doi.org/10.1016/j.ic.2016.07.008.
  28. Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-time temporal logic with team semantics: Expressivity and complexity. CoRR, abs/2010.03311, 2020. URL: https://arxiv.org/abs/2010.03311.
  29. Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-time temporal logic with team semantics: Expressivity and complexity. In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference, volume 213 of LIPIcs, pages 52:1-52:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.52.
  30. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact