UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

On Decidability of Concurrent Kleene Algebra

Brunet, P; Pous, D; Struth, G; (2017) On Decidability of Concurrent Kleene Algebra. In: Meyer, R and Nestmann, U, (eds.) Proceedings of the 28th International Conference on Concurrency Theory (CONCUR 2017). (pp. 28:1-28:15). LIPICS: Dagstuhl, Germany. Green open access

[img]
Preview
Text
Brunet_On decidability of concurrent kleene algebra_VoR.pdf - ["content_typename_Published version" not defined]

Download (606kB) | Preview

Abstract

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.

Type: Proceedings paper
Title: On Decidability of Concurrent Kleene Algebra
Event: 28th International Conference on Concurrency Theory (CONCUR 2017)
Location: Berlin, Germany
Dates: 5th-8th September 2017
ISBN-13: 978-3-95977-048-4
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/LIPIcs.CONCUR.2017.28
Publisher version: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2017.28
Language: English
Additional information: © Paul Brunet, Damien Pous, and Georg Struth; licensed under Creative Commons License CC-BY (https://creativecommons.org/licenses/by/3.0/).
Keywords: oncurrent Kleene algebra, series-parallel pomsets, Petri nets
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: http://discovery.ucl.ac.uk/id/eprint/10053782
Downloads since deposit
12Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item