{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:53:39Z","timestamp":1725537219357},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_23","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T13:27:52Z","timestamp":1252934872000},"page":"302-316","source":"Crossref","is-referenced-by-count":0,"title":["On Model Checking Boolean BI"],"prefix":"10.1007","author":[{"given":"Heng","family":"Guo","sequence":"first","affiliation":[]},{"given":"Hanpin","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Zhongyuan","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Yongzhi","family":"Cao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-24597-1_3","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"N. Biri","year":"2003","unstructured":"Biri, N., Galmiche, D.: A separation logic for resource distribution. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 23\u201337. Springer, Heidelberg (2003)"},{"key":"23_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-71070-7_4","volume-title":"Automated Reasoning","author":"M. Bozga","year":"2008","unstructured":"Bozga, M., Iosif, R., Perarnau, S.: Quantitative separation logic and programs with lists. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 34\u201349. Springer, Heidelberg (2008)"},{"key":"23_CR4","first-page":"328","volume-title":"Proc. 36th ACM Symp. Principles of Prog. Lang. (POPL 1909)","author":"J. Brotherston","year":"2009","unstructured":"Brotherston, J., Calcagno, C.: Classical bi: a logic for reasoning about dualising resources. In: Proc. 36th ACM Symp. Principles of Prog. Lang (POPL 1909), pp. 328\u2013339. ACM Press, New York (2009)"},{"unstructured":"Calcagno, C., Dinsdale-Young, T., Gardner, P.: Decidability of context logic (unpublished) (2008), http:\/\/www.doc.ic.ac.uk\/~ccris\/ftp\/decidCL.pdf","key":"23_CR5"},{"key":"23_CR6","first-page":"271","volume-title":"Proc. 32th ACM Symp. Principles of Prog. Lang. (POPL 2005)","author":"C. Calcagno","year":"2005","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: Proc. 32th ACM Symp. Principles of Prog. Lang (POPL 2005), pp. 271\u2013282. ACM Press, New York (2005)"},{"key":"23_CR7","first-page":"123","volume-title":"Proc. 34th ACM Symp. Principles of Prog. Lang. (POPL 2007)","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic as modal logic: completeness and parametric inexpressivity. In: Proc. 34th ACM Symp. Principles of Prog. Lang (POPL 2007), pp. 123\u2013134. ACM Press, New York (2007)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: Proc. 27th ACM Symp. Principles of Prog. Lang (POPL 2000), pp. 365\u2013377 (2000)","key":"23_CR9","DOI":"10.1145\/325694.325742"},{"issue":"1","key":"23_CR10","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","volume":"240","author":"L. Cardelli","year":"2000","unstructured":"Cardelli, L., Gordon, A.D.: Mobile ambients. Theor. Comput. Sci.\u00a0240(1), 177\u2013213 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-45315-6_10","volume-title":"Foundations of Software Science and Computation Structures","author":"W. Charatonik","year":"2001","unstructured":"Charatonik, W., Dal Zilio, S., Gordon, A.D., Mukhopadhyay, S., Talbot, J.-M.: The complexity of model checking mobile ambients. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 152\u2013167. Springer, Heidelberg (2001)"},{"issue":"1-3","key":"23_CR12","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/S0304-3975(02)00832-0","volume":"308","author":"W. Charatonik","year":"2003","unstructured":"Charatonik, W., Dal-Zilio, S., Gordon, A.D., Mukhopadhyay, S., Talbot, J.-M.: Model checking mobile ambients. Theor. Comput. Sci.\u00a0308(1-3), 277\u2013331 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/3-540-44802-0_24","volume-title":"Computer Science Logic","author":"W. Charatonik","year":"2001","unstructured":"Charatonik, W., Talbot, J.-M.: The decidability of model checking mobile ambients. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 339\u2013354. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Clifford, A.H., Preston, G.B.: The Algebraic Theory of Semigroups, vol.\u00a02. The American Mathematical Society (1967)","key":"23_CR14","DOI":"10.1090\/surv\/007.2"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-54345-7_57","volume-title":"Mathematical Foundations of Computer Science 1991","author":"E. Domenjoud","year":"1991","unstructured":"Domenjoud, E., Lorraine, I.: Solving systems of linear diophantine equations: An algebraic approach. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol.\u00a0520, pp. 141\u2013150. Springer, Heidelberg (1991)"},{"issue":"2","key":"23_CR16","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0021-8693(69)90070-2","volume":"13","author":"S. Eilenberg","year":"1969","unstructured":"Eilenberg, S., Schutzenberger, M.-P.: Rational sets in commutative monoids. J. Algebra\u00a013(2), 173\u2013191 (1969)","journal-title":"J. Algebra"},{"key":"23_CR17","first-page":"1003","volume":"19","author":"P. Freyd","year":"1968","unstructured":"Freyd, P.: Redei\u2019s finiteness theorem for commutative semigroups. Proc. of the AMS\u00a019, 1003 (1968)","journal-title":"Proc. of the AMS"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11944836_33","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"D. Galmiche","year":"2006","unstructured":"Galmiche, D., Larchey-Wendling, D.: Expressivity properties of boolean BI through relational models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 357\u2013368. Springer, Heidelberg (2006)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-45793-3_13","volume-title":"Computer Science Logic","author":"D. Galmiche","year":"2002","unstructured":"Galmiche, D., M\u00e9ry, D., Pym, D.J.: Resource tableaux (Extended abstract). In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 183\u2013199. Springer, Heidelberg (2002)"},{"issue":"2","key":"23_CR20","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0304-3975(95)00037-W","volume":"148","author":"P. Jan\u010dar","year":"1995","unstructured":"Jan\u010dar, P.: Undecidability of bisimilarity for petri nets and some related problems. Theor. Comput. Sci.\u00a0148(2), 281\u2013301 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0036189","volume-title":"Fundamentals of Computation Theory","author":"U. Koppenhagen","year":"1997","unstructured":"Koppenhagen, U., Mayr, E.W.: The complexity of the coverability, the containment, and the equivalence problems for commutative semigroups. In: Chlebus, B.S., Czaja, L. (eds.) FCT 1997. LNCS, vol.\u00a01279, pp. 257\u2013268. Springer, Heidelberg (1997)"},{"issue":"1","key":"23_CR22","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00245019","volume":"5","author":"D. Lankford","year":"1989","unstructured":"Lankford, D.: Non-negative integer basis algorithms for linear equations with integer coefficients. J. Automated Reasoning\u00a05(1), 25\u201335 (1989)","journal-title":"J. Automated Reasoning"},{"key":"23_CR23","first-page":"662","volume-title":"Proc. 31st Symp. Found. of Comp. Sci. (FOCS 1990)","author":"P. Lincoln","year":"1990","unstructured":"Lincoln, P., Mitchell, J.C., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. In: Proc. 31st Symp. Found. of Comp. Sci (FOCS 1990), vol.\u00a0II, pp. 662\u2013671. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"3","key":"23_CR24","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"E. Mayr","year":"1982","unstructured":"Mayr, E., Meyer, A.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. in Math.\u00a046(3), 305\u2013329 (1982)","journal-title":"Adv. in Math."},{"key":"23_CR25","volume-title":"Computation: Finite and Infinite Machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)"},{"issue":"2","key":"23_CR26","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05(2), 215\u2013244 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"issue":"1","key":"23_CR27","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","volume":"315","author":"D.J. Pym","year":"2004","unstructured":"Pym, D.J., O\u2019Hearn, P.W., Yang, H.: Possible worlds and resources: the semantics of bi. Theor. Comput. Sci.\u00a0315(1), 257\u2013305 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR28","volume-title":"The Theory of Finitely Generated Commutative Semigroups","author":"L. Redei","year":"1965","unstructured":"Redei, L.: The Theory of Finitely Generated Commutative Semigroups. Oxford University Press, Oxford (1965)"},{"key":"23_CR29","first-page":"55","volume-title":"Proc. 17th IEEE Symp. Logic in Comp. Sci. (LICS 2002)","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symp. Logic in Comp. Sci (LICS 2002), pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"issue":"1","key":"23_CR30","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BF02574262","volume":"43","author":"C.P. Rupert","year":"1991","unstructured":"Rupert, C.P.: On commutative kleene monoids. Semigroup Forum\u00a043(1), 163\u2013177 (1991)","journal-title":"Semigroup Forum"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T11:19:30Z","timestamp":1558523970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}