Joint
Invited
CONCUR
FMICS
Q+F
Category Theory for Fast Model Checking Algorithms
Category theory has seen several “killer applications” in computer science, such as those in functional programming, coalgebraic process theory, and quantum computation. In this talk, I will showcase another application that I believe is big: in model checking. I will first give an overview of basic categorical structures in model checking, where the use of category theory is motivated as a natural generalization of lattice theory. I will then exhibit some recent work of ours where category theory gives us fast model checking algorithms. It does so via the general axiomatization of structures that enable fast algorithms, and via the identification of “boundary conditions” in the search for efficient heuristics.