Title: Ramsey-Based Buechi Complementation

Abstract:
This talk presents a case study in algorithm evaluation. The
complementation of Buechi automata is a key step in program
verification. Early constructions using a Ramsey-based argument have
been supplanted by rank-based constructions with exponentially better
bounds.  In 2001 Lee et al. presented the size-change termination
(SCT) problem, along with both a reduction to Buechi automata and a
Ramsey-based algorithm. This algorithm strongly resembles the
Ramsey-based complementation constructions for Buechi automata.

We prove that the SCT algorithm is a specialized realization of the
Ramsey-based complementation construction. Surprisingly, empirical
analysis suggests Ramsey-based approaches are superior over the domain
of SCT problems. Upon further analysis we discover an interesting
property of the problem space that both explains this result and
provides a chance to improve rank-based tools. With these
improvements, we show that theoretical gains in efficiency are
mirrored in empirical performance, but that the difference is smaller
than we might expect.

Motivated by the above discovery, we move our investigation to the
realm of Buechi universality problems. The best rank-based algorithm
for Buechi universality, by Doyen and Raskin, employs a subsumption
technique to minimize the size of the working set. The strongest
Ramsey-based SCT tool, from Ben-Amram and Lee, also uses a subsumption
technique, although only for the special case of SCT problems. We
extend the subsumption technique of Ben-Amram and Lee to the general
case of Buechi universality problems, and experimentally demonstrate
the necessity of subsumption for the scalability of the Ramsey-based
approach.

We then empirically compare the Ramsey-based tool to the rank-based
tool over a terrain of random Buechi universality problems. We
discover that the two algorithms exhibit distinct behavior over this
problem terrain.  As expected, on many of the most difficult areas the
rank-based approach provides the superior tool. Surprisingly, there
also exist several areas, including the area most difficult for
rank-based tools, on which the Ramsey-based solver scales better than
the rank-based solver. These results demonstrates the pitfalls of
using only worst-case complexity to evaluate algorithms, while also
highlighting some of the difficulties in experimental evaluation.