Seth Fogarty, Buechi Complementation and Size-Change Termination

We compare existing techniques for complementing nondeterministic Buechi automata with a recent termination-analysis algorithm. Efficient complementation of Buechi automata is a core problem for program verification. Early solutions 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 strongly resembling the initial complementation constructions. Initial implementations of this algorithm perform well, leading us to wonder if theoretical gains in efficiency are mirrored in empirical performance.

We first extend the Ramsey-based complementation construction to containment, allowing us to show that the SCT algorithm is a specialized realization of the Ramsey-based containment test. We can then compare Ramsey and rank based solvers on problems from either domain: SCT problems from the literature and a space of random Buechi automata. Our experiments reveal Ramsey-based solutions to be competitive or superior to rank-based tools.