{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,14]],"date-time":"2025-12-14T15:57:32Z","timestamp":1765727852089,"version":"3.37.3"},"reference-count":38,"publisher":"Oxford University Press (OUP)","issue":"2","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61472369"],"award-info":[{"award-number":["61472369"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,3,6]]},"DOI":"10.1093\/logcom\/exx038","type":"journal-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T11:10:03Z","timestamp":1509102603000},"page":"367-402","source":"Crossref","is-referenced-by-count":17,"title":["Symbolic model checking for Dynamic Epistemic Logic \u2014 S5 and beyond*"],"prefix":"10.1093","volume":"28","author":[{"given":"Johan","family":"van Benthem","sequence":"first","affiliation":[{"name":"Institute for Logic, Language & Computation, University of Amsterdam, Amsterdam, The Netherlands"},{"name":"Department of Philosophy, Stanford University, Stanford, USA"},{"name":"Changjiang scholars program, Tsinghua University, Beijing, China"}]},{"given":"Jan","family":"van Eijck","sequence":"additional","affiliation":[{"name":"Institute for Logic, Language & Computation, University of Amsterdam, Amsterdam, The Netherlands"},{"name":"Centrum Wiskunde & Informatica, Amsterdam, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2498-5073","authenticated-orcid":false,"given":"Malvin","family":"Gattinger","sequence":"additional","affiliation":[{"name":"Institute for Logic, Language & Computation, University of Amsterdam, Amsterdam, The Netherlands"}]},{"given":"Kaile","family":"Su","sequence":"additional","affiliation":[{"name":"Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia"},{"name":"Department of Computer Science, Jinan University, Guangzhou, China"}]}],"member":"286","published-online":{"date-parts":[[2017,11,22]]},"reference":[{"key":"key\n\t\t\t\t20180306103555_B1","first-page":"7","article-title":"On the complexity of Dynamic Epistemic Logic.","volume-title":"Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013)","author":"Aucher","year":"2013"},{"key":"key\n\t\t\t\t20180306103555_B2","first-page":"43","article-title":"The logic of public announcements, common knowledge, and private suspicions.","author":"Baltag","year":"1998","journal-title":"Proceedings of TARK\u201998"},{"key":"key\n\t\t\t\t20180306103555_B3","first-page":"366","article-title":"Symbolic model checking for Dynamic Epistemic Logic.","author":"van Benthem","year":"2015","journal-title":"Proceedings of The Fifth International Conference on Logic, Rationality and Interaction (LORI-V) in Taipei, Taiwan, October 28\u201330"},{"key":"key\n\t\t\t\t20180306103555_B4","doi-asserted-by":"crossref","first-page":"1620","DOI":"10.1016\/j.ic.2006.04.006","article-title":"Logics of communication and change.","volume":"204","author":"van Benthem","year":"2006","journal-title":"Information and Computation"},{"key":"key\n\t\t\t\t20180306103555_B5","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/s10992-008-9099-x","article-title":"Merging frameworks for interaction.","volume":"38","author":"van Benthem","year":"2009","journal-title":"Journal of Philosophical Logic"},{"key":"key\n\t\t\t\t20180306103555_B6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume":"Vol. 53","author":"Blackburn","year":"2001","journal-title":"Modal Logic"},{"key":"key\n\t\t\t\t20180306103555_B7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-Based Algorithms for Boolean Function Manipulation.","volume":"C-35","author":"Bryant.","year":"1986","journal-title":"IEEE Transaction on Computers"},{"key":"key\n\t\t\t\t20180306103555_B8","first-page":"1471","article-title":"Arbitrary public announcement logic with mental programs.","author":"Charrier","year":"2015","journal-title":"Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems"},{"key":"key\n\t\t\t\t20180306103555_B9","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BF00206326","article-title":"The Dining Cryptographers problem: unconditional sender and recipient untraceability.","volume":"1","author":"Chaum.","year":"1988","journal-title":"Journal of Cryptology"},{"volume-title":"Model Checking","year":"1999","author":"Clarke","key":"key\n\t\t\t\t20180306103555_B10"},{"key":"key\n\t\t\t\t20180306103555_B11","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction.","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM transactions on Programming Languages and Systems"},{"key":"key\n\t\t\t\t20180306103555_B12","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s10623-013-9855-y","article-title":"A geometric protocol for cryptography with cards.","volume":"74","author":"Cord\u00f3n-Franco","year":"2015","journal-title":"Designs, Codes and Cryptography"},{"key":"key\n\t\t\t\t20180306103555_B13","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1023\/A:1026168632319","article-title":"The Russian Cards problem.","volume":"75","author":"van Ditmarsch.","year":"2003","journal-title":"Studia Logica"},{"volume-title":"Dynamic Epistemic Logic","year":"2007","author":"van Ditmarsch","key":"key\n\t\t\t\t20180306103555_B14"},{"key":"key\n\t\t\t\t20180306103555_B15","first-page":"105","article-title":"Model Checking Russian Cards.","volume":"Vol. 149","author":"van Ditmarsch","year":"2006","journal-title":"Proceedings of the Third Workshop on Model Checking and Artificial Intelligence (MoChArt 2005)"},{"key":"key\n\t\t\t\t20180306103555_B16","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1093\/jigpal\/jzr038","article-title":"Connecting Dynamic Epistemic and Temporal Epistemic Logics.","volume":"21","author":"van Ditmarsch","year":"2013","journal-title":"Logic Journal of IGPL"},{"article-title":"Secure aggregation of distributed information.","year":"2014","author":"Duque","key":"key\n\t\t\t\t20180306103555_B17"},{"key":"key\n\t\t\t\t20180306103555_B18","first-page":"303","article-title":"DEMO\u2014a demo of epistemic modelling.","volume":"vol. 1","author":"van Eijck.","year":"2007","journal-title":"Interactive Logic. Selected Papers from the 7th Augustus de Morgan Workshop, London"},{"key":"key\n\t\t\t\t20180306103555_B19","article-title":"DEMO-S5.","volume-title":"Technical Report","author":"van Eijck.","year":"2014"},{"key":"key\n\t\t\t\t20180306103555_B20","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-319-06025-5_7","article-title":"Dynamic Epistemic Logics.","volume-title":"Johan van Benthem on Logic and Information Dynamics","author":"van Eijck.","year":"2014"},{"key":"key\n\t\t\t\t20180306103555_B21","first-page":"159","article-title":"Epistemic verification of anonymity.","volume":"Vol. 168","author":"van Eijck","year":"2007","journal-title":"Proceedings of the Second International Workshop on Views on Designing Complex Architectures (VODCA 2006)"},{"key":"key\n\t\t\t\t20180306103555_B22","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/s11229-012-0083-1","article-title":"Action emulation.","volume":"185","author":"van Eijck","year":"2012","journal-title":"Synthese"},{"key":"key\n\t\t\t\t20180306103555_B23","first-page":"68","article-title":"Cooperative epistemic multi-agent planning with implicit coordination.","author":"Engesser","year":"2015","journal-title":"Distributed and Multi-Agent Planning (DMAP-15)"},{"key":"key\n\t\t\t\t20180306103555_B24","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"Fagin","year":"1995"},{"key":"key\n\t\t\t\t20180306103555_B25","first-page":"152","article-title":"Formulering van het \u2018som-en-product\u2019-probleem.","volume":"17","author":"Freudenthal.","year":"1969","journal-title":"Nieuw Archief voor Wiskunde"},{"year":"2016","author":"Gattinger.","key":"key\n\t\t\t\t20180306103555_B26"},{"key":"key\n\t\t\t\t20180306103555_B27","first-page":"257","article-title":"A note on a generalization of the Muddy Children puzzle.","volume-title":"TARK\u201911","author":"Gierasimczuk","year":"2011"},{"key":"key\n\t\t\t\t20180306103555_B28","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1023\/A:1014610426691","article-title":"Implementation of belief change operators using BDDs.","volume":"70","author":"Gorogiannis","year":"2002","journal-title":"Studia Logica"},{"key":"key\n\t\t\t\t20180306103555_B29","article-title":"The Art of Computer Programming.","volume":"vol. 4A.","author":"Knuth.","year":"2011","journal-title":"Combinatorial Algorithms, Part 1"},{"volume-title":"A Mathematician\u2019s Miscellany","year":"1953","author":"Littlewood.","key":"key\n\t\t\t\t20180306103555_B30"},{"key":"key\n\t\t\t\t20180306103555_B31","first-page":"1","article-title":"MCMAS: an open-source model checker for the verification of multi-agent systems.","author":"Lomuscio","year":"2015","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"key\n\t\t\t\t20180306103555_B32","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1145\/359496.359527","article-title":"Knowledge in Multiagent Systems: Initial Configurations and Broadcast.","volume":"1","author":"Lomuscio","year":"2000","journal-title":"ACM Transactions on Computational Logic"},{"key":"key\n\t\t\t\t20180306103555_B33","first-page":"630","article-title":"Solving sum and product riddle via BDD-based model checking.","author":"Luo","year":"2008","journal-title":"Web Intel.\/IAT Workshops"},{"key":"key\n\t\t\t\t20180306103555_B34","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/978-3-642-39799-8_15","article-title":"CacBDD: A BDD Package with dynamic cache management.","volume-title":"Proceedings of the 25th International Conference on Computer Aided Verification (CAV\u201913)","author":"Lv","year":"2013"},{"key":"key\n\t\t\t\t20180306103555_B35","first-page":"280","article-title":"Symbolic Model Checking the Knowledge of the Dining Cryptographers.","volume-title":"CSFW","author":"van der Meyden","year":"2004"},{"year":"2016","author":"O\u2019Sullivan.","key":"key\n\t\t\t\t20180306103555_B36"},{"year":"2012","author":"Somenzi.","key":"key\n\t\t\t\t20180306103555_B37"},{"key":"key\n\t\t\t\t20180306103555_B38","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1093\/comjnl\/bxm009","article-title":"Model checking temporal logics of knowledge via OBDDs.","volume":"50","author":"Su","year":"2007","journal-title":"The Computer Journal"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/28\/2\/367\/24261865\/exx038.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T02:49:52Z","timestamp":1719542992000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/28\/2\/367\/4653527"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,22]]},"references-count":38,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2017,11,22]]},"published-print":{"date-parts":[[2018,3,6]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exx038","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2018,3]]},"published":{"date-parts":[[2017,11,22]]}}}