Document Open Access Logo

Canonical Models and the Complexity of Modal Team Logic

Author Martin Lück

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.30.pdf
  • Filesize: 0.58 MB
  • 23 pages

Document Identifiers

Author Details

Martin Lück
  • Institut für Theoretische Informatik, Leibniz Universität Hannover, Appelstraße 4, 30167 Hannover, Germany

Cite As Get BibTex

Martin Lück. Canonical Models and the Complexity of Modal Team Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.30

Abstract

We study modal team logic MTL, the team-semantical extension of classical modal logic closed under Boolean negation. Its fragments, such as modal dependence, independence, and inclusion logic, are well-understood. However, due to the unrestricted Boolean negation, the satisfiability problem of full MTL has been notoriously resistant to a complexity theoretical classification.
In our approach, we adapt the notion of canonical models for team semantics. By construction of such a model, we reduce the satisfiability problem of MTL to simple model checking. Afterwards, we show that this method is optimal in the sense that MTL-formulas can efficiently enforce canonicity.
Furthermore, to capture these results in terms of computational complexity, we introduce a non-elementary complexity class, TOWER(poly), and prove that the satisfiability and validity problem of MTL are complete for it. We also show that the fragments of MTL with bounded modal depth are complete for the levels of the elementary hierarchy (with polynomially many alternations).

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Logic
Keywords
  • team semantics
  • modal logic
  • complexity
  • satisfiability

Metrics

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

Related Versions

