{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:46:45Z","timestamp":1765547205493,"version":"3.41.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,1,16]],"date-time":"2024-01-16T00:00:00Z","timestamp":1705363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,1,31]]},"abstract":"<jats:p>\n            We establish the precise complexity of the model-checking problem for the main logics of knowledge and time. While this problem was known to be non-elementary for agents with perfect recall, with a number of exponentials that increases with the alternation of knowledge operators, the precise complexity of the problem when the maximum alternation is fixed has been an open problem for 20 years. We close it by establishing improved upper bounds for\n            <jats:sans-serif>CTL<\/jats:sans-serif>\n            * with knowledge and providing matching lower bounds that also apply for epistemic extensions of\n            <jats:sans-serif>LTL<\/jats:sans-serif>\n            and\n            <jats:sans-serif>CTL<\/jats:sans-serif>\n            . We also study the model-checking problem for these logics on systems satisfying the \u201cno learning\u201d property, introduced by Halpern and Vardi in their taxonomy of logics of knowledge and time, and we settle the complexity in almost all cases.\n          <\/jats:p>","DOI":"10.1145\/3637212","type":"journal-article","created":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T11:39:18Z","timestamp":1702467558000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Complexity of Model Checking Knowledge and Time"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0963-8169","authenticated-orcid":false,"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9081-2920","authenticated-orcid":false,"given":"Bastien","family":"Maubert","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4876-3448","authenticated-orcid":false,"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,16]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"664","volume-title":"TACAS","author":"Alur Rajeev","year":"2007","unstructured":"Rajeev Alur, Pavol \u010cern\u1ef3, and Swarat Chaudhuri. 2007. Model checking on trees with path equivalences. In TACAS. Springer, 664\u2013678."},{"key":"e_1_3_2_3_2","volume-title":"KR","author":"Aminof Benjamin","year":"2016","unstructured":"Benjamin Aminof, Aniello Murano, Sasha Rubin, and Florian Zuleger. 2016. Prompt alternating-time epistemic logics. In KR."},{"key":"e_1_3_2_4_2","first-page":"333","volume-title":"AAMAS","author":"Aucher Guillaume","year":"2014","unstructured":"Guillaume Aucher. 2014. Supervisory control theory in epistemic temporal logic. In AAMAS. 333\u2013340. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=2615787"},{"key":"e_1_3_2_5_2","first-page":"62","volume-title":"AAMAS","author":"Belardinelli Francesco","year":"2022","unstructured":"Francesco Belardinelli, Wojtek Jamroga, Vadim Malvone, Munyque Mittelmann, Aniello Murano, and Laurent Perrussel. 2022. Reasoning about human-friendly strategies in repeated keyword auctions. In AAMAS, Piotr Faliszewski, Viviana Mascardi, Catherine Pelachaud, and Matthew E. Taylor (Eds.). International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS), 62\u201371."},{"key":"e_1_3_2_6_2","first-page":"1787","volume-title":"IJCAI","author":"Belardinelli Francesco","year":"2021","unstructured":"Francesco Belardinelli, Sophia Knight, Alessio Lomuscio, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2021. Reasoning about agents that may know other agents\u2019 strategies. In IJCAI, Zhi-Hua Zhou (Ed.). ijcai.org, 1787\u20131793."},{"key":"e_1_3_2_7_2","first-page":"91","volume-title":"IJCAI","author":"Belardinelli Francesco","year":"2017","unstructured":"Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin. 2017. Verification of broadcasting multi-agent systems against an epistemic strategy logic. In IJCAI, Vol. 17. 91\u201397."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103302"},{"key":"e_1_3_2_9_2","first-page":"7071","volume-title":"AAAI","author":"Belardinelli Francesco","year":"2020","unstructured":"Francesco Belardinelli, Alessio Lomuscio, and Emily Yu. 2020. Model checking temporal epistemic logic under bounded recall. In AAAI. 7071\u20137078."},{"key":"e_1_3_2_10_2","first-page":"331","volume-title":"Complexity, Logic, and Recursion Theory","author":"Boas P. Van Emde","year":"1997","unstructured":"P. Van Emde Boas. 1997. The convenience of tilings. In Complexity, Logic, and Recursion Theory. Marcel Dekker Inc, 331\u2013363."},{"key":"e_1_3_2_11_2","first-page":"441","volume-title":"CAV","author":"Bozianu Rodica","year":"2014","unstructured":"Rodica Bozianu, C\u0103t\u0103lin Dima, and Emmanuel Filiot. 2014. Safraless synthesis for epistemic temporal specifications. In CAV. Springer, 441\u2013456."},{"key":"e_1_3_2_12_2","first-page":"1595","volume-title":"IJCAI","author":"Bozzelli Laura","year":"2019","unstructured":"Laura Bozzelli, Bastien Maubert, and Aniello Murano. 2019. The complexity of model checking knowledge and time. In IJCAI. 1595\u20131601."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.03.012"},{"key":"e_1_3_2_14_2","first-page":"167","volume-title":"FoSSaCS","author":"Bozzelli Laura","year":"2015","unstructured":"Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. 2015. Unifying hyper and epistemic temporal logics. In FoSSaCS. Springer, 167\u2013182."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/265910.265912"},{"key":"e_1_3_2_16_2","first-page":"525","volume-title":"CAV","author":"\u010cerm\u00e1k Petr","year":"2014","unstructured":"Petr \u010cerm\u00e1k, Alessio Lomuscio, Fabio Mogavero, and Aniello Murano. 2014. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In CAV. Springer, 525\u2013532."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-010-9765-8"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02734-5_8"},{"key":"e_1_3_2_19_2","article-title":"Chain-monadic second order logic over regular automatic trees and epistemic planning synthesis.","volume":"7","author":"Dou\u00e9neau-Tabot Ga\u00ebtan","year":"2018","unstructured":"Ga\u00ebtan Dou\u00e9neau-Tabot, Sophie Pinchinat, and Fran\u00e7ois Schwarzentruber. 2018. Chain-monadic second order logic over regular automatic trees and epistemic planning synthesis. Adv. Modal Logic 7 (2018).","journal-title":"Adv. Modal Logic"},{"key":"e_1_3_2_20_2","first-page":"99","volume-title":"LICS","author":"Dziembowski Stefan","year":"1997","unstructured":"Stefan Dziembowski, Marcin Jurdzinski, and Igor Walukiewicz. 1997. How much memory is needed to win infinite games? In LICS. IEEE, 99\u2013110."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90036-0"},{"key":"e_1_3_2_23_2","first-page":"195","volume-title":"LFCS","author":"Engelhardt Kai","year":"2007","unstructured":"Kai Engelhardt, Peter Gammie, and Ron Van Der Meyden. 2007. Model checking knowledge and linear time: PSPACE cases. In LFCS. Springer, 195\u2013211."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_3_2_25_2","first-page":"479","volume-title":"CAV","author":"Gammie Peter","year":"2004","unstructured":"Peter Gammie and Ron Van Der Meyden. 2004. MCK: Model checking the logic of knowledge. In CAV. Springer, 479\u2013483."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.21.93-131"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2005-13305"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797320906"},{"key":"e_1_3_2_29_2","first-page":"304","volume-title":"STOC","author":"Halpern Joseph Y.","year":"1986","unstructured":"Joseph Y. Halpern and Moshe Y. Vardi. 1986. The complexity of reasoning about knowledge and time. In STOC. ACM, 304\u2013315."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/12130.12161"},{"key":"e_1_3_2_31_2","first-page":"1076","volume-title":"IJCAI","author":"Huang Xiaowei","year":"2015","unstructured":"Xiaowei Huang, Qingliang Chen, and Kaile Su. 2015. The complexity of model checking succinct multiagent systems. In IJCAI. 1076\u20131082. Retrieved from http:\/\/ijcai.org\/Abstract\/15\/156"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3233769"},{"key":"e_1_3_2_33_2","first-page":"549","volume-title":"ECAI","author":"Huang Xiaowei","year":"2010","unstructured":"Xiaowei Huang and Ron van der Meyden. 2010. The complexity of epistemic model checking: Clock semantics and branching time. In ECAI. 549\u2013554."},{"issue":"2","key":"e_1_3_2_34_2","first-page":"221","article-title":"From bounded to unbounded model checking for temporal epistemic logic","volume":"63","author":"Kacprzak Magdalena","year":"2004","unstructured":"Magdalena Kacprzak, Alessio Lomuscio, and Wojciech Penczek. 2004. From bounded to unbounded model checking for temporal epistemic logic. Fundam. Inform. 63, 2-3 (2004), 221\u2013240.","journal-title":"Fundam. Inform."},{"key":"e_1_3_2_35_2","first-page":"638","volume-title":"AAMAS","author":"Kacprzak Magdalena","year":"2004","unstructured":"Magdalena Kacprzak, Alessio Lomuscio, and Wojciech Penczek. 2004. Verification of multiagent systems via unbounded model checking. In AAMAS. IEEE, 638\u2013645."},{"key":"e_1_3_2_36_2","first-page":"114","volume-title":"AAMAS","author":"Kong Jeremy","year":"2017","unstructured":"Jeremy Kong and Alessio Lomuscio. 2017. Symbolic model checking multi-agent systems against CTL*K specifications. In AAMAS. 114\u2013122. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=3091147"},{"key":"e_1_3_2_37_2","first-page":"207","volume-title":"TARK","author":"Ladner Richard E.","year":"1986","unstructured":"Richard E. Ladner and John H. Reif. 1986. The logic of distributed protocols. In TARK. 207\u2013222."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.05.005"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0378-x"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160733"},{"key":"e_1_3_2_41_2","volume-title":"Logical Foundations of Games with Imperfect Information: Uniform Strategies. (Fondations logiques des jeux \u00e0 information imparfaite : Strat\u00e9gies uniformes)","author":"Maubert Bastien","year":"2014","unstructured":"Bastien Maubert. 2014. Logical Foundations of Games with Imperfect Information: Uniform Strategies. (Fondations logiques des jeux \u00e0 information imparfaite : Strat\u00e9gies uniformes). Ph. D. Dissertation. University of Rennes 1, France. Retrieved from https:\/\/tel.archives-ouvertes.fr\/tel-00980490"},{"key":"e_1_3_2_42_2","volume-title":"KR","author":"Maubert Bastien","year":"2018","unstructured":"Bastien Maubert and Aniello Murano. 2018. Reasoning about knowledge and strategies under hierarchical information. In KR."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA200088"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/260"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-013-9232-2"},{"key":"e_1_3_2_46_2","first-page":"34","volume-title":"CONCUR","author":"Meyden Ron van der","year":"1998","unstructured":"Ron van der Meyden and Moshe Y. Vardi. 1998. Synthesis from knowledge-based specifications. In CONCUR. Springer, 34\u201349."},{"key":"e_1_3_2_47_2","first-page":"43","volume-title":"TARK","author":"Neiger Gil","year":"1992","unstructured":"Gil Neiger and Rida Bazzi. 1992. Using knowledge to optimally achieve coordination in distributed systems. In TARK. 43\u201359."},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_21"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.5555\/937485.937491"},{"key":"e_1_3_2_50_2","first-page":"46","volume-title":"FOCS","author":"Pnueli Amir","year":"1977","unstructured":"Amir Pnueli. 1977. The temporal logic of programs. In FOCS. IEEE, 46\u201357."},{"key":"e_1_3_2_51_2","first-page":"592","volume-title":"MFCS","author":"Puchala Bernd","year":"2010","unstructured":"Bernd Puchala. 2010. Asynchronous omega-regular games with partial information. In MFCS. 592\u2013603."},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.12.010"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"e_1_3_2_54_2","first-page":"25","volume-title":"FICS","author":"Shilov Nikolay V.","year":"2002","unstructured":"Nikolay V. Shilov and Natalya Olegovna Garanina. 2002. Model checking knowledge and fixpoints. In FICS. 25\u201339."},{"issue":"1","key":"e_1_3_2_55_2","first-page":"347","article-title":"Update and abstraction in model checking of knowledge and branching time","volume":"72","author":"Shilov Nikolay V.","year":"2006","unstructured":"Nikolay V. Shilov, Natalya Olegovna Garanina, and K.-M. Choe. 2006. Update and abstraction in model checking of knowledge and branching time. Fundam. Inform. 72, 1-3 (2006), 347\u2013361.","journal-title":"Fundam. Inform."},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026185103185"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2679"},{"key":"e_1_3_2_59_2","volume-title":"Personal communication","author":"Meyden Ron van der","year":"2020","unstructured":"Ron van der Meyden. 2020. Personal communication."},{"key":"e_1_3_2_60_2","first-page":"432","volume-title":"FSTTCS","author":"Meyden Ron van der","year":"1999","unstructured":"Ron van der Meyden and Nikolay V. Shilov. 1999. Model checking knowledge and time in systems with perfect recall (extended abstract). In FSTTCS. 432\u2013445."},{"key":"e_1_3_2_61_2","first-page":"280","volume-title":"CSFW","author":"Meyden Ron van der","year":"2004","unstructured":"Ron van der Meyden and Kaile Su. 2004. Symbolic model checking the knowledge of the dining cryptographers. In CSFW. 280\u2013291."},{"key":"e_1_3_2_62_2","first-page":"34","volume-title":"CONCUR","author":"Meyden Ron van der","year":"1998","unstructured":"Ron van der Meyden and Moshe Y. Vardi. 1998. Synthesis from knowledge-based specifications. In CONCUR. Springer, 34\u201349."},{"key":"e_1_3_2_63_2","first-page":"562","volume-title":"CONCUR","author":"Meyden Ron Van der","year":"2005","unstructured":"Ron Van der Meyden and Thomas Wilke. 2005. Synthesis of distributed systems from knowledge-based specifications. In CONCUR, Vol. 5. Springer, 562\u2013576."},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3637212","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3637212","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:43:42Z","timestamp":1750290222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3637212"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,16]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1,31]]}},"alternative-id":["10.1145\/3637212"],"URL":"https:\/\/doi.org\/10.1145\/3637212","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2024,1,16]]},"assertion":[{"value":"2021-06-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-27","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}