{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,5]],"date-time":"2026-08-05T02:04:41Z","timestamp":1785895481783,"version":"3.56.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T00:00:00Z","timestamp":1781308800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA23862114029"],"award-info":[{"award-number":["FA23862114029"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008812","name":"Defence Science and Technology Group","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100008812","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,16]]},"DOI":"10.1145\/3732772.3733552","type":"proceedings-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T14:23:34Z","timestamp":1749824614000},"page":"131-140","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking and Synthesis for Optimal Use of Knowledge in Consensus Protocols"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4843-883X","authenticated-orcid":false,"given":"Kaya","family":"Alpturer","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1014-2567","authenticated-orcid":false,"given":"Gerald","family":"Huang","sequence":"additional","affiliation":[{"name":"University of Melbourne, Melbourne, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9243-0571","authenticated-orcid":false,"given":"Ron","family":"van der Meyden","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"SYNT workshop series. https:\/\/cgi.csc.liv.ac.uk\/~sven\/synt\/.","unstructured":"2012-2024. SYNT workshop series. https:\/\/cgi.csc.liv.ac.uk\/~sven\/synt\/."},{"key":"e_1_3_2_1_2_1","volume-title":"Proc. 16th Int. Colloquium on Automata, Languages and Programming","volume":"372","author":"Abadi M.","unstructured":"M. Abadi, L. Lamport, and P. Wolper. 1989. Realizable and Unrealizable Concurrent Program Specifications. In Proc. 16th Int. Colloquium on Automata, Languages and Programming, Vol. 372. Lecture Notes in Computer Science, Springer-Verlag, 1\u201317."},{"key":"e_1_3_2_1_3_1","volume-title":"PODC '86: Proc. 5th ACM symposium on Principles of Distributed Computing. 263\u2013271","author":"Afrati F.","unstructured":"F. Afrati, C. Papadimitriou, and G. Papageorgiou. 1986. The synthesis of communication protocols. In PODC '86: Proc. 5th ACM symposium on Principles of Distributed Computing. 263\u2013271."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/FORMALISE.2019.00014"},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. SecureComm. 429\u2013447","author":"Al-Bataineh O. I.","unstructured":"O. I. Al-Bataineh and R. van der Meyden. 2010. Epistemic Model Checking for Knowledge-Based Program Implementation: An Application to Anonymous Broadcast. In Proc. SecureComm. 429\u2013447."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583668.3594573"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"K. Alpturer G. Huang and R. van der Meyden. 2025. Model Checking and Synthesis for Optimal Use of Knowledge in Consensus Protocols. Full version of the PODC'25 paper. 10.48550\/arXiv.2505.02353","DOI":"10.48550\/arXiv.2505.02353"},{"key":"e_1_3_2_1_8_1","volume-title":"Conf. on Theoretical Aspects of Rationality and Knowledge, TARK","author":"Alpturer K.","year":"2025","unstructured":"K. Alpturer, R. van der Meyden, S. Ruj, and G. Wong. 2025. Optimality of Simultaneous Byzantine Agreement with Limited Information Exchange. (2025). to appear, Conf. on Theoretical Aspects of Rationality and Knowledge, TARK, July 2025."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"A. Anuchitanukul and Z. Manna. 1994. Realizability and Synthesis of Reactive Modules. In Computer-Aided Verification Proc. 6th Int'l Conference. SpringerVerlag Lecture Notes in Computer Science 818 Stanford California 156\u2013169.","DOI":"10.1007\/3-540-58179-0_51"},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. 16th ACM Symposium on Principles of Programming Languages","author":"Attie P. C.","unstructured":"P. C. Attie and E.A. Emerson. 1989. Synthesis of Concurrent Systems with Many Similar Sequential Processes. In Proc. 16th ACM Symposium on Principles of Programming Languages. Austin, 191\u2013201."},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. ICFEM. 99\u2013114","author":"Baukus K.","unstructured":"K. Baukus and R. van der Meyden. 2004. A Knowledge Based Analysis of Cache Coherence. In Proc. ICFEM. 99\u2013114."},{"key":"e_1_3_2_1_12_1","volume-title":"Essays in Memory of Amir Pnueli (Lecture Notes in Computer Science","volume":"41","author":"Bensalem S.","unstructured":"S. Bensalem, D. Peled, and J. Sifakis. 2010. Knowledge Based Scheduling of Distributed Systems. In Time for Verification, Essays in Memory of Amir Pnueli (Lecture Notes in Computer Science, Vol. 6200). Springer, 26\u201341."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. 28th International Conference on Distributed Computing (DISC '14)","author":"Casta\u00f1eda A.","unstructured":"A. Casta\u00f1eda, Y. A. Gonczorowski, and Y. Moses. 2014. Unbeatable consensus. In Proc. 28th International Conference on Distributed Computing (DISC '14). 91\u2013106."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59647-1_16"},{"key":"e_1_3_2_1_16_1","unstructured":"E. Clarke O. Grumberg and D. Peled. 1999. Model Checking. The MIT Press."},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. Conf. Tools and Algorithms for the Construction and Analysis of Systems. 278\u2013283","author":"Dembinski P.","unstructured":"P. Dembinski, A. Janowska, P. Janowski, W. Penczek, A. P\u00f3lrola, M. Szreter, B. Wozna, and A. Zbrzezny. 2003. Verics: A Tool for Verifying Timed Automata and Estelle Specifications. In Proc. Conf. Tools and Algorithms for the Construction and Analysis of Systems. 278\u2013283."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/96559.96565"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90014-9"},{"key":"e_1_3_2_1_20_1","unstructured":"R. Fagin J.Y. Halpern Y. Moses and M.Y. Vardi. 2003. Reasoning About Knowledge. The MIT Press."},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. Conf. on Computer Aided Verification (CAV) (LNCS","volume":"483","author":"Gammie P.","unstructured":"P. Gammie and R. van der Meyden. 2004. MCK: Model Checking the Logic of Knowledge.. In Proc. Conf. on Computer Aided Verification (CAV) (LNCS, Vol. 3114), Rajeev Alur and Doron Peled (Eds.). Springer, 479\u2013483."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0138-9"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798340217"},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. IJCAI. 240\u2013245","author":"Huang X.","unstructured":"X. Huang, P. Maupin, and R. van der Meyden. 2011. Model Checking Knowledge in Pursuit Evasion Games. In Proc. IJCAI. 240\u2013245."},{"key":"e_1_3_2_1_26_1","volume-title":"Proc. TARK. 121\u2013130","author":"Huang X.","unstructured":"X. Huang and R. van der Meyden. 2013. Symbolic Synthesis of Knowledge-based Program Implementations with Synchronous Semantics. In Proc. TARK. 121\u2013130."},{"key":"e_1_3_2_1_27_1","volume-title":"Proc. TARK.","author":"Huang X.","unstructured":"X. Huang and R. van der Meyden. 2013. Symbolic Synthesis of Knowledge-based Program Implementations with Synchronous Semantics. In Proc. TARK."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_39"},{"key":"e_1_3_2_1_29_1","volume-title":"Proc. TACAS. 455\u2013469","author":"Huang X.","unstructured":"X. Huang and R. van der Meyden. 2014. Symbolic Synthesis for Epistemic Specifications with Observational Semantics. In Proc. TACAS. 455\u2013469."},{"key":"e_1_3_2_1_30_1","volume-title":"Proc. Workshop on Synthesis, SYNT. 120\u2013137","author":"Huang X.","unstructured":"X. Huang and R. van der Meyden. 2015. The complexity of approximations for epistemic synthesis (extended abstract). In Proc. Workshop on Synthesis, SYNT. 120\u2013137."},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. Int. Conf on Computer Aided Verification. 510\u2013525","author":"Katz G.","unstructured":"G. Katz, D. Peled, and S. Schewe. 2011. Synthesis of Distributed Control through Knowledge Accumulation. In Proc. Int. Conf on Computer Aided Verification. 510\u2013525."},{"key":"e_1_3_2_1_32_1","volume-title":"Proc. Conf. on Computer Aided Verification (CAV) (Lecture Notes in Computer Science","volume":"688","author":"Lomuscio A.","unstructured":"A. Lomuscio, H. Qu, and F. Raimondi. 2009. MCMAS: A Model Checker for the Verification of Multi-Agent Systems.. In Proc. Conf. on Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 5643), Ahmed Bouajjani and Oded Maler (Eds.). Springer, 682\u2013688."},{"key":"e_1_3_2_1_33_1","volume-title":"Distributed Algorithms","author":"Lynch N.","unstructured":"N. Lynch. 1996. Distributed Algorithms. MIT Press."},{"key":"e_1_3_2_1_34_1","unstructured":"R. van der Meyden. 2024. Optimal Simultaneous Byzantine Agreement Common Knowledge and Limited Information Exchange. https:\/\/cgi.cse.unsw.edu.au\/~meyden\/research\/common-knowledge.pdf"},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. CSFW. 280\u2013291","author":"van der Meyden R.","unstructured":"R. van der Meyden and K. Su. 2004. Symbolic Model Checking the Knowledge of the Dining Cryptographers. In Proc. CSFW. 280\u2013291."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04355-0_45"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01762112"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322188"},{"key":"e_1_3_2_1_39_1","unstructured":"MCK Team. [n. d.]. MCK User Manual. Available from http:\/\/www.cse.unsw.edu.au\/~mck."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73582"}],"event":{"name":"PODC '25: ACM Symposium on Principles of Distributed Computing","location":"Hotel Las Brisas Huatulco Huatulco Mexico","acronym":"PODC '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the ACM Symposium on Principles of Distributed Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3732772.3733552","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3732772.3733552","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T14:25:18Z","timestamp":1749824718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3732772.3733552"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,13]]},"references-count":40,"alternative-id":["10.1145\/3732772.3733552","10.1145\/3732772"],"URL":"https:\/\/doi.org\/10.1145\/3732772.3733552","relation":{},"subject":[],"published":{"date-parts":[[2025,6,13]]},"assertion":[{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}