CS786 Spring 04
Introduction to Kleene Algebra
Course Information

Staff

Instructor Dexter Kozen kozen@cs.cornell.edu Upson 5143 255-9209 office 257-4579 home 592-2437 cell

Teaching Assistant In my dreams

Administrator Kelly Patwell patwell@cs.cornell.edu Upson 5147 255-7790 office

Time and Place

Mondays 5:15-7pm, Upson 5126.

Office Hours

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

Sources

Textbooks

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.

Handouts

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.

Homework and Exams

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.

Prerequisites

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.

Approximate Syllabus

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