{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,14]],"date-time":"2025-12-14T15:57:44Z","timestamp":1765727864763},"reference-count":43,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,12,31]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We study the symbolic model checking problem against public announcement protocol logic (PAPL), featuring protocols with public announcements, arbitrary public announcements and group announcements. Technically, symbolic models are Kripke models whose accessibility relations are presented as programs described in a dynamic logic style with propositional assignments. We highlight the relevance of such symbolic models and show that the symbolic model checking problem against PAPL is A$_{\\textrm{pol}}$Exptime-complete as soon as announcement protocols allow for either arbitrary announcements or iteration of public announcements. However, when both options are discarded, the complexity drops to Pspace-complete.<\/jats:p>","DOI":"10.1093\/logcom\/exz023","type":"journal-article","created":{"date-parts":[[2019,9,4]],"date-time":"2019-09-04T19:28:51Z","timestamp":1567625331000},"page":"1211-1249","source":"Crossref","is-referenced-by-count":5,"title":["Symbolic model checking of public announcement protocols"],"prefix":"10.1093","volume":"29","author":[{"given":"Tristan","family":"Charrier","sequence":"first","affiliation":[{"name":"Univ Rennes, CNRS, IRISA, 35042 Rennes Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sophie","family":"Pinchinat","sequence":"additional","affiliation":[{"name":"Univ Rennes, CNRS, IRISA, 35042 Rennes Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00c7ois","family":"Schwarzentruber","sequence":"additional","affiliation":[{"name":"Univ Rennes, CNRS, IRISA, 35042 Rennes Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2019,12,10]]},"reference":[{"key":"2020012603564417500_ref1","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1016\/j.jal.2008.12.002","article-title":"Group announcement logic","volume":"8","author":"Agotnes","year":"2010","journal-title":"Journal of Applied Logics"},{"key":"2020012603564417500_ref2","first-page":"1","article-title":"Boolean games with epistemic goals","volume-title":"Logic, Rationality, and Interaction\u20144th International Workshop, LORI 2013, Hangzhou, China, October 9\u201312, 2013","author":"Agotnes","year":"2013"},{"key":"2020012603564417500_ref3","first-page":"893","article-title":"The undecidability of group announcements","volume-title":"International Conference on Autonomous Agents and Multi-Agent Systems, AAMAS\u201914, Paris, France, May 5\u20139, 2014","author":"Agotnes","year":"2014"},{"key":"2020012603564417500_ref4","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","article-title":"Binary decision diagrams","volume":"6","author":"Akers","year":"1978","journal-title":"IEEE Transactions on Computers"},{"key":"2020012603564417500_ref5","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"Journal of the ACM"},{"key":"2020012603564417500_ref6","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"2020012603564417500_ref7","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/1324249.1324259","article-title":"What can we achieve by arbitrary announcements? A dynamic take on Fitch\u2019s knowability","volume-title":"TARK","author":"Balbiani","year":"2007"},{"key":"2020012603564417500_ref8","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1093\/jigpal\/jzs052","article-title":"Agents that look at one another","volume":"21","author":"Balbiani","year":"2013","journal-title":"Logic Journal of the IGPL"},{"key":"2020012603564417500_ref9","article-title":"DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE","author":"Balbiani","year":"2014"},{"key":"2020012603564417500_ref10","first-page":"143","article-title":"Dynamic logic of propositional assignments: a well-behaved variant of PDL","volume-title":"LICS","author":"Balbiani","year":"2013"},{"key":"2020012603564417500_ref11","article-title":"The logic of public announcements, common knowledge, and private suspicions","volume-title":"Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge","author":"Baltag","year":"1998"},{"key":"2020012603564417500_ref12","first-page":"120","article-title":"The complexity of one-agent refinement modal logic","volume-title":"JELIA","author":"Bozzelli","year":"2012"},{"key":"2020012603564417500_ref13","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"2020012603564417500_ref14","first-page":"98","article-title":"Alternation","volume-title":"Proc. of FOCS\u201976","author":"Chandra","year":"1976"},{"key":"2020012603564417500_ref15","article-title":"Building epistemic logic from observations and public announcements","volume-title":"International Conference on Principles of Knowledge Representation and Reasoning (KR)","author":"Charrier","year":"2016"},{"key":"2020012603564417500_ref16","first-page":"133","article-title":"Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment","volume-title":"Dynamic Logic. New Trends and Applications\u2014First International Workshop, DALI 2017, Brasilia, Brazil, September 23\u201324, 2017","author":"Charrier","year":"2017"},{"key":"2020012603564417500_ref17","first-page":"1471","article-title":"Arbitrary public announcement logic with mental programs","volume-title":"Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4\u20138, 2015","author":"Charrier","year":"2015"},{"key":"2020012603564417500_ref18","first-page":"123","article-title":"A succinct language for dynamic epistemic logic","volume-title":"Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, S\u00e3o Paulo, Brazil, May 8\u201312, 2017","author":"Charrier","year":"2017"},{"key":"2020012603564417500_ref19","first-page":"151","article-title":"The complexity of theorem-proving procedures","volume-title":"Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3\u20135, 1971","author":"Cook","year":"1971"},{"key":"2020012603564417500_ref20","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/s004460050038","article-title":"Knowledge-based programs","volume":"10","author":"Fagin","year":"1997","journal-title":"Distributed Computing"},{"key":"2020012603564417500_ref21","volume-title":"Reasoning About Knowledge","author":"Fagin","year":"2003"},{"key":"2020012603564417500_ref22","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"Journal of Computer and System Sciences"},{"key":"2020012603564417500_ref23","first-page":"23","article-title":"Undecidability for arbitrary public announcement logic","volume-title":"Advances in Modal Logic","author":"French","year":"2008"},{"key":"2020012603564417500_ref24","first-page":"1","article-title":"Big brother logic: visual-epistemic reasoning in stationary multi-agent systems","volume":"5","author":"Gasquet","year":"2015","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"2020012603564417500_ref25","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1023\/A:1008222603071","article-title":"Reasoning about information change","volume":"6","author":"Gerbrandy","year":"1997","journal-title":"Journal of Logic, Language and Information"},{"key":"2020012603564417500_ref26","first-page":"325","article-title":"Model checking vs. theorem proving: a manifesto","volume-title":"Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR'91). Cambridge, MA, USA, April 22-25, 1991. Morgan Kaufmann 1991, ISBN 1-55860-165-1","author":"Halpern","year":"1991"},{"key":"2020012603564417500_ref27","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-48561-3_13","article-title":"A poor man\u2019s epistemic logic based on propositional assignment and higher-order observation","volume-title":"Logic, Rationality, and Interaction\u20146th International Workshop, LORI 2015","author":"Herzig","year":"2015"},{"key":"2020012603564417500_ref28","first-page":"228","article-title":"A dynamic logic of normative systems","author":"Herzig","year":"2011","journal-title":"In IJCAI"},{"key":"2020012603564417500_ref29","first-page":"67","article-title":"A catalog of complexity classes","volume-title":"Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity (A)","author":"Johnson","year":"1990"},{"key":"2020012603564417500_ref30","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.jal.2005.08.002","article-title":"Model checking propositional dynamic logic with all extras","volume":"4","author":"Lange","year":"2006","journal-title":"Journal of Applied Logic"},{"key":"2020012603564417500_ref31","article-title":"Formalization of two puzzles involving knowledge","author":"McCarthy","year":"1987"},{"key":"2020012603564417500_ref32","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-1-4615-3190-6_3","volume-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"2020012603564417500_ref33","article-title":"Efficient representations for the modal logic S5","volume-title":"Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016","author":"Niveau","year":"2016"},{"key":"2020012603564417500_ref34","volume-title":"Computational Complexity","author":"Papadimitriou","year":"2003"},{"key":"2020012603564417500_ref35","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S0019-9958(86)80009-2","article-title":"A note on succinct representations of graphs","volume":"71","author":"Papadimitriou","year":"1986","journal-title":"Information and Control"},{"key":"2020012603564417500_ref36","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s11229-007-9168-7","article-title":"Logics of public communications","volume":"158","author":"Plaza","year":"2007","journal-title":"Synthese"},{"key":"2020012603564417500_ref37","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-48561-3_30","article-title":"Symbolic model checking for dynamic epistemic logic","volume-title":"Logic, Rationality, and Interaction\u20145th International Workshop, LORI 2015 Taipei, Taiwan, October 28\u201331, 2015","author":"van Benthem","year":"2015"},{"key":"2020012603564417500_ref38","first-page":"1115","article-title":"A logic of revelation and concealment","volume-title":"International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2012, Valencia, Spain, June 4\u20138, 2012 (3 Volumes)","author":"van der Hoek","year":"2012"},{"key":"2020012603564417500_ref39","first-page":"719","article-title":"Knowledge and control","volume-title":"10th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2011), Taipei, Taiwan, May 2\u20136, 2011, Volume 1\u20133","author":"van der Hoek","year":"2011"},{"key":"2020012603564417500_ref40","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"},{"key":"2020012603564417500_ref41","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1080\/11663081.2012.705964","article-title":"Public announcements, public assignments and the complexity of their logic","volume":"22","author":"van Ditmarsch","year":"2012","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2020012603564417500_ref42","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-319-16694-0_9","article-title":"One hundred prisoners and a light bulb","volume-title":"One Hundred Prisoners and a Light Bulb","author":"van Ditmarsch","year":"2015"},{"key":"2020012603564417500_ref43","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4020-5839-4","volume-title":"Dynamic Epistemic Logic","author":"van Ditmarsch","year":"2008"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1211\/32008465\/exz023.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1211\/32008465\/exz023.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,26]],"date-time":"2020-01-26T08:56:58Z","timestamp":1580029018000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/8\/1211\/5669855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":43,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2019,12,10]]},"published-print":{"date-parts":[[2019,12,31]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz023","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2019,12]]},"published":{"date-parts":[[2019,12]]}}}