Abstract
We compare tools for complementing nondeterministic Büchi automata with a recent termination-analysis algorithm. Complementation of Büchi 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üchi automata and a Ramsey-based algorithm. This algorithm strongly resembles the initial complementation constructions for Büchi 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.
A full version of this paper, including proofs, is available at http://www.cs.rice.edu/~sfogarty/tacas09-supplement.pdf
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ben-Amram, A.M., Lee, C.: Program termination analysis in polynomial time. ACM Trans. Program. Lang. Syst 29(1) (2007)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: ICLMPS, pp. 1–12. Stanford University Press (1962)
Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of Computer and Systems Science 8, 117–141 (1974)
Doyen, L., Raskin, J.-F.: Improved algorithms for the automata-based approach to model-checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 451–465. Springer, Heidelberg (2007)
Emerson, A.E., Sistla, A.P.: Deciding full branching time logics. Information and Control 61(3), 175–201 (1984)
Frederiksen, C.C.: A simple implementation of the size-change termination principle. Tech. Rep. D-442, DIKU (2001)
Glenstrup, A.J.: Terminator ii: Stopping partial evaluation of fully recursive programs. Master’s thesis, DIKU, University of Copenhagen (June 1999)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. Transactions on Computational Logic, 409–429 (2001)
Lee, C., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81–92 (2001)
Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)
Sereni, D., Jones, N.D.: Termination analysis of higher-order functional programs. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 281–297. Springer, Heidelberg (2005)
Safra, S.: On the Complexity of ω-Automat. In: FOCS, pp. 319–327 (1988)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 217–237. Springer, Heidelberg (1985)
Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS, vol. 3835, pp. 396–411. Springer, Heidelberg (2005)
Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137–150. Springer, Heidelberg (2007)
Wahlstedt, D.: Detecting termination using size-change in parameter values. Master’s thesis, Göteborgs Universitet (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fogarty, S., Vardi, M.Y. (2009). Büchi Complementation and Size-Change Termination. In: Kowalewski, S., Philippou, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2009. Lecture Notes in Computer Science, vol 5505. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00768-2_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-00768-2_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00767-5
Online ISBN: 978-3-642-00768-2
eBook Packages: Computer ScienceComputer Science (R0)