Pomset languages and concurrent Kleene algebras
Séminaire automates
in Paris,
November 2017
Concurrent Kleene algebras (CKA) and biKleene 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.
In the first part of the talk, I will present an automaton model designed to describe such languages of pomset, which satisfies a Kleenelike theorem. The main difference with previous constructions is that from expressions to automata, we use Brzozowski derivatives.
In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidabilty as well as provide tight complexity bounds.
I will finish the presentation by briefly presenting a recent proof of completeness, showing that two seriesrational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal.
Joint work with Damien Pous, Georg Struth, Tobias Kappé, Bas Luttik, Alexandra Silva, and Fabio Zanasi.
Related talks  
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire du LACL
in Créteil,
December 2021
(in French)
.

More  
Recent developments in concurrent Kleene algebra
JetBrains Research
in St Petersburg (remote talk),
October 2021
.

More  
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire MAREL
in Montpellier,
April 2021
.

More  
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire ACADIE
in Toulouse,
April 2021
.

More  
Observations and locality in distributed processes
IRIS scientific meeting
in London,
March 2021
.

More  
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire LIRICA
in Marseille,
January 2021
(in French)
.

More  
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire LOVE
in Paris,
January 2021
.

More  
Recent developments in concurrent Kleene algebra
IRIS scientific meeting
in London,
December 2020
.

More  
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
FSCD
in Paris,
July 2020
.

More  
Recent developments in concurrent Kleene algebra
Séminaire PPS
in Paris,
June 2020
.

More  
Pomsets with boxes: towards Atomic CKA
Highlights
in Warsaw,
September 2019
.

More  
Pomset languages and concurrent Kleene algebra
Theory seminar  QMU
in London,
February 2018
.

More  
On Decidability of Concurrent Kleene Algebra
CONCUR
in Berlin,
September 2017
.

More  
Related papers  
Equivalence checking for weak biKleene algebra
(in LMCS 2021)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi. 
More  
Partially Observable Concurrent Kleene Algebra
(in CONCUR 2020)
with Jana Wagemaker, Simon Docherty, Jurriaan Rot, Tobias Kappé and Alexandra Silva. 
More  
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness
(in FoSSaCS 2020)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi and Jana Wagemaker. 
More  
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
(in FSCD 2020)
with David Pym. 
More  
On SeriesParallel Pomset Languages: Rationality, ContextFreeness and Automata
(in JLAMP 2019)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi. 
More  
Kleene Algebra with Observations
(in CONCUR 2019)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi, Jurriaan Rot and Jana Wagemaker. 
More  
Concurrent Kleene Algebra: Free Model and Completeness
(in ESOP 2018)
with Tobias Kappé, Alexandra Silva and Fabio Zanasi. 
More  
Brzozowski Goes Concurrent  A Kleene Theorem for Pomset Languages
(in CONCUR 2017)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi. 
More  
On Decidability of Concurrent Kleene Algebra
(in CONCUR 2017)
with Damien Pous and Georg Struth. 
More 