{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:54:32Z","timestamp":1743062072946,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Finitary Idealized Concurrent Algol (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, which in principle can be used to prove equivalence and safety of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known.<\/jats:p><jats:p>We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. The automata use an infinite alphabet with a tree structure. We show that the game semantics of any <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> term. Because of the close match with <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation.<\/jats:p><jats:p>Moreover, we identify a fragment of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {FICA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>FICA<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_10","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"184-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Leafy automata for higher-order concurrency"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3048-5128","authenticated-orcid":false,"given":"Alex","family":"Dixon","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3663-5182","authenticated-orcid":false,"given":"Ranko","family":"Lazi\u0107","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4725-410X","authenticated-orcid":false,"given":"Andrzej S.","family":"Murawski","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.H.L.: Applying game semantics to compositional software modelling and verification. In: Proceedings of TACAS, Lecture Notes in Computer Science, vol.\u00a02988, pp. 421\u2013435. Springer-Verlag (2004)","DOI":"10.1007\/978-3-540-24730-2_32"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., McCusker, G.: Call-by-value games. In: Proceedings of CSL. Lecture Notes in Computer Science, vol.\u00a01414, pp. 1\u201317. Springer-Verlag (1997)","DOI":"10.1007\/BFb0028004"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Abramsky, S., McCusker, G.: Game semantics. In: Schwichtenberg, H., Berger, U.(eds.) Logic and Computation. Springer-Verlag (1998), proceedings of the NATO Advanced Study Institute, Marktoberdorf","DOI":"10.1007\/978-3-642-58622-4_1"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Aiswarya, C., Gastin, P., Kumar, K.N.: Verifying communicating multi-pushdown systems via split-width. In: Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Lecture Notes in Computer Science, vol.\u00a08837, pp. 1\u201317. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_1"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bakewell, A., Ghica, D.R.: On-the-fly techniques for games-based software model checking. In: Proceedings of TACAS, Lecture Notes in Computer Science, vol.\u00a04963, pp. 78\u201392. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_7"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Berger, M., Honda, K., Yoshida, N.: Sequentiality and the pi-calculus. In: Proceedings of TLCA, Lecture Notes in Computer Science, vol.\u00a02044, pp. 29\u201345. Springer-Verlag (2001)","DOI":"10.1007\/3-540-45413-6_7"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund, H., Boja\u0144czyk, M.: Shuffle expressions and words with nested data. In: Proceedings of MFCS. Lecture Notes in Computer Science, vol.\u00a04708, pp. 750\u2013761 (2007)","DOI":"10.1007\/978-3-540-74456-6_66"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4-5), 702\u2013715 (2010)","DOI":"10.1016\/j.tcs.2009.10.009"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27:1\u201327:26 (2011)","DOI":"10.1145\/1970398.1970403"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cotton-Barratt, C., Hopkins, D., Murawski, A.S., Ong, C.L.: Fragments of ML decidable by nested data class memory automata. In: Proceedings of FOSSACS. Lecture Notes in Computer Science, vol.\u00a09034, pp. 249\u2013263. Springer (2015)","DOI":"10.1007\/978-3-662-46678-0_16"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Cotton-Barratt, C., Murawski, A.S., Ong, C.L.: ML, visibly pushdown class memory automata, and extended branching vector addition systems with states. ACM Trans. Program. Lang. Syst. 41(2), 11:1\u201311:38 (2019)","DOI":"10.1145\/3310338"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Cotton-Barratt, C., Murawski, A.S., Ong, C.L.: Weak and nested class memory automata. In: Proceedings of LATA. LNCS, vol.\u00a08977, pp. 188\u2013199. Springer (2015)","DOI":"10.1007\/978-3-319-15579-1_14"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Czerwi\u0144ski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. In: Proceedings of STOC. pp. 24\u201333. ACM (2019)","DOI":"10.1145\/3313276.3316369"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Decker, N., Habermehl, P., Leucker, M., Thoma, D.: Ordered navigation on multi-attributed data words. In: Proceedings of CONCUR. LNCS, vol.\u00a08704, pp. 497\u2013511. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_34"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Dimovski, A., Ghica, D.R., Lazic, R.: A counterexample-guided refinement tool for open procedural programs. In: Proceedings of SPIN. Lecture Notes in Computer Science, vol.\u00a03925, pp. 288\u2013292. Springer-Verlag (2006)","DOI":"10.1007\/11691617_17"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Proceedings of SPIN. Lecture Notes in Computer Science, vol.\u00a09641, pp. 19\u201337. Springer (2016)","DOI":"10.1007\/978-3-319-32582-8_2"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S.: Probabilistic analysis based on symbolic game semantics and model counting. In: Proceedings of GandALF. EPTCS, vol.\u00a0256, pp. 1\u201315 (2017)","DOI":"10.4204\/EPTCS.256.1"},{"key":"10_CR18","unstructured":"Dixon, A., Lazic, R., Murawski, A.S., Walukiewicz, I.: Leafy automata for higher-order concurrency. CoRR abs\/2101.08720 (2021), https:\/\/arxiv.org\/abs\/2101.08720"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Fredriksson, O., Ghica, D.R.: Abstract machines for game semantics, revisited. In: Proceedings of LICS. pp. 560\u2013569 (2013)","DOI":"10.1109\/LICS.2013.63"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Ghica, D.R., McCusker, G.: Reasoning about Idealized Algol using regular expressions. In: Proceedings of ICALP, Lecture Notes in Computer Science, vol.\u00a01853, pp. 103\u2013115. Springer-Verlag (2000)","DOI":"10.1007\/3-540-45022-X_10"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Ghica, D.R., Murawski, A.S.: Compositional model extraction for higher-order concurrent programs. In: Proceedings of TACAS, Lecture Notes in Computer Science, vol.\u00a03920, pp. 303\u2013317. Springer (2006)","DOI":"10.1007\/11691372_20"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Ghica, D.R., Murawski, A.S.: Angelic semantics of fine-grained concurrency. Annals of Pure and Applied Logic 151(2-3), 89\u2013114 (2008)","DOI":"10.1016\/j.apal.2007.10.005"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Ghica, D.R., Murawski, A.S., Ong, C.H.L.: Syntactic control of concurrency. Theoretical Computer Science pp. 234\u2013251 (2006)","DOI":"10.1016\/j.tcs.2005.10.032"},{"key":"10_CR24","unstructured":"Hague, M.: Saturation of concurrent collapsible pushdown systems. In: Proceedings of FSTTCS. LIPIcs, vol.\u00a024, pp. 313\u2013325. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation. Theoretical Computer Science 221(1\u20132), 393\u2013456 (1999)","DOI":"10.1016\/S0304-3975(99)00039-0"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Hopkins, D., Murawski, A.S., Ong, C.H.L.: Hector: An Equivalence Checker for a Higher-Order Fragment of ML. In: Proceedings of CAV, Lecture Notes in Computer Science, vol.\u00a07358, pp. 774\u2013780. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_63"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Hopkins, D., Ong, C.H.L.: Homer: A Higher-order Observational equivalence Model checkER. In: Proceedings of CAV, Lecture Notes in Computer Science, vol.\u00a05643, pp. 654\u2013660. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_51"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: APEX: An Analyzer for Open Probabilistic Programs. In: Proceedings of CAV, Lecture Notes in Computer Science, vol.\u00a07358, pp. 693\u2013698. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_51"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Igarashi, A.: Model-checking higher-order programs with recursive types. In: Proceedings of ESOP. Lecture Notes in Computer Science, vol.\u00a07792, pp. 431\u2013450. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_24"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Proceedings of CAV. Lecture Notes in Computer Science, vol.\u00a05643, pp. 477\u2013492. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Lago, U.D., Tanaka, R., Yoshimizu, A.: The geometry of concurrent interaction: handling multiple ports by way of multiple tokens. In: Proceedings of LICS. pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005112"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: Proceedings of LICS. pp. 1\u201313. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785796"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Murawski, A.S.: Games for complexity of second-order call-by-name programs. Theoretical Computer Science 343(1\/2), 207\u2013236 (2005)","DOI":"10.1016\/j.tcs.2005.05.013"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: Game semantic analysis of equivalence in IMJ. In: Proceedings of ATVA. Lecture Notes in Computer Science, vol.\u00a09364, pp. 411\u2013428. Springer (2015)","DOI":"10.1007\/978-3-319-24953-7_30"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Murawski, A.S., Tzevelekos, N.: An invitation to game semantics. SIGLOG News 3(2), 56\u201367 (2016)","DOI":"10.1145\/2948896.2948902"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Murawski, A.S., Walukiewicz, I.: Third-order Idealized Algol with iteration is decidable. Theoretical Computer Science 390(2-3), 214\u2013229 (2008)","DOI":"10.1016\/j.tcs.2007.09.022"},{"key":"10_CR37","unstructured":"Ong, C.H.L.: Observational equivalence of 3rd-order Idealized Algol is decidable. In: Proceedings of IEEE Symposium on Logic in Computer Science. pp. 245\u2013256. Computer Society Press (2002)"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS. Lecture Notes in Computer Science, vol.\u00a03440, pp. 93\u2013107. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"10_CR39","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416\u2013430 (2000)"},{"key":"10_CR40","unstructured":"Reynolds, J.C.: The essence of Algol. In: de\u00a0Bakker, J.W., van Vliet, J.(eds.) Algorithmic Languages, pp. 345\u2013372. North Holland (1978)"},{"key":"10_CR41","unstructured":"Schwentick, T.: Automata for XML - A survey. J. Comput. Syst. Sci. 73(3), 289\u2013315 (2007)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:06:15Z","timestamp":1616432775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"88","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":"28","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":"32% - 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,2","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}