Kleene algebra is an algebraic system for calculating with sequential composition, choice and finite iteration. Although its theory has a long history, going back to Kleene (1956) and Conway (1971), and the connections with classical relational algebra and formal language theory are well established, new theoretical connections but also more practical applications are constantly being discovered. It is becoming increasingly apparent that Kleene algebra provides a theoretically rich and general algebraic framework whose power and versatility has yet to be fully discovered.

Theory of Kleene Algebra

On the theoretical side there is much important work to be done. Recent algebraic versions of classical results in formal language theory, e.g. Parikh's theorem, point to the exciting possibility of a general algebraic theory that subsumes classical combinatorial automata and formal language theory. Although some movement in this direction took place in the seventies [mainly by Schutzenberger, Salomaa & Soittola, Kuich], much of this work was concerned with encoding specific combinatorial models in specific algebraic models such as semirings of formal power series. In contrast, recent results point to a much more general, purely axiomatic theory in the spirit of modern algebra.

The focus of the proposed Seminar, however, is on the

Applications of Kleene Algebra

It has also recently been observed that Kleene algebra provides a useful verification tool that can be used to establish basic program equivalences that arise in low-level verification tasks such as verification of communication protocols or compiler optimization. Proofs in this system are short, natural, and elegant.

For example, in compiler optimization, verification conditions are typically Horn formulas whose premises are self-evident conditions on the atomic programs and tests and whose conclusion is an equation between the unoptimized and optimized form of the program fragment. The premises are typically used to introduce and eliminate assertions valid at a particular point in the program or to allow noninterfering atomic programs and assertions to commute. It is similar to the type of reasoning with pre- and postconditions as in Hoare logic, but much less cumbersome and more versatile. It is also quite amenable to automation. Next to verification, Kleene algebra is also most useful in the formal derivation of programs.

Particular Fields of Application

• Within the field of efficient algorithms it has been applied to path problems on graphs (being closely related to the algebra of closed semirings), to convex hull algorithms and formal treatment of pointer algorithms.
• In compiler construction, Kleene algebra can be used to prove the correctness of optimization techniques for loop constructs.
• More recently, Kleene algebra has been successfully applied to the semantic description of imperative programs with non-deterministic choice. It covers both angelic and demonic composition and choice.
• Moreover, it allows a simple algebraic incorporation of assertions as well as modal and dynamic logic. Also, there are close relations with interval and temporal logic, the duration calculus and timed automata. Further applications concern switching theory.
• Finally, a particular form of Kleene algebra corresponds to quantales with unit elements. Hence there is a correspondence with linear logic.
• Extensions of Kleene algebra deal with infinite iteration. They have been used in the description and verification of protocols and in proofs about concurrent systems in general. Related systems are iteration theories , the computation calculus and the theory of ω-languages. Dropping one of the distributivity requirements for Kleene algebras leads to a system that is close to process algebras such as ACP or μCRL. Finally, there are close connections to network algebra.

Purpose of the Seminar

Compared with other algebraic approaches to semantics, such as relation algebra or sequential calculus, Kleene algebra and its relatives enjoy a particularly simple axiomatisation, since they do not use a notion of (pseudo)- converse and the corresponding axioms.

Since its basic features and rules are known even to beginner students of computer science, Kleene algebra will be more easily accepted than other formal systems and thus may serve as an effective vehicle for formal treatment of various subjects in computer science.

The above-mentioned tracks of research have so far been undertaken in a rather isolated manner. The aim of the proposed symposium is to bring the researchers from these tracks together for fruitful interaction and for helping the subject to more public visibility. To our knowledge, this is the first international symposion dedicated to the applications of Kleene algebra.