Introduction to Kleene Algebra

Course Information

## Instructor
Dexter Kozen |
## Teaching AssistantIn my dreams |
## AdministratorKelly Patwell |

Mondays 5:15-7pm, Upson 5126.

By appointment. For an appointment with Dexter, please contact Kelly.

The following text will be used.

- John Horton Conway,
*Regular Algebra and Finite Machines*, Chapman and Hall, London, 1971.

Other useful sources:

- J. Berstel and C. Reutenauer,
*Rational Series and Their Languages*, Springer, 1988. - Samuel Eilenberg,
*Automata, Languages and Machines*, vol. A, Academic Press, 1974. - Arto Salomaa and Matti Soittola,
*Automata-Theoretic Aspects of Formal Power Series*, Springer, 1978.

All handouts, articles, homework sets, etc. will be available on the web in pdf or html format. It is your responsibility to check often for new postings. For viewing pdf files, we recommend Adobe Reader, available free of charge.

There will be biweekly homework sets consisting of 3-5 problems, due in class on the due date. You may collaborate on homework. If you collaborate, pass in one copy of your solutions with the names of all collaborators. Acknowledge all sources, including others in the class from whom you obtained ideas. Late homework will not be accepted without a good excuse. Assignments and solutions will be posted on the web.

There will be two 72-hour takehome exams, open book and notes. No collaboration is allowed on the exams.

Approximate weights: Homework 50%, exams 25% each.

Familiarity with the content of CS481 is essential. In addition, familiarity with the content of CS682 and (CS482 or CS681), as well as elementary logic and algebra (Math 432, Math 481, Math 681) will be helpful. In particular, we will assume knowledge of:

- discrete mathematical structures, including graphs, trees, dags
- O( ) and o( ) notation
- finite automata, regular expressions, pushdown automata, context-free languages
- Turing machines and computability.

Entries in *italics* will be covered as time permits.

- automata and regular expressions
- basic results of Kleene algebra
- model theory -- language, relational, and trace models
- matrix algebras and automata as matrices
- formal power series in noncommuting variables
- Salomaa's completeness theorem
- Redko's theorem
- deductive completeness over Reg and Rel
- related structures -- S-algebras, closed semirings
- ideal completion
- PSPACE completeness of the equational theory
- Kleene algebra with tests
- guarded strings and automata on traces
- reduction of the Hoare theory to the equational theory
- program schematology
- commutative Kleene algebra
- Brzozowski derivatives and Taylor's theorem
- algebraic closure and Parikh's theorem
- applications in program verification