{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T09:57:10Z","timestamp":1785319030595,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662485606","type":"print"},{"value":"9783662485613","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48561-3_30","type":"book-chapter","created":{"date-parts":[[2015,10,28]],"date-time":"2015-10-28T17:39:12Z","timestamp":1446053952000},"page":"366-378","source":"Crossref","is-referenced-by-count":16,"title":["Symbolic Model Checking for Dynamic Epistemic Logic"],"prefix":"10.1007","author":[{"given":"Johan","family":"van Benthem","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"van Eijck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Malvin","family":"Gattinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kaile","family":"Su","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,19]]},"reference":[{"key":"30_CR1","unstructured":"Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: Bilboa, I. (ed.) TARK 1998, pp. 43\u201356 (1998)"},{"issue":"11","key":"30_CR2","doi-asserted-by":"publisher","first-page":"1620","DOI":"10.1016\/j.ic.2006.04.006","volume":"204","author":"J. Benthem van","year":"2006","unstructured":"van Benthem, J., van Eijck, J., Kooi, B.: Logics of communication and change. Information and Computation\u00a0204(11), 1620\u20131662 (2006)","journal-title":"Information and Computation"},{"issue":"5","key":"30_CR3","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/s10992-008-9099-x","volume":"38","author":"J. Benthem van","year":"2009","unstructured":"van Benthem, J., Gerbrandy, J., Hoshi, T., Pacuit, E.: Merging frameworks for interaction. Journal of Philosophical Logic\u00a038(5), 491\u2013526 (2009)","journal-title":"Journal of Philosophical Logic"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. In: Cambridge Tracts in Theoretical Computer Science, no.\u00a053. CUP, Cambridge (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transaction on Computers C-35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"30_CR6","unstructured":"Charrier, T., Schwarzentruber, F.: Arbitrary public announcement logic with mental programs. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, pp. 1471\u20131479. IFAAMAS (2015)"},{"issue":"1","key":"30_CR7","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D. Chaum","year":"1988","unstructured":"Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology\u00a01(1), 65\u201375 (1988)","journal-title":"Journal of Cryptology"},{"issue":"5","key":"30_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"30_CR9","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s10623-013-9855-y","volume":"74","author":"A. Cord\u00f3n-Franco","year":"2015","unstructured":"Cord\u00f3n-Franco, A., van Ditmarsch, H., Fern\u00e1ndez-Duque, D., Soler-Toscano, F.: A geometric protocol for cryptography with cards. Designs, Codes and Cryptography\u00a074(1), 113\u2013125 (2015), http:\/\/dx.doi.org\/10.1007\/s10623-013-9855-y","journal-title":"Designs, Codes and Cryptography"},{"issue":"1","key":"30_CR10","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1023\/A:1026168632319","volume":"75","author":"H. Ditmarsch van","year":"2003","unstructured":"van Ditmarsch, H.: The russian cards problem. Studia Logica\u00a075(1), 31\u201362 (2003)","journal-title":"Studia Logica"},{"key":"30_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5839-4","volume-title":"Dynamic epistemic logic","author":"H. Ditmarsch van","year":"2007","unstructured":"van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic epistemic logic, vol.\u00a01. Springer, Heidelberg (2007)"},{"issue":"2","key":"30_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.entcs.2005.07.029","volume":"149","author":"H. Ditmarsch van","year":"2006","unstructured":"van Ditmarsch, H., van der Hoek, W., van der Meyden, R., Ruan, J.: Model Checking Russian Cards. Electr. Notes Theor. Comput. Sci.\u00a0149(2), 105\u2013123 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"30_CR13","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1093\/jigpal\/jzr038","volume":"21","author":"H. Ditmarsch van","year":"2013","unstructured":"van Ditmarsch, H., van der Hoek, W., Ruan, J.: Connecting dynamic epistemic and temporal epistemic logics. Logic Journal of IGPL\u00a021(3), 380\u2013403 (2013)","journal-title":"Logic Journal of IGPL"},{"key":"30_CR14","unstructured":"Duque, D.F., Goranko, V.: Secure aggregation of distributed information. CoRR abs\/1407.7582 (2014), http:\/\/arxiv.org\/abs\/1407.7582"},{"key":"30_CR15","unstructured":"van Eijck, J.: DEMO-S5. Tech. rep., CWI (2014)"},{"issue":"1","key":"30_CR16","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/s11229-012-0083-1","volume":"185","author":"J. Eijck van","year":"2012","unstructured":"van Eijck, J., Ruan, J., Sadzik, T.: Action emulation. Synthese\u00a0185(1), 131\u2013151 (2012)","journal-title":"Synthese"},{"key":"30_CR17","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge, vol.\u00a04. MIT Press, Cambridge (1995)"},{"key":"30_CR18","unstructured":"Gammie, P.: hBDD. https:\/\/github.com\/peteg\/hBDD (2011, updated 2014)"},{"key":"30_CR19","unstructured":"Gattinger, M.: HasCacBDD (2015), https:\/\/github.com\/m4lvin\/HasCacBDD"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Gierasimczuk, N., Szymanik, J.: A note on a generalization of the Muddy Children puzzle. In: Apt, K.R. (ed.) TARK 2011, pp. 257\u2013264. ACM (2011)","DOI":"10.1145\/2000378.2000409"},{"issue":"1","key":"30_CR21","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1023\/A:1014610426691","volume":"70","author":"N. Gorogiannis","year":"2002","unstructured":"Gorogiannis, N., Ryan, M.D.: Implementation of Belief Change Operators Using BDDs. Studia Logica\u00a070(1), 131\u2013156 (2002)","journal-title":"Studia Logica"},{"key":"30_CR22","unstructured":"Knuth, D.E.: The Art of Computer Programming. Combinatorial Algorithms, Part 1, vol.\u00a04A. Addison-Wesley Professional (2011)"},{"key":"30_CR23","volume-title":"A Mathematician\u2019s Miscellany","author":"J. Littlewood","year":"1953","unstructured":"Littlewood, J.: A Mathematician\u2019s Miscellany. Methuen, London (1953)"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 1\u201322 (2015)","DOI":"10.1007\/s10009-015-0378-x"},{"issue":"2","key":"30_CR25","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1145\/359496.359527","volume":"1","author":"A.R. Lomuscio","year":"2000","unstructured":"Lomuscio, A.R., van der Meyden, R., Ryan, M.: Knowledge in Multiagent Systems: Initial Configurations and Broadcast. ACM Trans. Comp. L.\u00a01(2), 247\u2013284 (2000)","journal-title":"ACM Trans. Comp. L."},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Luo, X., Su, K., Sattar, A., Chen, Y.: Solving Sum and Product Riddle via BDD-Based Model Checking. In: Web Intel.\/IAT Workshops, pp. 630\u2013633. IEEE (2008)","DOI":"10.1109\/WIIAT.2008.277"},{"key":"30_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39799-8_15","volume-title":"Computer Aided Verification","author":"G. Lv","year":"2013","unstructured":"Lv, G., Su, K., Xu, Y.: CacBDD: A BDD Package with Dynamic Cache Management. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 229\u2013234. Springer, Heidelberg (2013)"},{"key":"30_CR28","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., Su, K.: Symbolic Model Checking the Knowledge of the Dining Cryptographers. In: CSFW, pp. 280\u2013291. IEEE Computer Society (2004)","DOI":"10.1109\/CSFW.2004.1310747"},{"key":"30_CR29","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.5.0 (2012)"},{"issue":"4","key":"30_CR30","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1093\/comjnl\/bxm009","volume":"50","author":"K. Su","year":"2007","unstructured":"Su, K., Sattar, A., Luo, X.: Model Checking Temporal Logics of Knowledge Via OBDDs. The Computer Journal\u00a050(4), 403\u2013420 (2007)","journal-title":"The Computer Journal"}],"container-title":["Lecture Notes in Computer Science","Logic, Rationality, and Interaction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48561-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T06:14:18Z","timestamp":1748672058000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48561-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662485606","9783662485613"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48561-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}