Computer Science – Formal Languages and Automata Theory
Scientific paper
2011-10-27
LMCS 8 (1:13) 2012
Computer Science
Formal Languages and Automata Theory
Scientific paper
10.2168/LMCS-8(1:13)2012
We compare tools for complementing nondeterministic B\"uchi automata with a recent termination-analysis algorithm. Complementation of B\"uchi 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 B\"uchi automata and a Ramsey-based algorithm. The Ramsey-based algorithm was presented as a more practical alternative to the automata-theoretic approach, but strongly resembles the initial complementation constructions for B\"uchi automata. We prove that the SCT algorithm is a specialized realization of the Ramsey-based complementation construction. To do so, we extend the Ramsey-based complementation construction to provide a containment-testing algorithm. Surprisingly, empirical analysis suggests that despite the massive gap in worst-case complexity, 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 of the rank-based approach are mirrored in empirical performance.
Fogarty Seth
Vardi Moshe Y.
No associations
LandOfFree
Büchi Complementation and Size-Change Termination does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Büchi Complementation and Size-Change Termination, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Büchi Complementation and Size-Change Termination will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-684750