On Decidability of Concurrent Kleene Algebra
Paul Brunet, Damien Pous & Georg Struth
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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see
our documentation.