{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T13:09:29Z","timestamp":1768828169385,"version":"3.49.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,8,17]],"date-time":"2015-08-17T00:00:00Z","timestamp":1439769600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"crossref"}]},{"name":"JSPS KAKENHI","award":["25330016"],"award-info":[{"award-number":["25330016"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,11,19]]},"abstract":"<jats:p>We reconstruct Peleg\u2019s concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an axiomatization of concurrent dynamic algebras from that basis. In this context, sequential composition is not associative. It interacts with parallel composition through a weak distributivity law. The modal operators of concurrent dynamic algebra are obtained from abstract axioms for domain and antidomain operators; the Kleene star is modelled as a least fixpoint. Algebraic variants of Peleg\u2019s axioms are shown to be derivable in these algebras, and their soundness is proved relative to the multirelational model. Additional results include iteration principles for the Kleene star and a refutation of variants of Segerberg\u2019s axiom in the multirelational setting. The most important results have been verified formally with Isabelle\/HOL.<\/jats:p>","DOI":"10.1145\/2785967","type":"journal-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T14:08:55Z","timestamp":1440425335000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Concurrent Dynamic Algebra"],"prefix":"10.1145","volume":"16","author":[{"given":"Hitoshi","family":"Furusawa","sequence":"first","affiliation":[{"name":"Kagoshima University, Korimoto, Kagoshima, Japan"}]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, UK"}]}],"member":"320","published-online":{"date-parts":[[2015,8,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_1","unstructured":"P. Blackburn M. de Rijke and Y. Venema. 2011. Modal Logic. Cambridge University Press New York NY.  P. Blackburn M. de Rijke and Y. Venema. 2011. Modal Logic. Cambridge University Press New York NY."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90069-9"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183285"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79980-1_25"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.05.007"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5109\/21043"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"R. Goldblatt. 1992. Parallel action: Concurrent dynamic logic with independent modalities. Studia Logica 51 3\/4 551--578.  R. Goldblatt. 1992. Parallel action: Concurrent dynamic logic with independent modalities. Studia Logica 51 3\/4 551--578.","DOI":"10.1007\/BF01028975"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"D. Harel D. Kozen and J. Tiuryn. 2000. Dynamic Logic. MIT Press Cambridge MA.   D. Harel D. Kozen and J. Tiuryn. 2000. Dynamic Logic. MIT Press Cambridge MA.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_1_13_1","unstructured":"R. D. Maddux. 2006. Relation Algebras. Elsevier.  R. D. Maddux. 2006. Relation Algebras. Elsevier."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.01.007"},{"key":"e_1_2_1_15_1","volume-title":"Fundamentals of Computation Theory (LNCS)","author":"N\u00e9meti I."},{"key":"e_1_2_1_16_1","first-page":"90","article-title":"Constructive Concurrent Dynamic Logic I","author":"Nerode A.","year":"1990","journal-title":"Technical Report"},{"key":"e_1_2_1_17_1","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS","volume":"2283","author":"Nipkow T."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04639-1_19"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1983.47"},{"key":"e_1_2_1_20_1","volume-title":"Topics in the Theory of Computation (Mathematics Studies)","author":"Parikh R."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90035-3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/23005.23008"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370685"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804649"},{"key":"e_1_2_1_25_1","volume-title":"Theory and Applications of Relational Structures as Knowledge Instruments (LNCS)","author":"Rewitzky I."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11828563_21"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90014-6"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-008-9390-y"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.12.001"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2785967","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2785967","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:14Z","timestamp":1750225394000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2785967"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,17]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,11,19]]}},"alternative-id":["10.1145\/2785967"],"URL":"https:\/\/doi.org\/10.1145\/2785967","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,17]]},"assertion":[{"value":"2014-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-08-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}