Current Announcements
[Click here for archived announcements.]
| Date | Topic | Description |
|---|---|---|
| Wed 5/8 | Final grades | The official due date for final projects is 4:30pm May 13, but as usual we will allow some flexibility. However, Tuesday May 28 is the absolute last day for us to get final grades in, so please keep that in mind. |
Course Info
Overview
Kleene algebra is the algebra of regular expressions and finite automata, structures of fundamental importance in computer science. Kleene algebra is the algebraic theory of these objects, although it has many other natural and useful interpretations: relational algebra, programming language semantics, program logics, automata and formal languages, network programming, computational geometry, and the design and analysis of algorithms. In this course we will explore the theory and applications of Kleene algebra and coalgebra, including models, deductive systems, completeness and complexity results, and applications in the areas mentioned above.
Prerequisites
CS 4810 and CS 6860 or permission.
Time & Place
10:10–11:25am TR, Hollister 312
Staff
| POSITION | NAME | CONTACT | OFFICE HOURS |
|---|---|---|---|
| Instructor | Dexter Kozen |
Turn on JavaScript to view email address
607-255-9209 w 607-592-2437 m |
436 Gates TR 1–2pm or by appt |
| TA | Goktug Saatcioglu | Turn on JavaScript to view email address | 400 Rhodes T 9–10am |
| Administrative Support | Corey Torres |
Turn on JavaScript to view email address
607-255-9197 w |
401 Gates MWR 8am–4:30pm |
Website
The course website is http://www.cs.cornell.edu/Courses/cs6861/. Announcements will be posted on the home page. Check frequently for new announcements.
Workload & Grading
Occasional readings as assigned.
Biweekly homework assignments with 4–6 problems each, 60% of grade.
You may work with a partner.
Final paper, software project, or takehome exam at the student's option, 40% of grade.
This is to be done individually. Final papers and projects are due at 4:30pm, May 13.
CMS
Homework will be available on CMS. Your solutions should be in .pdf format and should be submitted to CMS. If you work with a partner, please form a group in CMS. Only one person needs to submit the homework. Click here to access.
Ed
Ed is a discussion forum for all course-related questions. Click here to access.
Sources (recommended, not required)
Dexter Kozen, Automata and Computability, Springer 1997. [§2-6] [§7-12] [§13-16]
Lecture Notes
Lecture notes 4, 2/1
Lecture notes 5-6, week of 2/5
Lecture notes 7-8, week of 2/12
Lecture notes 9-10, week of 2/19
Lecture notes 11, 2/29
Lecture notes 12, 3/5 (Spencer)
Lecture notes 12, 3/5 (Luke)
Lecture notes 13, 3/7 (Mark)
Lecture notes 14-15, week of 3/11
Lecture notes 16-17, week of 3/18
Lecture notes 18-19, week of 3/25
Lectures 20-21, week of 4/8 from here
Lectures 22-23, week of 4/15 from here
Lectures 24-25, week of 4/22 from here
Lectures 26-27, week of 4/29 from here and here
Handouts
Equational Horn Logic
Leinster, Basic Category Theory
Rutten, Universal Coalgebra
Silva thesis
Hardin & Kozen, On the elimination of hypotheses in KAT
Notes on the Horn theory of KAT
Gibbons & Rytter, On the decidability of some problems about rational subsets of free partially commutative monoids
Notes on PDL
Some papers on KA-related subjects
Index here. Take a look at these for some final project ideas. I will be adding more to this list as time goes on.
Approximate Syllabus (subject to change)
Models of Kleene algebra: standard language models, regular sets,
context-free languages, binary relations, trace models, (min,+)
algebra (tropical semiring), Viterbi algebra, convex sets
Relations among models, ideal completion
Finite automata and Kleene's theorem
Axiomatization of KA: standard axiomatization, quantales, closed
semirings, star-continuity
Completeness of the equational theory: star-continuity,
standard axiomatization
Complexity: PSPACE completeness of the equational theory,
Pi-1-1-completeness of the Horn theory
Redko's theorem, Aceto et al: no finite purely equational
axiomatization for KA
Parikh's Theorem in Commutative KA
Kleene Algebra with Tests (KAT): models, completeness, complexity
KAT subsumes Hoare logic, completeness of KAT for the Hoare theory of
relational models, complexity of KAT and PHL
Schematic KAT (SKAT), program schematology
Coalgebraic theory of KA and KAT, automata on guarded strings,
completeness, complexity
Concurrent KA, NetKAT
Academic Integrity
It goes without saying that the utmost degree of academic integrity is expected of everyone. Please familiarize yourself with The Essential Guide to Academic Integrity at Cornell. Acknowledge all sources, including Internet sources and other students with whom you discussed ideas. It is ok to discuss ideas with others as long as you acknowledge them.
Special Needs
Special needs will be accommodated. Please let us know as soon as possible.