30 citations · 66 across the 10 of their papers we have counts for
11 papers
Partially Observable Concurrent Kleene Algebra
Jana Wagemaker, Paul Brunet, Simon Docherty +3
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and lo…
Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness
Tobias Kappé, Paul Brunet, Alexandra Silva +2
Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally mis…
A note on commutative Kleene algebra
Paul Brunet
In this paper we present a detailed proof of an important result of algebraic logic: namely that the free commutative Kleene algebra is the space of semilinear sets. The first proo…
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
Paul Brunet, David Pym
Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability…
A complete axiomatisation of reversible Kleene lattices
Paul Brunet
We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star)…
On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata
Tobias Kappé, Paul Brunet, Bas Luttik +2
Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operation…
Kleene Algebra with Observations
Tobias Kappé, Paul Brunet, Jurriaan Rot +3
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not s…
Equivalence checking for weak bi-Kleene algebra
Tobias Kappé, Paul Brunet, Bas Luttik +2
Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution ca…
Concurrent Kleene Algebra: Free Model and Completeness
Tobias Kappé, Paul Brunet, Alexandra Silva +1
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 axioms for CKA wi…
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages
Tobias Kappé, Paul Brunet, Bas Luttik +2
Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the f…
Petri Automata
Paul Brunet, Damien Pous
Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only i…