{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:43Z","timestamp":1740099043583,"version":"3.37.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319735788"},{"type":"electronic","value":"9783319735795"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73579-5_9","type":"book-chapter","created":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T21:32:44Z","timestamp":1514842364000},"page":"133-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking Against Arbitrary Public Announcement Logic: A First-Order-Logic Prover Approach for the Existential Fragment"],"prefix":"10.1007","author":[{"given":"Tristan","family":"Charrier","sequence":"first","affiliation":[]},{"given":"Sophie","family":"Pinchinat","sequence":"additional","affiliation":[]},{"given":"Fran\u00e7ois","family":"Schwarzentruber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,1,3]]},"reference":[{"key":"9_CR1","unstructured":"The tptp (thousands of problems for theorem provers) library. http:\/\/www.cs.miami.edu\/~tptp\/"},{"issue":"1","key":"9_CR2","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1016\/j.jal.2008.12.002","volume":"8","author":"T \u00c5gotnes","year":"2010","unstructured":"\u00c5gotnes, T., Balbiani, P., van Ditmarsch, H., Seban, P.: Group announcement logic. J. Appl. Logic 8(1), 62\u201381 (2010)","journal-title":"J. Appl. Logic"},{"key":"9_CR3","unstructured":"\u00c5gotnes, T., van Ditmarsch, H., French, T.: The undecidability of group announcements. In: International Conference on Autonomous Agents and Multi-agent Systems, AAMAS 2014, Paris, France, 5\u20139 May 2014, pp. 893\u2013900 (2014)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS 1993), Montreal, Canada, 19\u201323 June 1993, pp. 75\u201383 (1993)","DOI":"10.1109\/LICS.1993.287598"},{"key":"9_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Balbiani, P., Baltag, A., van Ditmarsch, H.P., Herzig, A., Hoshi, T., De Lima, T.: What can we achieve by arbitrary announcements?: a dynamic take on fitch\u2019s knowability. In: TARK, pp. 42\u201351 (2007)","DOI":"10.1145\/1324249.1324259"},{"issue":"3","key":"9_CR7","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1093\/jigpal\/jzs052","volume":"21","author":"P Balbiani","year":"2013","unstructured":"Balbiani, P., Gasquet, O., Schwarzentruber, F.: Agents that look at one another. Logic J. IGPL 21(3), 438\u2013467 (2013)","journal-title":"Logic J. IGPL"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Balbiani, P., Herzig, A., Troquard, N.: Dynamic logic of propositional assignments: a well-behaved variant of PDL. In: LICS, pp. 143\u2013152 (2013)","DOI":"10.1109\/LICS.2013.20"},{"key":"9_CR9","unstructured":"Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge, pp. 43\u201356. Morgan Kaufmann Publishers Inc. (1998)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"9_CR11","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, New York (2001)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1\u201320. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_1"},{"issue":"1","key":"9_CR13","doi-asserted-by":"crossref","first-page":"9","DOI":"10.3166\/jancl.21.9-34","volume":"21","author":"T Bolander","year":"2011","unstructured":"Bolander, T., Andersen, M.B.: Epistemic planning for single and multi-agent systems. J. Appl. Non-Class. Logics 21(1), 9\u201334 (2011)","journal-title":"J. Appl. Non-Class. Logics"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-33353-8_10","volume-title":"Logics in Artificial Intelligence","author":"L Bozzelli","year":"2012","unstructured":"Bozzelli, L., van Ditmarsch, H., Pinchinat, S.: The complexity of one-agent refinement modal logic. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS (LNAI), vol. 7519, pp. 120\u2013133. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33353-8_10"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., van Ditmarsch, H.P., Pinchinat, S.: The complexity of one-agent refinement modal logic. In: IJCAI (2013)","DOI":"10.1007\/978-3-642-33353-8_10"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Chandra, A.K., Stockmeyer, L.J.: Alternation. In: Proceedings of FOCS 1976, pp. 98\u2013108 (1976)","DOI":"10.1109\/SFCS.1976.4"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-662-55665-8_24","volume-title":"Logic, Rationality, and Interaction","author":"C Chareton","year":"2017","unstructured":"Chareton, C., van Ditmarsch, H.: Strategic knowledge of the past in quantum cryptography. In: Baltag, A., Seligman, J., Yamada, T. (eds.) LORI 2017. LNCS, vol. 10455, pp. 347\u2013361. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-55665-8_24"},{"key":"9_CR18","unstructured":"Charrier, T., Herzig, A., Lorini, E., Maffre, F., Schwarzentruber, F.: Building epistemic logic from observations and public announcements. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, 25\u201329 April 2016, pp. 268\u2013277 (2016)"},{"key":"9_CR19","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, AAMAS 2015, Istanbul, Turkey, 4\u20138 May 2015, pp. 1471\u20131479 (2015)"},{"key":"9_CR20","unstructured":"Charrier, T., Schwarzentruber, F.: A succinct language for dynamic epistemic logic. In: Proceedings of the 16th Conference on Autonomous Agents and Multi-agent Systems, AAMAS 2017, S\u00e3o Paulo, Brazil, 8\u201312 May 2017, pp. 123\u2013131 (2017)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2892-7","volume-title":"Binary Decision Diagrams - Theory and Implementation","author":"R Drechsler","year":"1998","unstructured":"Drechsler, R., Becker, B.: Binary Decision Diagrams - Theory and Implementation. Springer, Berlin (1998). https:\/\/doi.org\/10.1007\/978-1-4757-2892-7"},{"key":"9_CR23","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"2003","unstructured":"Fagin, R., Moses, Y., Halpern, J.Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (2003)"},{"issue":"2","key":"9_CR24","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR25","unstructured":"French, T., van Ditmarsch, H.P.: Undecidability for arbitrary public announcement logic. In: Advances in Modal Logic, pp. 23\u201342 (2008)"},{"issue":"5","key":"9_CR26","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/s10458-015-9306-4","volume":"30","author":"O Gasquet","year":"2016","unstructured":"Gasquet, O., Goranko, V., Schwarzentruber, F.: Big brother logic: visual-epistemic reasoning in stationary multi-agent systems. Auton. Agent. Multi-Agent Syst. 30(5), 793\u2013825 (2016)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-662-48561-3_13","volume-title":"Logic, Rationality, and Interaction","author":"A Herzig","year":"2015","unstructured":"Herzig, A., Lorini, E., Maffre, F.: A poor man\u2019s epistemic logic based on propositional assignment and higher-order observation. In: van der Hoek, W., Holliday, W.H., Wang, W. (eds.) LORI 2015. LNCS, vol. 9394, pp. 156\u2013168. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48561-3_13"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-33509-4_20","volume-title":"Multi-agent Systems and Agreement Technologies","author":"A Herzig","year":"2016","unstructured":"Herzig, A., Maffre, F.: How to share knowledge by gossiping. In: Rovatsos, M., Vouros, G., Julian, V. (eds.) EUMAS\/AT -2015. LNCS (LNAI), vol. 9571, pp. 249\u2013263. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33509-4_20"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Johnson, D.S.: A catalog of complexity classes. In: Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity (A), pp. 67\u2013161. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88071-0.50007-2"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Lemaignan, S., Ros, R., Mosenlechner, L., Alami, R., Beetz, M.: ORO, a knowledge management platform for cognitive architectures in robotics. In: 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3548\u20133553. IEEE (2010)","DOI":"10.1109\/IROS.2010.5649547"},{"key":"9_CR32","unstructured":"Lemaignan, S., Warnier, M., Sisbot, A.E., Alami, R.: Human-robot interaction: tackling the AI challenges. Artif. Intell. (2014)"},{"issue":"3","key":"9_CR33","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"HR Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR34","unstructured":"L\u00f6we, B., et al.: Logic and the simulation of interaction and reasoning: introductory remarks (2008)"},{"key":"9_CR35","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BF01458217","volume":"76","author":"L L\u00f6wenheim","year":"1915","unstructured":"L\u00f6wenheim, L.: \u00dcber m\u00f6glichkeiten im relativkalk\u00fcl. Math. Ann. 76, 447\u2013470 (1915)","journal-title":"Math. Ann."},{"issue":"3","key":"9_CR36","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s11225-005-3612-9","volume":"79","author":"JS Miller","year":"2005","unstructured":"Miller, J.S., Moss, L.S.: The undecidability of iterated modal relativization. Stud. Logica. 79(3), 373\u2013407 (2005)","journal-title":"Stud. Logica."},{"key":"9_CR37","unstructured":"Niveau, A., Zanuttini, B.: Efficient representations for the modal logic S5. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016, pp. 1223\u20131229 (2016)"},{"issue":"2","key":"9_CR38","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s11229-007-9168-7","volume":"158","author":"J Plaza","year":"2007","unstructured":"Plaza, J.: Logics of public communications. Synthese 158(2), 165\u2013179 (2007)","journal-title":"Synthese"},{"issue":"2","key":"9_CR39","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-662-48561-3_30","volume-title":"Logic, Rationality, and Interaction","author":"J Benthem van","year":"2015","unstructured":"van Benthem, J., van Eijck, J., Gattinger, M., Su, K.: Symbolic model checking for dynamic epistemic logic. In: van der Hoek, W., Holliday, W.H., Wang, W. (eds.) LORI 2015. LNCS, vol. 9394, pp. 366\u2013378. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48561-3_30"},{"key":"9_CR41","unstructured":"van Ditmarsch, H., Grossi, D., Herzig, A., van der Hoek, W., Kuijer, L.B.: Parameters for epistemic gossip problems. In: Proceedings of LOFT 2016 (2016)"},{"key":"9_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16694-0","volume-title":"One Hundred Prisoners and a Light Bulb","author":"H Ditmarsch van","year":"2015","unstructured":"van Ditmarsch, H., Kooi, B.: One Hundred Prisoners and a Light Bulb. Springer, Switzerland (2015). https:\/\/doi.org\/10.1007\/978-3-319-16694-0"},{"key":"9_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5839-4","volume-title":"Dynamic Epistemic Logic","author":"H Ditmarsch van","year":"2008","unstructured":"van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Springer, Dordecht (2008). https:\/\/doi.org\/10.1007\/978-1-4020-5839-4"},{"issue":"1","key":"9_CR44","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1023\/A:1026168632319","volume":"75","author":"HP Ditmarsch van","year":"2003","unstructured":"van Ditmarsch, H.P.: The Russian cards problem. Stud. Logica. 75(1), 31\u201362 (2003)","journal-title":"Stud. Logica."}],"container-title":["Lecture Notes in Computer Science","Dynamic Logic. New Trends and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73579-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T18:34:09Z","timestamp":1570559649000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73579-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319735788","9783319735795"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73579-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}