{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:26Z","timestamp":1763468126141,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-BS02-011"],"award-info":[{"award-number":["ANR-11-BS02-011"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"name":"University Henri Poincar\u00e9 of Nancy"},{"DOI":"10.13039\/501100004794","name":"Centre National de la Recherche Scientifique","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004794","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,2]]},"abstract":"<jats:p>We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered the core of separation and spatial logics. For this, we define a complete phase semantics suitable for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out the elementary fragment of ILL, which is both undecidable and complete for trivial phase semantics. Thus, we obtain the undecidability of BBI.<\/jats:p>","DOI":"10.1145\/2422085.2422091","type":"journal-article","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T19:25:04Z","timestamp":1361561104000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Nondeterministic Phase Semantics and the Undecidability of Boolean BI"],"prefix":"10.1145","volume":"14","author":[{"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[{"name":"LORIA -- CNRS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Didier","family":"Galmiche","sequence":"additional","affiliation":[{"name":"LORIA -- University Henri Poincar\u00e9"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory (CONCUR\u201997)","volume":"1243","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Application to model-checking . In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR\u201997) . Lecture Notes in Computer Science , vol. 1243 . Springer, Berlin, 135--150. Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR\u201997). Lecture Notes in Computer Science, vol. 1243. Springer, Berlin, 135--150."},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1016\/j.entcs.2010.08.012"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1145\/1480881.1480923"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1109\/LICS.2010.24"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1017\/S0956796804005404"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1109\/LICS.2007.30"},{"volume-title":"Proceedings of the 19th IEEE Symposium on Logic in Computer Science. 64--73","author":"de Groote P.","unstructured":"de Groote , P. , Guillaume , B. , and Salvati , S . 2004. Vector addition tree automata . In Proceedings of the 19th IEEE Symposium on Logic in Computer Science. 64--73 . de Groote, P., Guillaume, B., and Salvati, S. 2004. Vector addition tree automata. In Proceedings of the 19th IEEE Symposium on Logic in Computer Science. 64--73.","key":"e_1_2_1_7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/11944836_33"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1017\/S0960129505004858"},{"key":"e_1_2_1_10_1","first-page":"193","article-title":"Modal logics with n-ary connectives. Zeitschr. f. math. Logik und Grundlagen d","volume":"36","author":"Ghilardi S.","year":"1990","unstructured":"Ghilardi , S. and Meloni , G. 1990 . Modal logics with n-ary connectives. Zeitschr. f. math. Logik und Grundlagen d . Math 36 , 193 -- 215 . Ghilardi, S. and Meloni, G. 1990. Modal logics with n-ary connectives. Zeitschr. f. math. Logik und Grundlagen d. Math 36, 193--215.","journal-title":"Math"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1016\/0304-3975(87)90045-4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/360204.375719"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1016\/0168-0072(94)90011-6"},{"volume-title":"Advances in Linear Logic, J.-Y","author":"Kanovich M.","unstructured":"Kanovich , M. 1995. The direct simulation of Minsky machines in linear logic . In Advances in Linear Logic, J.-Y . Girard, Y. Lafont, and L. Regnier Eds., London Mathematical Society Lecture Notes, vol. 222 . Cambridge University Press , Chapter 2, 123--145. Kanovich, M. 1995. The direct simulation of Minsky machines in linear logic. In Advances in Linear Logic, J.-Y. Girard, Y. Lafont, and L. Regnier Eds., London Mathematical Society Lecture Notes, vol. 222. Cambridge University Press, Chapter 2, 123--145.","key":"e_1_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.2307\/2275674"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1006\/inco.1996.0019"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1016\/j.entcs.2010.08.022"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1017\/S0960129509007567"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1109\/LICS.2010.18"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1017\/S0960129500000062"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.2307\/1970290"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.2307\/421090"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1016\/S0304-3975(02)00024-5"},{"key":"e_1_2_1_24_1","series-title":"Applied Logic Series","volume-title":"The semantics and proof theory of the logic of bunched implications","author":"Pym D.","unstructured":"Pym , D. 2002. The semantics and proof theory of the logic of bunched implications . Applied Logic Series , vol. 26 . Kluwer Academic Publishers . Errata available at http:\/\/www.cs.ac.uk\/~pym\/pym-tofts-fac-errata.pdf. Pym, D. 2002. The semantics and proof theory of the logic of bunched implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers. Errata available at http:\/\/www.cs.ac.uk\/~pym\/pym-tofts-fac-errata.pdf."},{"volume-title":"Monographs on Theoretical Computer Science","author":"Reisig W.","unstructured":"Reisig , W. 1985. Petri nets, an introduction. EATCS , Monographs on Theoretical Computer Science , Springer Verlag , Berlin . Reisig, W. 1985. Petri nets, an introduction. EATCS, Monographs on Theoretical Computer Science, Springer Verlag, Berlin.","key":"e_1_2_1_25_1"},{"key":"e_1_2_1_26_1","series-title":"Lecture Notes Series","volume-title":"Lectures on linear logic","author":"Troelstra A.","unstructured":"Troelstra , A. 1992. Lectures on linear logic . Lecture Notes Series , vol. 29 . CSLI , Stanford, CA . Troelstra, A. 1992. Lectures on linear logic. Lecture Notes Series, vol. 29. CSLI, Stanford, CA."},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.2307\/2274953"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422091","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2422085.2422091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:35Z","timestamp":1750234715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["10.1145\/2422085.2422091"],"URL":"https:\/\/doi.org\/10.1145\/2422085.2422091","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,2]]},"assertion":[{"value":"2011-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}