{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:37:08Z","timestamp":1791301028150,"version":"4.1.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_37","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"539-554","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Balbiani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Boudou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"37_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BFb0022461","volume-title":"Semantics of Concurrent Computation","author":"K Abrahamson","year":"1979","unstructured":"Abrahamson, K.: Modal logic of concurrent nondeterministic programs. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol. 70, pp. 21\u201333. Springer, Heidelberg (1979)"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"Balbiani, P., Boudou, J.: Iteration-free PDL with storing, recovering and parallel composition: a complete axiomatization, J. Logic Comput. (2015)","DOI":"10.1093\/logcom\/exv035"},{"key":"37_CR3","unstructured":"Balbiani, P., Tinchev, T.: Definability and computability for PRSPDL. In: Advances in Modal Logic, pp. 16\u201333. College Publications (2014)"},{"key":"37_CR4","first-page":"95","volume":"269","author":"MRF Benevides","year":"2011","unstructured":"Benevides, M.R.F., de Freitas, R.P., Viana, J.P.: Propositional dynamic logic with storing, recovering and parallel composition. ENTCS 269, 95\u2013107 (2011)","journal-title":"ENTCS"},{"issue":"3","key":"37_CR5","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.apal.2009.07.004","volume":"161","author":"R Brochenin","year":"2009","unstructured":"Brochenin, R., Demri, S., Lozes, \u00c9.: Reasoning about sequences of memory states. Ann. Pure Appl. Logic 161(3), 305\u2013323 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"5","key":"37_CR6","doi-asserted-by":"publisher","first-page":"959","DOI":"10.1017\/S0960129509990077","volume":"19","author":"M Collinson","year":"2009","unstructured":"Collinson, M., Pym, D.J.: Algebra and logic for resource-based systems modelling. Math. Struct. Comput. Sci. 19(5), 959\u20131027 (2009)","journal-title":"Math. Struct. Comput. Sci."},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-35722-0_10","volume-title":"Logical Foundations of Computer Science","author":"JR Courtault","year":"2013","unstructured":"Courtault, J.R., Galmiche, D.: A Modal BI logic for dynamic resource properties. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 134\u2013148. Springer, Heidelberg (2013)"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-16066-3_5","volume-title":"Computation Theory","author":"R Danecki","year":"1984","unstructured":"Danecki, R.: Nondeterministic propositional dynamic logic with intersection is decidable. In: Skowron, A. (ed.) Computation Theory. LNCS, vol. 208, pp. 34\u201353. Springer, Heidelberg (1984)"},{"issue":"1\u20132","key":"37_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1006\/inco.1999.2852","volume":"162","author":"G De Giacomo","year":"2000","unstructured":"De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for converse-PDL. Inf. Comput. 162(1\u20132), 117\u2013137 (2000)","journal-title":"Inf. Comput."},{"issue":"1","key":"37_CR10","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1080\/11663081.2015.1018801","volume":"25","author":"S Demri","year":"2015","unstructured":"Demri, S., Deters, M.: Separation logics and modalities: a survey. J. Appl. Non-Class. Logics 25(1), 50\u201399 (2015)","journal-title":"J. Appl. Non-Class. Logics"},{"issue":"2","key":"37_CR11","doi-asserted-by":"publisher","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":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-02959-2_32","volume-title":"Automated Deduction \u2013 CADE-22","author":"R Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 437\u2013452. Springer, Heidelberg (2009)"},{"issue":"3","key":"37_CR13","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","volume":"9","author":"I Horrocks","year":"1999","unstructured":"Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385\u2013410 (1999)","journal-title":"J. Log. Comput."},{"issue":"3","key":"37_CR14","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF01049412","volume":"4","author":"\u00c1 Kurucz","year":"1995","unstructured":"Kurucz, \u00c1., N\u00e9meti, I., Sain, I., Simon, A.: Decidable and undecidable logics with a binary modality. J. Logic Lang. Inf. 4(3), 191\u2013206 (1995)","journal-title":"J. Logic Lang. Inf."},{"key":"37_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/11538363_29","volume-title":"Computer Science Logic","author":"C Lutz","year":"2005","unstructured":"Lutz, C.: PDL with intersection and converse is decidable. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 413\u2013427. Springer, Heidelberg (2005)"},{"key":"37_CR16","unstructured":"Massacci, F.: Decision procedures for expressive description logics with intersection, composition, converse of roles and role identity. In: IJCAI, pp. 193\u2013198. Morgan Kaufmann (2001)"},{"issue":"2","key":"37_CR17","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1145\/23005.23008","volume":"34","author":"D Peleg","year":"1987","unstructured":"Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450\u2013479 (1987)","journal-title":"J. ACM"},{"issue":"2","key":"37_CR18","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"VR Pratt","year":"1980","unstructured":"Pratt, V.R.: A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20(2), 231\u2013254 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"37_CR19","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The semantics and Proof Theory of the Logic of Bunched Implications","author":"DJ Pym","year":"2002","unstructured":"Pym, D.J.: The semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T17:10:49Z","timestamp":1748538649000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}