Skip to content

CS 6861 Fall 2025 — Introduction to Kleene Algebra

Current Announcements

  • Mon 8/25: First class today!

Course Info

Overview

Kleene algebra is the framework that underlies the study of regular expressions and finite automata. Beyond its classical role in automata and formal language theory, it has a wide range of natural interpretations, including relational algebra, semantics of programming languages, program logics, network programming, computational geometry, and the analysis of algorithms. Its expressive power and versatility make it a central tool in both theoretical computer science and practical verification.

This course offers an exploration of the theory and applications of Kleene algebra, including a coalgebraic view. We will examine fundamental models and deductive systems, study key results on completeness and computational complexity, and investigate applications across diverse domains. Particular emphasis will be placed on the interplay between algebraic and coalgebraic perspectives, highlighting how these complementary approaches provide powerful techniques for reasoning.

Prerequisites

CS 4810 and CS 6860 or permission.

Time & Place

10:10–11:25am MW, Hollister 110

Staff

  • Instructor: Alexandra Silva — Office: 434 Gates — Office hours: M 1.00–2.30pm or by appointment
  • Administrative support: Corey Torres — 401 Gates — MWR 8am–4:30pm

Website, CMS, Ed

Workload & Grading

  • Biweekly homework: 60% (you may work with a partner)
  • Final paper: 40% — due December 15, 4:30pm
  • Occasional readings as assigned

Syllabus (Approximate)

Topics include (subject to change):

  • Models of Kleene algebra: languages, regular sets, binary relations, trace models, (min,+) algebra (tropical semiring), Viterbi algebra, convex sets
  • Finite automata and Kleene's theorem
  • Axiomatizations: standard axiomatization, quantales, closed semirings, star-continuity
  • Completeness of the equational theory: star-continuity, standard axiomatization
  • Complexity: PSPACE-complete equational theory.
  • 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/KAT: automata on guarded strings, completeness, complexity
  • NetKAT

Schedule

  • 8/25: Introduction, first examples of a Kleene Algebra
  • 8/27: Kleene Algebra, axiomatization and models

Handouts

  • Some useful background on automata: Dexter Kozen, Automata and Computability, Springer 1997. (pdfs courtesy of Dexter: 2-6, 7-12, 13-16.)

  • A set of draft lecture notes

Policies

Academic Integrity

The utmost degree of academic integrity is expected of everyone. Acknowledge all sources, including Internet sources and collaborators. It is ok to discuss ideas with others as long as you acknowledge them. See Cornell's guidance: https://gradschool.cornell.edu/policies/academic-integrity/

Accessibility & Special Needs

Special needs will be accommodated—please reach out as soon as possible to arrange accommodations.