Seth Fogarty, Size Doesn't Matter When You Have Good (Automata-Theoretic) Technique

I compare tools for complementing Buechi automata with a recent termination-analysis algorithm. In 2001, Lee et al. presented the size-change termination (SCT) problem, along with both a reduction to Buechi containment and their own algorithm. Their algorithm strongly resembles the initial Ramsey-based complementation constructions for Buechi automata, which have since been supplanted by rank-based constructions with exponentially better bounds.

After proving the SCT algorithm is a realization of the old Ramsey-based complementation construction, I empirically compare the SCT algorithm with exponentially better rank-based techniques. Surprisingly, the 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.