Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Brunet, Paul; Pous, Damien; Struth, Georg http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-77881
URL:

; ;

On Decidability of Concurrent Kleene Algebra

pdf-format:


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.

BibTeX - Entry

@InProceedings{brunet_et_al:LIPIcs:2017:7788,
  author =	{Paul Brunet and Damien Pous and Georg Struth},
  title =	{{On Decidability of Concurrent Kleene Algebra}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Roland Meyer and Uwe Nestmann},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7788},
  URN =		{urn:nbn:de:0030-drops-77881},
  doi =		{10.4230/LIPIcs.CONCUR.2017.28},
  annote =	{Keywords: Concurrent Kleene algebra, series-parallel pomsets, Petri nets}
}

Keywords: Concurrent Kleene algebra, series-parallel pomsets, Petri nets
Seminar: 28th International Conference on Concurrency Theory (CONCUR 2017)
Issue date: 2017
Date of publication: 2017


DROPS-Home | Fulltext Search | Imprint Published by LZI