Tools and techniques for probabilistic Kleene Algebras 
Tahiry Rabehaja

Kleene Algebras yield a complete axiomatisation of the equational theory
of regular languages, that is, the class of regular languages forms the
Kleene Algebra which is freely generated by a given (finite) alphabet.
Probabilistic Kleene Algebras take into account the existence of an
internal (probabilistic) choice; their axiomatisation is very similar to
that of a Kleene Algebra. The natural question is then: What are the
free algebras for this weaker axiomatisation? In Kleene Algebras,
completeness implies that (valid) equalities are exactly trace
equivalences of labelled transition systems. But since probabilistic
Kleene Algebras are much more similar to process algebras, certain trees
or automata under (bi)simulation equivalence are then a candidate. A
completeness proof seems rather tricky because the behaviour of the
Kleene star changes due to the lack of one distributivity law. We
present some tools such as minimisation modulo simulation equivalence
and the notion of partial derivative. We then show that the equational
theory of a probabilistic Kleene Algebra is completely characterised by
a simulation relation on derivatives.

(Joint work with Annabelle McIver and Georg Struth)