| Kleene's theorem establishes the link between regular expressions and finite automata. Brzozowszki described the construction of an automaton from an expression on the basis of a calculus of derivatives. Rutten used this result for the formulation of a coalgebraic calculus, in which equality of expressions is proved by coinduction. The latter coalgebraic perspective has recently been proved very relevant by the development of a number of similar coinductive calculi and Kleene theorems for many other types of automata, namely: (i) Mealy automata: there did not exist a formal language of expressions, let alone a Kleene theorem; (ii) Kleene algebras with tests (KAT): the contribution here was a new and efficient coinductive proof principle; and (iii) automata for so-called Kripke-polynomial functors: here coinductive calculi have been derived from the type (functor) of the automata. These recent and promising developments give rise to further research questions. In this project, we want to: (G1) extend the methods of (i), (ii), and (iii) above, to include also quantitative systems such as weighted and probabilistic automata; (G2) expand these methods in order to derive (in a canonical way) axiom systems for process languages specified by structural operational semantics; (G3) develop and implement efficient coinductieve algorithms for these calculi, in particular for Mealy machines and KAT; (G4) develop tool support for these techniques, building on existing verification tools such as CIRC and Coq. In this project, the combined expertise of the research groups at LIACS and CWI is further strengthened by the involvement of Prof.dr. D. Kozen (who formulated KAT) and Prof.dr. G. Rosu and D. Lucanu (developers of CIRC). |
