CS 6861 Spring 2024  —  Introduction to Kleene Algebra

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.