Concurrent Kleene Algebra: Free Model and Completeness

with Tobias Kappé, Alexandra Silva and Fabio Zanasi .

conference paper, in ESOP 2018

Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the semantics proposed in the original paper is the free model of CKA with bounded parallel iteration, meaning the completeness of these axioms. This result settles a conjecture of Hoare and collaborators. Moreover, it allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.

@inproceedings{kbsz18,
    title = "Concurrent Kleene Algebra: Free Model and Completeness",
    author = "{Paul Brunet}, {Tobias Kappé}, {Alexandra Silva}, {Fabio Zanasi}",
    year = 2018,
    booktitle = "ESOP",
    doi = "10.1007/978-3-319-89884-1_30"
}

Links

	Permanent link
	Preprint on arXiV
	Paper on Springer Link

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
	Pomset languages and concurrent Kleene algebras Séminaire automates in Paris, November 2017.	More
	On Decidability of Concurrent Kleene Algebra CONCUR in Berlin, September 2017.	More
Related papers
	Equivalence checking for weak bi-Kleene 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 Series-Parallel Pomset Languages: Rationality, Context-Freeness 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
	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