2026-08-13T08:41:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7788 2024-03-06T10:41:09Z ddc:004 open_access

On Decidability of Concurrent Kleene Algebra Brunet, Paul Pous, Damien Struth, Georg Concurrent Kleene algebra series-parallel pomsets Petri nets Concurrent Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets. We use constructions on Petri nets to provide two decision procedures for such pomset languages motivated by the equational and the refinement theory of concurrent Kleene algebra. The contribution to the first problem lies in a much simpler algorithm and an EXPSPACE complexity bound. Decidability of the second, more interesting problem is new and, in fact, EXPSPACE-complete. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Paul Brunet and Damien Pous and Georg Struth 2017 Is Part Of LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2017.28 urn:nbn:de:0030-drops-77881 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.28 eng https://creativecommons.org/licenses/by/3.0/legalcode