{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T16:51:27Z","timestamp":1773939087149,"version":"3.50.1"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T00:00:00Z","timestamp":1569542400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["247444366"],"award-info":[{"award-number":["247444366"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Commission, Community Research and Development Service","award":["647289"],"award-info":[{"award-number":["647289"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,1,31]]},"abstract":"<jats:p>We investigate the computational complexity of the satisfiability problem of modal inclusion logic. We distinguish two variants of the problem: one for the strict and another one for the lax semantics. Both problems turn out to be EXPTIME-complete on general structures. Finally, we show how for a specific class of structures NEXPTIME-completeness for these problems under strict semantics can be achieved.<\/jats:p>","DOI":"10.1145\/3356043","type":"journal-article","created":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T12:33:44Z","timestamp":1569587624000},"page":"1-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Satisfiability of Modal Inclusion Logic"],"prefix":"10.1145","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9117-8124","authenticated-orcid":false,"given":"Lauri","family":"Hella","sequence":"first","affiliation":[{"name":"Tampere University, Kanslerinrinne, Tampere, Finland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1356-8749","authenticated-orcid":false,"given":"Antti","family":"Kuusisto","sequence":"additional","affiliation":[{"name":"Tampere University, Kanslerinrinne, Tampere, Finland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8061-5376","authenticated-orcid":false,"given":"Arne","family":"Meier","sequence":"additional","affiliation":[{"name":"Leibniz Universit\u00fct Hannover, Hannover, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9292-1960","authenticated-orcid":false,"given":"Heribert","family":"Vollmer","sequence":"additional","affiliation":[{"name":"Leibniz Universit\u00fct Hannover, Hannover, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,9,27]]},"reference":[{"key":"#cr-split#-e_1_2_1_1_1.1","doi-asserted-by":"crossref","unstructured":"Samson Abramsky Juha Kontinen Jouko V\u00e4\u00e4n\u00e4nen and Heribert Vollmer (Eds.). 2016. Dependence Logic Theory and Applications. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-31803-5 10.1007\/978-3-319-31803-5","DOI":"10.1007\/978-3-319-31803-5"},{"key":"#cr-split#-e_1_2_1_1_1.2","doi-asserted-by":"crossref","unstructured":"Samson Abramsky Juha Kontinen Jouko V\u00e4\u00e4n\u00e4nen and Heribert Vollmer (Eds.). 2016. Dependence Logic Theory and Applications. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-31803-5","DOI":"10.1007\/978-3-319-31803-5"},{"key":"e_1_2_1_2_1","volume-title":"Modal Logic","author":"Blackburn Patrick","unstructured":"Patrick Blackburn , Maarten de Rijke , and Yde Venema . 2001. Modal Logic . Cambridge University Press . DOI:https:\/\/doi.org\/10.1017\/CBO9781107050884 10.1017\/CBO9781107050884 Patrick Blackburn, Maarten de Rijke, and Yde Venema. 2001. Modal Logic. Cambridge University Press. DOI:https:\/\/doi.org\/10.1017\/CBO9781107050884"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27660-6_19"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.08.005"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the Conference on Computer Science Logic (CSL\u201913)","volume":"23","author":"Galliani Pietro","year":"2013","unstructured":"Pietro Galliani , Miika Hannula , and Juha Kontinen . 2013 . Hierarchies in independence logic . In Proceedings of the Conference on Computer Science Logic (CSL\u201913) (LIPIcs), Simona Ronchi Della Rocca (Ed.) , Vol. 23 . Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 263--280. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.263 10.4230\/LIPIcs.CSL.2013.263 Pietro Galliani, Miika Hannula, and Juha Kontinen. 2013. Hierarchies in independence logic. In Proceedings of the Conference on Computer Science Logic (CSL\u201913) (LIPIcs), Simona Ronchi Della Rocca (Ed.), Vol. 23. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 263--280. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.263"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the Conference on Computer Science Logic (CSL\u201913)","volume":"23","author":"Galliani Pietro","year":"2013","unstructured":"Pietro Galliani and Lauri Hella . 2013 . Inclusion logic and fixed point logic . In Proceedings of the Conference on Computer Science Logic (CSL\u201913) (LIPIcs), Simona Ronchi Della Rocca (Ed.) , Vol. 23 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 281--295. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.281 10.4230\/LIPIcs.CSL.2013.281 Pietro Galliani and Lauri Hella. 2013. Inclusion logic and fixed point logic. In Proceedings of the Conference on Computer Science Logic (CSL\u201913) (LIPIcs), Simona Ronchi Della Rocca (Ed.), Vol. 23. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 281--295. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.281"},{"key":"e_1_2_1_8_1","first-page":"70","article-title":"Logics for dependence and independence (Dagstuhl seminar 15261)","volume":"5","author":"Gr\u00e4del Erich","year":"2015","unstructured":"Erich Gr\u00e4del , Juha Kontinen , Jouko V\u00e4\u00e4n\u00e4nen , and Heribert Vollmer . 2015 . Logics for dependence and independence (Dagstuhl seminar 15261) . Dagstuhl Rep. 5 , 6 (2015), 70 -- 85 . DOI:https:\/\/doi.org\/10.4230\/DagRep.5.6.70 10.4230\/DagRep.5.6.70 Erich Gr\u00e4del, Juha Kontinen, Jouko V\u00e4\u00e4n\u00e4nen, and Heribert Vollmer. 2015. Logics for dependence and independence (Dagstuhl seminar 15261). Dagstuhl Rep. 5, 6 (2015), 70--85. DOI:https:\/\/doi.org\/10.4230\/DagRep.5.6.70","journal-title":"Dagstuhl Rep."},{"key":"e_1_2_1_9_1","volume-title":"Ruzzo","author":"Greenlaw Raymond","year":"1995","unstructured":"Raymond Greenlaw , H. James Hoover , and Walter L . Ruzzo . 1995 . Limits to Parallel Computation : P-completeness Theory. Oxford University Press , Inc., New York, NY. Raymond Greenlaw, H. James Hoover, and Walter L. Ruzzo. 1995. Limits to Parallel Computation: P-completeness Theory. Oxford University Press, Inc., New York, NY."},{"key":"e_1_2_1_10_1","volume-title":"The entailment problem in modal and propositional dependence logics. Retrieved from CoRR abs\/1608.04301","author":"Hannula Miika","year":"2016","unstructured":"Miika Hannula . 2016. The entailment problem in modal and propositional dependence logics. Retrieved from CoRR abs\/1608.04301 ( 2016 ). http:\/\/arxiv.org\/abs\/1608.04301 Miika Hannula. 2016. The entailment problem in modal and propositional dependence logics. Retrieved from CoRR abs\/1608.04301 (2016). http:\/\/arxiv.org\/abs\/1608.04301"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 26th Conference on Computer Science Logic (CSL\u201917) (Leibniz International Proceedings in Informatics (LIPIcs)), Valentin Goranko and Mads Dam (Eds.)","volume":"82","author":"Hannula Miika","year":"2017","unstructured":"Miika Hannula . 2017 . Validity and entailment in modal and propositional dependence logics . In Proceedings of the 26th Conference on Computer Science Logic (CSL\u201917) (Leibniz International Proceedings in Informatics (LIPIcs)), Valentin Goranko and Mads Dam (Eds.) , Vol. 82 . Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 28:1--28:17. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2017.28 10.4230\/LIPIcs.CSL.2017.28 Miika Hannula. 2017. Validity and entailment in modal and propositional dependence logics. In Proceedings of the 26th Conference on Computer Science Logic (CSL\u201917) (Leibniz International Proceedings in Informatics (LIPIcs)), Valentin Goranko and Mads Dam (Eds.), Vol. 82. Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 28:1--28:17. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2017.28"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3157054"},{"key":"e_1_2_1_13_1","volume-title":"Model checking and validity in propositional and modal inclusion logics. Retrieved from CoRR abs\/1609.06951","author":"Hella Lauri","year":"2016","unstructured":"Lauri Hella , Antti Kuusisto , Arne Meier , and Jonni Virtema . 2016. Model checking and validity in propositional and modal inclusion logics. Retrieved from CoRR abs\/1609.06951 ( 2016 ). Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. 2016. Model checking and validity in propositional and modal inclusion logics. Retrieved from CoRR abs\/1609.06951 (2016)."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201917)","volume":"83","author":"Hella Lauri","year":"2017","unstructured":"Lauri Hella , Antti Kuusisto , Arne Meier , and Jonni Virtema . 2017 . Model checking and validity in propositional and modal inclusion logics . In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201917) (LIPIcs), Kim G. Larsen, Hans L. Bodlaender, and Jean-Fran\u00e7ois Raskin (Eds.) , Vol. 83 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 32:1--32:14. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.32 10.4230\/LIPIcs.MFCS.2017.32 Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. 2017. Model checking and validity in propositional and modal inclusion logics. In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201917) (LIPIcs), Kim G. Larsen, Hans L. Bodlaender, and Jean-Fran\u00e7ois Raskin (Eds.), Vol. 83. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 32:1--32:14. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.32"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_22"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1040046086"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802187"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30227-8_32"},{"key":"e_1_2_1_19_1","first-page":"1333","article-title":"Modal independence logic","volume":"27","author":"Kontinen Juha","year":"2017","unstructured":"Juha Kontinen , Julian-Steffen M\u00fcller , Henning Schnoor , and Heribert Vollmer . 2017 . Modal independence logic . J. Log. Comput. 27 , 5 (2017), 1333 -- 1352 . DOI:https:\/\/doi.org\/10.1093\/logcom\/exw019 10.1093\/logcom Juha Kontinen, Julian-Steffen M\u00fcller, Henning Schnoor, and Heribert Vollmer. 2017. Modal independence logic. J. Log. Comput. 27, 5 (2017), 1333--1352. DOI:https:\/\/doi.org\/10.1093\/logcom\/exw019","journal-title":"J. Log. Comput."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-015-9217-4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 27th EACSL Conference on Computer Science Logic (CSL\u201918)","volume":"119","author":"L\u00fcck Martin","year":"2018","unstructured":"Martin L\u00fcck . 2018 . Canonical models and the complexity of modal team logic . In Proceedings of the 27th EACSL Conference on Computer Science Logic (CSL\u201918) (LIPIcs), Dan R. Ghica and Achim Jung (Eds.) , Vol. 119 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 30:1--30:23. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.30 10.4230\/LIPIcs.CSL.2018.30 Martin L\u00fcck. 2018. Canonical models and the complexity of modal team logic. In Proceedings of the 27th EACSL Conference on Computer Science Logic (CSL\u201918) (LIPIcs), Dan R. Ghica and Achim Jung (Eds.), Vol. 119. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 30:1--30:23. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.30"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0898-1221(00)00333-3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl034"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 4th Conference on Advances in Modal Logic, Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev (Eds.). King\u2019s College Publications, 393--436","author":"Schnoebelen Philippe","year":"2002","unstructured":"Philippe Schnoebelen . 2002 . The complexity of temporal logic model checking . In Proceedings of the 4th Conference on Advances in Modal Logic, Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev (Eds.). King\u2019s College Publications, 393--436 . Philippe Schnoebelen. 2002. The complexity of temporal logic model checking. In Proceedings of the 4th Conference on Advances in Modal Logic, Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev (Eds.). King\u2019s College Publications, 393--436."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn102"},{"key":"e_1_2_1_28_1","volume-title":"New Perspectives on Games and Interaction","author":"V\u00e4\u00e4n\u00e4nen Jouko","unstructured":"Jouko V\u00e4\u00e4n\u00e4nen . 2008. Modal dependence logic . In New Perspectives on Games and Interaction , K. Apt and R. van Rooij (Eds.). Amsterdam University Press , 237--254. Jouko V\u00e4\u00e4n\u00e4nen. 2008. Modal dependence logic. In New Perspectives on Games and Interaction, K. Apt and R. van Rooij (Eds.). Amsterdam University Press, 237--254."},{"key":"e_1_2_1_29_1","volume-title":"Dependence Logic\u2014A New Approach to Independence Friendly Logic","author":"V\u00e4\u00e4n\u00e4nen Jouko A.","unstructured":"Jouko A. V\u00e4\u00e4n\u00e4nen . 2007. Dependence Logic\u2014A New Approach to Independence Friendly Logic . London Mathematical Society student texts, Vol. 70 . Cambridge University Press . Retrieved from http:\/\/www.cambridge.org\/de\/knowledge\/isbn\/item1164246\/?site_locale&equals;de_DE. Jouko A. V\u00e4\u00e4n\u00e4nen. 2007. Dependence Logic\u2014A New Approach to Independence Friendly Logic. London Mathematical Society student texts, Vol. 70. Cambridge University Press. Retrieved from http:\/\/www.cambridge.org\/de\/knowledge\/isbn\/item1164246\/?site_locale&equals;de_DE."},{"key":"e_1_2_1_30_1","volume-title":"Johan van Benthem on Logic and Information Dynamics","author":"van Eijck Jan","unstructured":"Jan van Eijck . 2014. Dynamic epistemic logics . In Johan van Benthem on Logic and Information Dynamics , Alexandru Baltag and Sonja Smets (Eds.). Springer , 175--202. DOI:https:\/\/doi.org\/10.1007\/978-3-319-06025-5_7 10.1007\/978-3-319-06025-5_7 Jan van Eijck. 2014. Dynamic epistemic logics. In Johan van Benthem on Logic and Information Dynamics, Alexandru Baltag and Sonja Smets (Eds.). Springer, 175--202. DOI:https:\/\/doi.org\/10.1007\/978-3-319-06025-5_7"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3356043","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3356043","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:08Z","timestamp":1750268948000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3356043"}},"subtitle":["Lax and Strict Semantics"],"short-title":[],"issued":{"date-parts":[[2019,9,27]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1,31]]}},"alternative-id":["10.1145\/3356043"],"URL":"https:\/\/doi.org\/10.1145\/3356043","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,27]]},"assertion":[{"value":"2017-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}