# CKA : Concurrent Kleene Algebras

Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. This project concerns itself with the study of this framework, and of its enhancements with extra features. The aim is to carry out sophisticated verification tasks using this language.

## Test equations

### How to use this :

Write an equation in the input field of the applet, and see its validity just to the right (a green tick meaning yes and a red cross meaning no).

Equations should be entered like this:

``````<expr1> <cmp> <expr2>
``````

An expression can use strings as variables/letters, and the operations:

• `0`: the empty set
• `1`: the empty process
• `<expr1> + <expr2>`: the set union
• `<expr1> | <expr2>`: the parallel product
• `<expr1> . <expr2>`: the sequential product
• `<expr1>*`: the unbounded sequential iteration
• `<expr1>+`: the unbounded non-empty sequential iteration
• `<expr1>{<int>}`: the fixed iteration. For instance, `(a.b){3}` is a shorthand for `(a.b).(a.b).(a.b)`

You can also use brackets `(...)`. The valid comparaisons `<cmp>` are:

• `<=`: loose inclusion
• `>=`: converse of the loose inclusion
• `<`: strict inclusion
• `>`: converse of the strict inclusion
• `=`: equality
• `=/=`: negation of the equality
• `<>`: means that the two expressions are incomparable, i.e. neither one of them is included in the other.

For instance, `(a|b)^+ . C + d < d + a.b.C + (d|a)` is an acceptable equation.

## Detailled equation checking

 ≤

 Net for the first expression: Net for the second expression: Automaton of the accepting runs: Product automaton:

Sources
Documentation

### Related papers

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

### Related talks

Avancées récentes sur les algèbres de Kleene concurrentes
séminaire du LACL in Créteil, December 2021
(in French)
.
Recent developments in concurrent Kleene algebra
JetBrains Research in St Petersburg (remote talk), October 2021
.
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire MAREL in Montpellier, April 2021
.
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire ACADIE in Toulouse, April 2021
.
Observations and locality in distributed processes
IRIS scientific meeting in London, March 2021
.
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire LIRICA in Marseille, January 2021
(in French)
.
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire LOVE in Paris, January 2021
.
Recent developments in concurrent Kleene algebra
IRIS scientific meeting in London, December 2020
.
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
FSCD in Paris, July 2020
.
Recent developments in concurrent Kleene algebra
Séminaire PPS in Paris, June 2020
.
Pomsets with boxes: towards Atomic CKA
Highlights in Warsaw, September 2019
.
Pomset languages and concurrent Kleene algebra
Theory seminar - QMU in London, February 2018
.
Pomset languages and concurrent Kleene algebras
Séminaire automates in Paris, November 2017
.
On Decidability of Concurrent Kleene Algebra
CONCUR in Berlin, September 2017
.