Invited Talk: Dexter Kozen
On the expressive power of the modal mu-calculus over transitive graphs
We develop a coalgebraic theory of Kleene algebra with tests (KAT)
along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella
(2003) for a limited version of KAT, resolving two open problems
of Chen and Pucella. Our treatment includes a simple definition of the
Brzozowski
derivative for KAT expressions and an automata-theoretic interpretation
involving automata on guarded strings. We also give a complexity analysis,
showing that an efficient implementation of coinductive equivalence
proofs in this setting is tantamount to standard automata-theoretic
constructions. It follows that
coinductive equivalence proofs can be generated automatically in PSPACE.
This matches the bound of Worthington (2008) for the automatic generation
of equational proofs for KAT.