References

  1. Samson Abramsky, Juha Kontinen, Jouko Väänänen, and Heribert Vollmer, editors. Dependence Logic, Theory and Applications. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-31803-5.
  2. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal logic. Cambridge University Press, New York, NY, USA, 2001. Google Scholar
  3. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: http://dx.doi.org/10.1145/322234.322243.
  4. Kevin J. Compton and C. Ward Henson. A Uniform Method for Proving Lower Bounds on the Computational Complexity of Logical Theories. Ann. Pure Appl. Logic, 48(1):1-79, 1990. URL: http://dx.doi.org/10.1016/0168-0072(90)90080-L.
  5. Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pages 151-158, 1971. URL: http://dx.doi.org/10.1145/800157.805047.
  6. Arnaud Durand, Juha Kontinen, and Heribert Vollmer. Expressivity and Complexity of Dependence Logic, pages 5-32. Springer International Publishing, 2016. URL: http://dx.doi.org/10.1007/978-3-319-31803-5_2.
  7. Pietro Galliani. Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Ann. Pure Appl. Logic, 163(1):68-84, 2012. URL: http://dx.doi.org/10.1016/j.apal.2011.08.005.
  8. Pietro Galliani. Upwards closed dependencies in team semantics. Information and Computation, 245:124-135, 2015. URL: http://dx.doi.org/10.1016/j.ic.2015.06.008.
  9. Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399-410, 2013. URL: http://dx.doi.org/10.1007/s11225-013-9479-2.
  10. Miika Hannula. Validity and entailment in modal and propositional dependence logics. CoRR, abs/1608.04301, 2016. URL: http://arxiv.org/abs/1608.04301.
  11. Miika Hannula. Validity and Entailment in Modal and Propositional Dependence Logics. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.28.
  12. Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On Quantified Propositional Logics and the Exponential Time Hierarchy. In Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, pages 198-212, 2016. URL: http://dx.doi.org/10.4204/EPTCS.226.14.
  13. Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of propositional independence and inclusion logic. In Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, pages 269-280, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48057-1_21.
  14. Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of Propositional Logics in Team Semantic. ACM Transactions on Computational Logic, 19(1):1-14, jan 2018. URL: http://dx.doi.org/10.1145/3157054.
  15. Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. Model checking and validity in propositional and modal inclusion logics. In 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, pages 32:1-32:14, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.MFCS.2017.32.
  16. Lauri Hella, Antti Kuusisto, Arne Meier, and Heribert Vollmer. Modal Inclusion Logic: Being Lax is Simpler than Being Strict. In Mathematical Foundations of Computer Science 2015, volume 9234, pages 281-292. Springer Berlin Heidelberg, 2015. URL: http://link.springer.com/10.1007/978-3-662-48057-1_22.
  17. Lauri Hella, Kerkko Luosto, Katsuhiko Sano, and Jonni Virtema. The expressive power of modal dependence logic. In Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic". Groningen, The Netherlands, August 5-8, 2014, pages 294-312, 2014. URL: http://www.aiml.net/volumes/volume10/Hella-Luosto-Sano-Virtema.pdf.
  18. Lauri Hella and Johanna Stumpf. The expressive power of modal logic with inclusion atoms. Electronic Proceedings in Theoretical Computer Science, 193:129-143, 2015. URL: http://dx.doi.org/10.4204/EPTCS.193.10.
  19. Jaakko Hintikka and Gabriel Sandu. Informational Independence as a Semantical Phenomenon. In Jens Erik Fenstad, Ivan T. Frolov, and Risto Hilpinen, editors, Logic, Methodology and Philosophy of Science VIII, volume 126 of Studies in Logic and the Foundations of Mathematics, pages 571-589. Elsevier, 1989. URL: http://dx.doi.org/10.1016/S0049-237X(08)70066-1.
  20. Wilfrid Hodges. Compositional semantics for a language of imperfect information. Logic Journal of IGPL, 5(4):539-563, 1997. URL: http://dx.doi.org/10.1093/jigpal/5.4.539.
  21. M. Jonáš and J. Strejček. On the complexity of the quantified bit-vector arithmetic with binary encoding. Information Processing Letters, 2018. URL: http://dx.doi.org/10.1016/j.ipl.2018.02.018.
  22. Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. A Van Benthem theorem for modal team semantics. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, pages 277-291, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.277.
  23. Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. Modal independence logic. Journal of Logic and Computation, 27(5):1333-1352, 2017. URL: http://dx.doi.org/10.1093/logcom/exw019.
  24. Juha Kontinen and Ville Nurmi. Team logic and second-order logic. Fundam. Inform., 106(2-4):259-272, 2011. URL: http://dx.doi.org/10.3233/FI-2011-386.
  25. Andreas Krebs, Arne Meier, and Jonni Virtema. A team based variant of CTL. In 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, pages 140-149, 2015. URL: http://dx.doi.org/10.1109/TIME.2015.11.
  26. Peter Lohmann and Heribert Vollmer. Complexity results for modal dependence logic. Studia Logica, 101(2):343-366, 04 2013. URL: http://dx.doi.org/10.1007/s11225-013-9483-6.
  27. Martin Lück. Axiomatizations for propositional and modal team logic. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, pages 33:1-33:18, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.33.
  28. Martin Lück. The power of the filtration technique for modal logics with team semantics. In 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, pages 31:1-31:20, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.31.
  29. Martin Lück. On the complexity of team logic and its two-variable fragment. MFCS 2018. To appear. Google Scholar
  30. Martin Lück. Canonical models and the complexity of modal team logic. CoRR, abs/1709.05253, 2017. URL: https://arxiv.org/abs/1709.05253.
  31. Julian-Steffen Müller. Satisfiability and model checking in team based logics. PhD thesis, University of Hanover, 2014. URL: http://d-nb.info/1054741921.
  32. Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3:1-3:36, 2016. URL: http://dx.doi.org/10.1145/2858784.
  33. Merlijn Sevenster. Model-theoretic and computational properties of modal dependence logic. J. Log. Comput., 19(6):1157-1173, 2009. URL: http://dx.doi.org/10.1093/logcom/exn102.
  34. Larry J. Stockmeyer and Albert R. Meyer. Word Problems Requiring Exponential Time: Preliminary Report. In Proceedings of the 5th Annual ACM Symposium on Theory of Computing, pages 1-9, 1973. URL: http://dx.doi.org/10.1145/800125.804029.
  35. Jouko Väänänen. Modal dependence logic. New perspectives on games and interaction, 4:237-254, 2008. Google Scholar
  36. 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.
  37. Marco Voigt. A fine-grained hierarchy of hard problems in the separated fragment. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005094.
  38. Jouko Väänänen. Dependence logic: A New Approach to Independence Friendly Logic. Number 70 in London Mathematical Society student texts. Cambridge University Press, Cambridge ; New York, 2007. Google Scholar
  39. Fan Yang and Jouko Väänänen. Propositional logics of dependence. Ann. Pure Appl. Logic, 167(7):557-589, 2016. URL: http://dx.doi.org/10.1016/j.apal.2016.03.003.
  40. Fan Yang and Jouko Väänänen. Propositional team logics. Ann. Pure Appl. Logic, 168(7):1406-1441, 2017. URL: http://dx.doi.org/10.1016/j.apal.2017.01.007.
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