10.4230/LIPICS.CONCUR.2017.28
Brunet, Paul
Paul
Brunet
Pous, Damien
Damien
Pous
Struth, Georg
Georg
Struth
On Decidability of Concurrent Kleene Algebra
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2017
Concurrent Kleene algebra
series-parallel pomsets
Petri nets
Meyer, Roland
Roland
Meyer
Nestmann, Uwe
Uwe
Nestmann
2017
2017-09-01
2017-09-01
2017-09-01
en
urn:nbn:de:0030-drops-77881
10.4230/LIPIcs.CONCUR.2017
978-3-95977-048-4
1868-8969
http://archive.numdam.org/article/ITA_1990__24_4_419_0.pdf
https://hal.archives-ouvertes.fr/hal-01558108/
10.1016/0304-3975(88)90124-7
10.1016/0304-3975(95)00132-8
10.1109/LICS.1991.151646
10.1007/BFb0032022
10.1007/978-3-319-06251-8_5
10.1007/978-3-540-40965-6_12
10.1016/S0304-3975(00)00031-1
10.1006/inco.1994.1098
10.1109/SWAT.1972.29
http://www.fing.edu.uy/inco/cursos/intropln/material/p419-thompson.pdf
10.1145/800135.804393
10.4230/LIPIcs.CONCUR.2017
LIPIcs, Volume 85, CONCUR 2017
28th International Conference on Concurrency Theory (CONCUR 2017)
2017
85
28
28:1
28:15
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Meyer, Roland
Roland
Meyer
Nestmann, Uwe
Uwe
Nestmann
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2017
85
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
15 pages
606086 bytes
application/pdf
Creative Commons Attribution 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 85, 28th International Conference on Concurrency Theory (CONCUR 2017), pages 28:1-28:15