{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:13:01Z","timestamp":1784232781558,"version":"3.55.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,12,27]],"date-time":"2024-12-27T00:00:00Z","timestamp":1735257600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>We give a general-purpose programming language in which programs can reason about their own knowledge. To specify what these intelligent programs know, we define a \u201cprogram epistemic\u201d logic, akin to a dynamic epistemic logic for programs. Our logic properties are complex, including programs introspecting into future state of affairs, i.e., reasoning now about facts that hold only after they and other threads will execute. To model aspects anchored in privacy, our logic is interpreted over partial observability of variables, thus capturing that each thread can \u201csee\u201d only a part of the global space of variables. We verify program-epistemic properties on such AI-centred programs. To this end, we give a sound translation of the validity of our program-epistemic logic into first-order validity, using a new weakest-precondition semantics and a book-keeping of variable assignment. We implement our translation and fully automate our verification method for well-established examples using SMT solvers.<\/jats:p>","DOI":"10.1145\/3700150","type":"journal-article","created":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T11:15:58Z","timestamp":1728645358000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["An SMT-Based Approach to the Verification of Knowledge-Based Programs"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7768-1794","authenticated-orcid":false,"given":"Francesco","family":"Belardinelli","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-777X","authenticated-orcid":false,"given":"Ioana","family":"Boureanu","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6138-4229","authenticated-orcid":false,"given":"Vadim","family":"Malvone","sequence":"additional","affiliation":[{"name":"T\u00e9l\u00e9com Paris, Institut Polytechnique de Paris, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4902-9800","authenticated-orcid":false,"given":"Fortunat","family":"Rajaona","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,12,27]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"[n. d.]. Pit Game Rules. Retrieved from https:\/\/www.hasbro.com\/common\/instruct\/pit.pdf"},{"key":"e_1_3_3_3_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.24"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/645876.671885"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V37I5.25769"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/381193"},{"key":"e_1_3_3_8_2","volume-title":"Handbook of Modal Logic","author":"Blackburn Patrick","year":"2006","unstructured":"Patrick Blackburn, Johan FAK van Benthem, and Frank Wolter. 2006. Handbook of Modal Logic. Elsevier."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/2343776.2343860"},{"key":"e_1_3_3_10_2","first-page":"268","volume-title":"15th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201916)","author":"Charrier Tristan","year":"2016","unstructured":"Tristan Charrier, Andreas Herzig, Emiliano Lorini, Faustine Maffre, and Fran\u00e7ois Schwarzentruber. 2016. Building epistemic logic from observations and public announcements. In 15th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201916). AAAI Press, 268\u2013277."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00206326"},{"key":"e_1_3_3_12_2","first-page":"1218","volume-title":"Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201916)","author":"Cimatti A.","year":"2016","unstructured":"A. Cimatti, M. Gario, and S. Tonetta. 2016. A lazy approach to temporal epistemic logic model checking. In Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201916). IFAAMAS, 1218\u20131226."},{"key":"e_1_3_3_13_2","first-page":"854","volume-title":"23rd International Joint Conference on Artificial Intelligence (IJCAI\u201913)","author":"Giacomo Giuseppe De","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In 23rd International Joint Conference on Artificial Intelligence (IJCAI\u201913). AAAI Press, Beijing, China, 854\u2013860."},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_15_2","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","year":"1976","unstructured":"E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_3_3_16_2","first-page":"1659","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI\u201911)","author":"Ezekiel J.","year":"2011","unstructured":"J. Ezekiel, A. Lomuscio, L. Molnar, S. Veres, and M. Pebody. 2011. Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle. In International Joint Conference on Artificial Intelligence (IJCAI\u201911). AAAI Press, 1659\u20131664."},{"key":"e_1_3_3_17_2","first-page":"153","volume-title":"Symposium on Principles of Distributed Computing","author":"Fagin Ronald","year":"1995","unstructured":"Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. 1995. Knowledge-based programs. In Symposium on Principles of Distributed Computing. 153\u2013163."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/30"},{"key":"e_1_3_3_20_2","volume-title":"26th International Joint Conference on Artificial Intelligence (IJCAI\u201917)","author":"Grossi Davide","year":"2017","unstructured":"Davide Grossi, Andreas Herzig, W. van der Hoek, and Christos Moyzes. 2017. Non-determinism and the dynamics of knowledge. In 26th International Joint Conference on Artificial Intelligence (IJCAI\u201917)."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exv086"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-6259-0_10"},{"key":"e_1_3_3_23_2","volume-title":"Knowledge and Belief","author":"Hintikka J.","year":"1962","unstructured":"J. Hintikka. 1962. Knowledge and Belief. Cornell University Press."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"issue":"1","key":"e_1_3_3_25_2","first-page":"215","article-title":"Comparing BDD and SAT based techniques for model checking Chaum\u2019s dining cryptographers protocol","volume":"72","author":"Kacprzak M.","year":"2006","unstructured":"M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, and M. Szreter. 2006. Comparing BDD and SAT based techniques for model checking Chaum\u2019s dining cryptographers protocol. Fundam. Inform. 72, 1\u20133 (2006), 215\u2013234.","journal-title":"Fundam. Inform."},{"issue":"1","key":"e_1_3_3_26_2","doi-asserted-by":"crossref","first-page":"313","DOI":"10.3233\/FUN-2008-851-422","article-title":"VerICS 2007\u2014A model checker for knowledge and real-time","volume":"85","author":"Kacprzak M.","year":"2008","unstructured":"M. Kacprzak, W. Nabia\u0142ek, A. Niewiadomski, W. Penczek, A. P\u00f3\u0142rola, M. Szreter, B. Wo\u017ana, and A. Zbrzezny. 2008. VerICS 2007\u2014A model checker for knowledge and real-time. Fundam. Inform. 85, 1\u20134 (2008), 313\u2013328.","journal-title":"Fundam. Inform."},{"key":"e_1_3_3_27_2","first-page":"62","volume-title":"3rd ACM Symposium on Principles of Distributed Computing","author":"Lehman D.","year":"1984","unstructured":"D. Lehman. 1984. Knowledge, common knowledge, and related puzzles. In 3rd ACM Symposium on Principles of Distributed Computing. 62\u201367."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0378-x"},{"key":"e_1_3_3_29_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-642-03466-4_3","volume-title":"Theoretical Aspects of Computing","author":"McIver Annabelle K.","year":"2009","unstructured":"Annabelle K. McIver. 2009. The secret art of computer programming. In Theoretical Aspects of Computing(Lecture Notes in Computer Science, Vol. 5684). Springer, 61\u201378."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/184737"},{"key":"e_1_3_3_31_2","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/11783596_21","volume-title":"Mathematics of Program Construction (Lecture Notes in Computer Science)","author":"Morgan C. C.","year":"2006","unstructured":"C. C. Morgan. 2006. The shadow knows: Refinement of ignorance in sequential programs. In Mathematics of Program Construction (Lecture Notes in Computer Science), Vol. 4014. Springer, 359\u2013378."},{"key":"e_1_3_3_32_2","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-15648-8_21","article-title":"Distributed processing and the logic of knowledge.","volume":"193","author":"Parikh R.","year":"1985","unstructured":"R. Parikh and R. Ramanujam. 1985. Distributed processing and the logic of knowledge. Lecture Notes in Computer Science 193. Springer, 256\u2013268.","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_3_3_33_2","article-title":"Logics of public communications","author":"Plaza J. A.","year":"1989","unstructured":"J. A. Plaza. 1989. Logics of public communications. In 4th International Symposium on Methodologies for Intelligent Systems.","journal-title":"4th International Symposium on Methodologies for Intelligent Systems"},{"key":"e_1_3_3_34_2","first-page":"109","volume-title":"17th Annual Symposium on Foundations of Computer Science","author":"Pratt V. R.","year":"1976","unstructured":"V. R. Pratt. 1976. Semantical considerations on Floyd-Hoare logic. In 17th Annual Symposium on Foundations of Computer Science. IEEE, 109\u2013121."},{"key":"e_1_3_3_35_2","volume-title":"An Algebraic Framework for Reasoning about Privacy","author":"Rajaona Solofomampionona Forunat","year":"2016","unstructured":"Solofomampionona Forunat Rajaona. 2016. An Algebraic Framework for Reasoning about Privacy. Ph. D. Dissertation. University of Stellenbosch, Stellenbosch."},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_27"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_3_38_2","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/978-3-662-48561-3_30","volume-title":"International Workshop on Logic, Rationality and Interaction","author":"Benthem Johan Van","year":"2015","unstructured":"Johan Van Benthem, Jan Van Eijck, Malvin Gattinger, and Kaile Su. 2015. Symbolic model checking for dynamic epistemic logic. In International Workshop on Logic, Rationality and Interaction. Springer, 366\u2013378."},{"key":"e_1_3_3_39_2","first-page":"87","article-title":"Semantic results for ontic and epistemic change","author":"Ditmarsch Hans Van","year":"2008","unstructured":"Hans Van Ditmarsch and Barteld Kooi. 2008. Semantic results for ontic and epistemic change. In Logic and the Foundations of Game and Decision Theory (LOFT 7). Amsterdam University Press, 87\u2013117.","journal-title":"Logic and the Foundations of Game and Decision Theory (LOFT 7)"},{"key":"e_1_3_3_40_2","article-title":"Cheryl\u2019s birthday","author":"Ditmarsch Hans Pieter van","year":"2017","unstructured":"Hans Pieter van Ditmarsch, Michael Ian Hartley, Barteld Kooi, Jonathan Welton, and Joseph B. W. Yeo. 2017. Cheryl\u2019s birthday. arXiv preprint arXiv:1708.02654 (2017).","journal-title":"arXiv preprint arXiv:1708.02654"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.5555\/1535423"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1082473.1082495"},{"key":"e_1_3_3_43_2","article-title":"A demo of epistemic modelling","author":"Eijck Jan van","year":"2007","unstructured":"Jan van Eijck. 2007. A demo of epistemic modelling. Interact. Logic. https:\/\/www.jstor.org\/stable\/j.ctt45kdbf.15?Search=yes&resultItemClick=true&searchText=au%3A&searchText=%22Jan+van+Eijck%22&searchUri=%2Fopen%2Fsearch%2F%3Fpage%3D1%26amp%3BQuery%3Dau%253A%2522Jan%2Bvan%2BEijck%2522%26amp%3Bso%3Drel%26amp%3Bsi%3D1%26amp%3Btheme%3Dopen","journal-title":"Interact. Logic"},{"key":"e_1_3_3_44_2","unstructured":"S. Wang. 2016. Dynamic Epistemic Model Checking with Yices. Retrieved from https:\/\/github.com\/airobert\/DEL\/blob\/master\/report.pdf"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/9.2.257"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3700150","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3700150","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:09:50Z","timestamp":1750295390000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3700150"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,27]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3700150"],"URL":"https:\/\/doi.org\/10.1145\/3700150","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,27]]},"assertion":[{"value":"2024-02-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-24","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}