文章基本信息

标题：On Decidability of Concurrent Kleene Algebra
本地全文：下载
作者：Paul Brunet ; Damien Pous ; Georg Struth 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：85
页码：28:1-28:15
DOI：10.4230/LIPIcs.CONCUR.2017.28
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Concurrent Kleene algebra; series-parallel pomsets; Petri nets