Document Open Access Logo

Model Checking and Validity in Propositional and Modal Inclusion Logics

Authors Lauri Hella, Antti Kuusisto, Arne Meier, Jonni Virtema

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.32.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Lauri Hella
Antti Kuusisto
Arne Meier
Jonni Virtema

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 32:1-32:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.32

Abstract

Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the basic reasoning problems for modal and propositional dependence, independence, and inclusion logics.
Keywords
  • Inclusion Logic
  • Model Checking
  • Complexity

Metrics

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

References

  1. S. R. Buss. The Boolean formula value problem is in ALOGTIME. In Proc. 19th STOC, pages 123-131, 1987. Google Scholar
  2. E. Clarke, E. A. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM ToPLS, 8(2):244-263, 1986. Google Scholar
  3. S. A. Cook. The complexity of theorem proving procedures. In Proc. 3rd STOC, pages 151-158, 1971. Google Scholar
  4. A. Durand, J. Kontinen, and H. Vollmer. Expressivity and complexity of dependence logic. In S. Abramsky, J. Kontinen, J. Väänänen, and H. Vollmer, editors, Dependence Logic: Theory and Applications, pages 5-32. Springer, 2016. Google Scholar
  5. P. 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.
  6. P. Galliani, M. Hannula, and J. Kontinen. Hierarchies in independence logic. In Proc. 22nd CSL, volume 23 of LIPIcs, pages 263-280, 2013. Google Scholar
  7. P. Galliani and L. Hella. Inclusion logic and fixed point logic. In Proc. 22nd CSL, LIPIcs, pages 281-295, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.281.
  8. M. R. Garey and D. S. Johnson. Computers and Intractability, A Guide to the Theory of NP-Completeness. Freeman, New York, 1979. Google Scholar
  9. L. M. Goldschlager. The monotone and planar circuit value problems are log-space complete for P. SIGACT News, 9:25-29, 1977. Google Scholar
  10. E. Grädel and J. Väänänen. Dependence and independence. Studia Logica, 101(2):399-410, 2013. Google Scholar
  11. M. Hannula and J. Kontinen. Hierarchies in independence and inclusion logic with strict semantics. J. Log. Comput., 25(3):879-897, 2015. URL: http://dx.doi.org/10.1093/logcom/exu057.
  12. M. Hannula, J. Kontinen, J. Virtema, and H. Vollmer. Complexity of propositional independence and inclusion logic. In Proc. 40th MFCS, pages 269-280, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48057-1_21.
  13. M. Hannula, J. Kontinen, J. Virtema, and H. Vollmer. Complexity of propositional logics in team semantics. CoRR, extended version of [12], abs/1504.06135, 2015. Google Scholar
  14. L. Hella, A. Kuusisto, A. Meier, and J. Virtema. Model checking and validity in propositional and modal inclusion logics. CoRR, abs/1609.06951, 2016. Google Scholar
  15. L. Hella, A. Kuusisto, A. Meier, and H. Vollmer. Modal inclusion logic: Being lax is simpler than being strict. In Proc. 40th MFCS, pages 281-292, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48057-1_22.
  16. L. Hella and J. Stumpf. The expressive power of modal logic with inclusion atoms. In Proc. 6th GandALF, pages 129-143, 2015. URL: http://dx.doi.org/10.4204/EPTCS.193.10.
  17. W. Hodges. Compositional semantics for a language of imperfect information. Logic Journal of the IGPL, 5(4):539-563, 1997. Google Scholar
  18. R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467-480, 1977. Google Scholar
  19. L. A. Levin. Universal sorting problems. Problems of Inform. Transm., 9:265-266, 1973. Google Scholar
  20. G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers &Math. with Applications, 41(7-8):957-992, 2001. URL: http://dx.doi.org/10.1016/S0898-1221(00)00333-3.
  21. K. Sano and J. Virtema. Characterizing frame definability in team semantics via the universal modality. In Proc. of WoLLIC 2015, pages 140-155, 2015. Google Scholar
  22. K. Sano and J. Virtema. Characterizing relative frame definability in team semantics via the universal modality. In Proc. of WoLLIC 2016, pages 392-409, 2016. Google Scholar
  23. P. Schnoebelen. The complexity of temporal logic model checking. In Proc. 4th AiML, pages 393-436, 2002. Google Scholar
  24. J. Väänänen. Dependence Logic. Cambridge University Press, 2007. Google Scholar
  25. H. Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer Verlag, Berlin Heidelberg, 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact