{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:42:08Z","timestamp":1770752528786,"version":"3.50.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031300431","type":"print"},{"value":"9783031300448","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Knowledge-based programs specify multi-agent protocols with epistemic guards that abstract from how agents learn and record facts or information about other agents and the environment. Their interpretation involves a non-monotone mutual dependency between the evaluation of epistemic guards over the reachable states and the derivation of the reachable states depending on the evaluation of epistemic guards. We apply the technique of a must\/cannot analysis invented for synchronous programming languages to the interpretation problem of knowledge-based programs and demonstrate that the resulting constructive interpretation is monotone and has a least fixed point. We relate our approach with existing interpretation schemes for both synchronous and asynchronous programs. Finally, we describe an implementation of the constructive interpretation and illustrate the procedure by several examples and an application to the Java memory model.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_10","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"253-280","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Interpreting Knowledge-based Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4050-3249","authenticated-orcid":false,"given":"Alexander","family":"Knapp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heribert","family":"M\u00fchlberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5807-856X","authenticated-orcid":false,"given":"Bernhard","family":"Reus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, chap.\u00a0C.7, pp. 783\u2013818. North-Holland (1977)","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"10_CR2","unstructured":"Aspinall, D., \u0160ev\u010d\u00edk, J.: Java Memory Model examples: Good, bad and ugly. In: Proc. Verification and Analysis of Multi-Threaded Java-like Programs (VAMP 2007) (2007)"},{"key":"10_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Baltag, A., Moss, L.S.: Logics for Epistemic Programs. Synth. 139(2), 165\u2013224 (2004). https:\/\/doi.org\/10.1023\/B:SYNT.0000024912.56773.5e","DOI":"10.1023\/B:SYNT.0000024912.56773.5e"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Baral, C., Gelfond, M.: Logic programming and knowledge representation. J. Logic Program. 19\u201320(Suppl.\u00a01), 73\u2013148 (1994)","DOI":"10.1016\/0743-1066(94)90025-6"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Guernic, P.L., de\u00a0Simone, R.: The synchronous languages twelve years later. Proc. IEEE 91(1), 64\u201383 (2003)","DOI":"10.1109\/JPROC.2002.805826"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Berry, G.: The foundations of Esterel. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 425\u2013454. Foundations of Computing Series, MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"10_CR8","unstructured":"Berry, G.: The Constructive Semantics of Pure Esterel, Draft v3 (2002), https:\/\/www-sop.inria.fr\/members\/Gerard.Berry\/Papers\/EsterelConstructiveBook.pdf"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, 2nd edn. (2002)","DOI":"10.1017\/CBO9780511809088"},{"key":"10_CR10","unstructured":"de Haan, H.W., Hesselink, W.H., de Lavalette, G.R.R.: Knowledge-based asynchronous programming. Fund. Inform. 63(2-3), 259\u2013281 (2004)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Denecker, M., Bruynooghe, M., Marek, V.: Logic programming revisited: Logic programs as inductive definitions. ACM Trans. Comput. Logic 2(4), 623\u2013654 (2001)","DOI":"10.1145\/383779.383789"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Denecker, M., Ternovska, E.: A logic of nonmonotone inductive definitions. ACM Trans. Comput. Log. 9(2), 14:1\u201314:52 (2008)","DOI":"10.1145\/1342991.1342998"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Knowledge-based programs. Distr. Comput. 10(4), 199\u2013225 (1997)","DOI":"10.1007\/s004460050038"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (2003)","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Fandinno, J., Faber, W., Gelfond, M.: Thirty years of epistemic specifications. Theo. Pract. Logic Program. 22(6), 1043\u20131083 (2022)","DOI":"10.1017\/S147106842100048X"},{"key":"10_CR16","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) Proc. 5th Intl. Conf. Symp. Logic Programming. pp. 1070\u20131080. MIT Press (1988)"},{"key":"10_CR17","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification. Addison-Wesley, 3rd edn. (2005)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data-flow programming language Lustre. Proc. IEEE 79(9), 1305\u20131320 (1991)","DOI":"10.1109\/5.97300"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Harper, R.: Practical Foundations of Programming Languages. Cambridge University Press (2013)","DOI":"10.1017\/CBO9781139342131"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"van\u00a0der Hoek, W., Wooldridge, M.J.: Model checking knowledge and time. In: Bosnacki, D., Leue, S. (eds.) Proc. 9th Intl. Ws. Model Checking of Software (SPIN 2002). Lect. Notes Comp. Sci., vol.\u00a02318, pp. 95\u2013111. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-46017-9_9","DOI":"10.1007\/3-540-46017-9_9"},{"key":"10_CR21","unstructured":"Lomuscio, A., Penczek, W.: Model checking temporal epistemic logic. In: van Ditmarsch et\u00a0al. [29], chap.\u00a08, pp. 397\u2013441"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"L\u00fcttgen, G., Mendler, M.: The intuitionism behind statecharts steps. ACM Trans. Comput. Log. 3(1), 1\u201341 (2002). https:\/\/doi.org\/10.1145\/504077.504078","DOI":"10.1145\/504077.504078"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model (2005), http:\/\/dl.dropbox.com\/u\/1011627\/journal.pdf, draft","DOI":"10.1145\/1040305.1040336"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Mousavi, M., Phillips, I., Reniers, M.A., Ulidowski, I.: Semantics and expressiveness of ordered SOS. Inform. & Comput. 207(2), 85\u2013119 (2009). https:\/\/doi.org\/10.1016\/j.ic.2007.11.008","DOI":"10.1016\/j.ic.2007.11.008"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Java memory model (1999\u2013), http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/","DOI":"10.1145\/304065.304106"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Sainsbury, R.M.: Paradoxes. Cambridge University Press, 3rd edn. (2009)","DOI":"10.1017\/CBO9780511812576"},{"key":"10_CR27","unstructured":"Su, K.: Model checking temporal logics of knowledge in distributed systems. In: McGuiness, D.L., Ferguson, G. (eds.) Proc. 19th Natl. Conf. Artificial Intelligence, 16th Conf. Innovative Applications of Artificial Intelligence (AAAI 2004). pp. 98\u2013103. AAAI Press, MIT Press (2004)"},{"key":"10_CR28","unstructured":"Vahidi, A.: JDD: A pure Java BDD and Z-BDD library. https:\/\/bitbucket.org\/vahidi\/jdd (2003)"},{"key":"10_CR29","unstructured":"van Ditmarsch, H., Halpern, J.Y., van der Hoek, W., Kooi, B. (eds.): Handbook of Epistemic Logic. College Publ. (2015)"},{"key":"10_CR30","unstructured":"van Ditmarsch, H., Halpern, J.Y., van der Hoek, W., Kooi, B.: An introduction to logics of knowledge and belief. In: Handbook of Epistemic Logic [29], chap.\u00a01, pp. 1\u201351"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic, Synthese Library, vol.\u00a0337. Springer (2008)","DOI":"10.1007\/978-1-4020-5839-4"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30044-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T10:38:45Z","timestamp":1729247925000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}