Concurrent Kleene Algebra

Reference. Concurrent Kleene Algebra

Cite

Cite as @hoare2009concurrent (helia, typst) · \cite{hoare2009concurrent} (LaTeX)

BibTeX

bibtex · 7 lines

@inproceedings{hoare2009concurrent,
 title = {Concurrent {Kleene} Algebra},
 author = {Hoare, CAR Tony and M{\"o}ller, Bernhard and Struth, Georg and Wehrman, Ian},
 year = {2009},
 booktitle = {CONCUR},
 pages = {399--414}
}

hayagriva YAML (typst)

yaml · 13 lines

hoare2009concurrent:
  type: article
  title: Concurrent {Kleene} Algebra
  author:
  - Hoare, CAR Tony
  - Möller, Bernhard
  - Struth, Georg
  - Wehrman, Ian
  date: 2009
  page-range: 399-414
  parent:
    type: proceedings
    title: CONCUR

Download: hoare2009concurrent.bib · hoare2009concurrent.yml

Cited by (2)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT zhang-2026-outrunningESOP · 2026

PDF · DOI · arXiv · pldb

Kleene Algebra with Commutativity Conditions Is Undecidable azevedodeamorim-2025-kleeneCSL · 2025

We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.

DOI · arXiv

Cites 31 works (2 here)

With notes (2)

Kleene algebra with tests kozen1997kleeneTOPLAS · 1997

We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.

PDF · DOI · pldb

A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events KOZEN1994366I&C · 1994

We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa′s axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras.

DOI

External (29)

Foundations of Concurrent Kleene Algebra (2009)
Concurrent Kleene Algebra (Univ. Augsburg Technical Report 2009-04) (2009)
Graphical models of separation logic (2009)
Prover9 and Mace4 (2009)
Extending Kleene algebra with synchrony — technicalities (Prisacariu, Oslo Research Report 376) (2008)
Q-Automata: Modelling the Resource Usage of Concurrent Components (2007)
Resources, concurrency, and local reasoning (2007)
Kleene algebra with domain (2006)
From μCRL to mCRL2 (2006)
The π-calculus — A theory of mobile processes (2001)
Separation and Reduction (2000)
Categories for the working mathematician (2nd edn) (1998)
Semiring-based constraint satisfaction and optimization (1997)
Process Algebra with Iteration and Nesting (1994)
Programming from Specifications (1990)
Quantales and their applications (1990)
On the semantics of concurrency: Partial orders and transition systems (1987)
Event structures (1987)
Axioms for memory access in asynchronous hardware systems (1986)
Modeling concurrency with partial orders (1986)
& (Mulvey, Rendiconti del Circolo Matematico di Palermo 12) (1986)
Communicating sequential processes (1985)
Partial orders and the axiomatic theory of shuffle (Gischer, PhD thesis, Stanford) (1984)
On Partial Languages (1981)
Development methods for computer programs including a notion of interference (Jones, PhD thesis, Oxford) (1981)
A Calculus of Communicating Systems (1980)
Regular Algebra and Finite Machines (1971)
An axiomatic basis for computer programming (1969)
Lattice Theory (3rd edn) (1967)