Current Announcements
[Click here for archived announcements.]
| Date | Topic | Description |
|---|---|---|
| Mon 3/25 | Final deliverable | I have posted some papers (index here) on some KA-related subjects as inspiration for final paper or project ideas. You are by no means limited to these. I will be posting more shortly. |
| Mon 3/25 | HW5 | HW5 is available in CMS, due Wednesday 4/17. Partners allowed as usual, but please form a group in CMS. |
| Mon 4/8 | This week | Lectures this week will cover the basics of NetKAT. No lecture notes, but the original papers are here and here. |
| Mon 4/8 | Final projects | Please get in touch with Goktug sometime this week to go over your final project proposals. Please also submit a synopsis of your proposal (no more than one page please) to CMS. |
| Wed 4/10 | Office hours | Dexter's office hours tomorrow 4/11 postponed to 4:30-5:30 due to an A exam. |
| Mon 4/15 | Office hours | Dexter's office hours Thu 4/18 moved to 11:30-12:30 due to travel. |
| Mon 4/15 | Next week | Dexter will be out of town the week of 4/22. Goktug will be lecturing. |
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
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.