{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:32Z","timestamp":1760202632968,"version":"3.41.2"},"reference-count":31,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,27]],"date-time":"2012-02-27T00:00:00Z","timestamp":1330300800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["0613889"],"award-info":[{"award-number":["0613889"]}]},{"name":"National Science Foundation","award":["0216467"],"award-info":[{"award-number":["0216467"]}]},{"name":"National Science Foundation","award":["0311326"],"award-info":[{"award-number":["0311326"]}]},{"name":"National Science Foundation","award":["0728882"],"award-info":[{"award-number":["0728882"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We compare tools for complementing nondeterministic B\\\"uchi automata with a\nrecent termination-analysis algorithm. Complementation of B\\\"uchi automata is a\nkey step in program verification. Early constructions using a Ramsey-based\nargument have been supplanted by rank-based constructions with exponentially\nbetter bounds. In 2001 Lee et al. presented the size-change termination (SCT)\nproblem, along with both a reduction to B\\\"uchi automata and a Ramsey-based\nalgorithm. The Ramsey-based algorithm was presented as a more practical\nalternative to the automata-theoretic approach, but strongly resembles the\ninitial complementation constructions for B\\\"uchi automata. We prove that the\nSCT algorithm is a specialized realization of the Ramsey-based complementation\nconstruction. To do so, we extend the Ramsey-based complementation construction\nto provide a containment-testing algorithm. Surprisingly, empirical analysis\nsuggests that despite the massive gap in worst-case complexity, Ramsey-based\napproaches are superior over the domain of SCT problems. Upon further analysis\nwe discover an interesting property of the problem space that both explains\nthis result and provides a chance to improve rank-based tools. With these\nimprovements, we show that theoretical gains in efficiency of the rank-based\napproach are mirrored in empirical performance.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:13)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":4,"title":["B\\\"uchi Complementation and Size-Change Termination"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Seth","family":"Fogarty","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,2,27]]},"reference":[{"key":"10.2168\/LMCS-8(1:13)2012_Daedalus","doi-asserted-by":"crossref","unstructured":"Daedalus. Available on: http:\/\/www.di.ens.fr\/ cousot\/projects\/DAEDALUS\/index.shtml. P.A. Abdulla, Y.-F. Chen, L. Hol\u00edk, R. Mayr, and T. Vojnar. When simulation meets antichains. InTools and Algorithms for the Construction and Analysis of Systems, volume 6015 ofLecture Notes in Computer Science, pages 158-174. Springer, 2010.","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"10.2168\/LMCS-8(1:13)2012_BenAm10","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:2)2010"},{"key":"10.2168\/LMCS-8(1:13)2012_BL07","doi-asserted-by":"crossref","unstructured":"A.M. Ben-Amram and C.S. Lee. Program termination analysis in polynomial time.ACM Trans. Program. Lang. Syst., 29:5:1-5:37, January 2007.","DOI":"10.1145\/1180475.1180480"},{"key":"10.2168\/LMCS-8(1:13)2012_Buc62","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. InProc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pages 1-12. Stanford University Press, 1962."},{"key":"10.2168\/LMCS-8(1:13)2012_Cho74","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","journal-title":"Journal of Computer and Systems Science"},{"key":"10.2168\/LMCS-8(1:13)2012_CGBFG11","doi-asserted-by":"crossref","unstructured":"M. Codish, I. Gonopolskiy, A.M. Ben-Amram, C. Fuhs, and J. Giesl. SAT-based termination analysis using monotonicity constraints over the integers.Theory and Practice of Logic Programming, 26th Int'l. Conference on Logic Programming (ICLP'11) Special Issue, 11:503-520, July 2011.","DOI":"10.1017\/S1471068411000147"},{"key":"10.2168\/LMCS-8(1:13)2012_CLS05","doi-asserted-by":"crossref","unstructured":"M. Codish, V. Lagoon, and P.J. Stuckey. Testing for termination with monotonicity constraints. InTwenty First International Conference on Logic Programming, volume 3668 ofLecture Notes in Computer Science, pages 326-340. Springer-Verlag, October 2005.","DOI":"10.1007\/11562931_25"},{"key":"10.2168\/LMCS-8(1:13)2012_DR07","doi-asserted-by":"crossref","unstructured":"L. Doyen and J.-F. Raskin. Improved algorithms for the automata-based approach to model-checking. InTools and Algorithms for the Construction and Analysis of Systems, volume 4424 ofLecture Notes in Computer Science, pages 451-465. Springer, 2007.","DOI":"10.1007\/978-3-540-71209-1_34"},{"key":"10.2168\/LMCS-8(1:13)2012_DR09","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(1:5)2009"},{"key":"10.2168\/LMCS-8(1:13)2012_EL86","unstructured":"E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional\u00ce\u00bc-calculus. InProc. 1st IEEE Symp. on Logic in Computer Science, pages 267-278, 1986."},{"issue":"3","key":"10.2168\/LMCS-8(1:13)2012_ES84b","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E.A. Emerson and A.P. Sistla","year":"1984","journal-title":"Information and Control"},{"key":"10.2168\/LMCS-8(1:13)2012_Fog08","doi-asserted-by":"crossref","unstructured":"S. Fogarty. B\u00fcchi containment and size-change termination. Master's thesis, Rice University, 2008.","DOI":"10.1007\/978-3-642-00768-2_2"},{"key":"10.2168\/LMCS-8(1:13)2012_FV10","doi-asserted-by":"crossref","unstructured":"S. Fogarty and M.Y. Vardi. Efficient B\u00fcchi universality checking. InTools and Algorithms for the Construction and Analysis of Systems, volume 6015 ofLecture Notes in Computer Science, pages 205-220. Springer, 2010.","DOI":"10.1007\/978-3-642-12002-2_17"},{"key":"10.2168\/LMCS-8(1:13)2012_Fred01","unstructured":"C.C. Frederiksen. A simple implementation of the size-change termination principle. Available at: ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/D-442.ps.gz, 2001."},{"key":"10.2168\/LMCS-8(1:13)2012_FKV04","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30476-0_10"},{"key":"10.2168\/LMCS-8(1:13)2012_Glen99","unstructured":"Arne J. Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master's thesis, DIKU, University of Copenhagen, June 1999."},{"key":"10.2168\/LMCS-8(1:13)2012_GKSV03","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_10"},{"key":"10.2168\/LMCS-8(1:13)2012_JB04","doi-asserted-by":"crossref","unstructured":"N.D Jones and Nina Bohr. Termination analysis of the untyped\u00ce\u00bb-calculus. InRewriting Techniques and Applications. Proceedings, volume 3091 ofLecture Notes in Computer Science, pages 1-23. Springer, 2004.","DOI":"10.1007\/978-3-540-25979-4_1"},{"key":"10.2168\/LMCS-8(1:13)2012_Kla90","unstructured":"N. Klarlund.Progress Measures and finite arguments for infinite computations. PhD thesis, Cornell University, 1990."},{"key":"10.2168\/LMCS-8(1:13)2012_KV97b","doi-asserted-by":"publisher","DOI":"10.1109\/ISTCS.1997.595167"},{"key":"10.2168\/LMCS-8(1:13)2012_KV01","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932514"},{"issue":"2","key":"10.2168\/LMCS-8(1:13)2012_KV01c","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman and M.Y. Vardi","year":"2001","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.2168\/LMCS-8(1:13)2012_LJB01","doi-asserted-by":"crossref","unstructured":"C.S. Lee, N.D. Jones, and A.M. Ben-Amram. The size-change principle for program termination. InProc. 28th ACM Symp. on Principles of Programming Languages, pages 81-92, 2001.","DOI":"10.1145\/373243.360210"},{"key":"10.2168\/LMCS-8(1:13)2012_Mic88","unstructured":"M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988."},{"key":"10.2168\/LMCS-8(1:13)2012_Saf88","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of\u00f8mega-automata. InProc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"10.2168\/LMCS-8(1:13)2012_Sch09","unstructured":"S. Schewe. B\u00fcchi complementation made tight. In26th Int. Symp. on Theoretical Aspects of Computer Science, volume 3, pages 661-672. Schloss Dagstuhl, 2009."},{"key":"10.2168\/LMCS-8(1:13)2012_SJ05","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_19"},{"key":"10.2168\/LMCS-8(1:13)2012_SVW85","doi-asserted-by":"crossref","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. InProc. 12th Int. Colloq. on Automata, Languages, and Programming, volume 194, pages 465-474. Springer, 1985.","DOI":"10.1007\/BFb0015772"},{"key":"10.2168\/LMCS-8(1:13)2012_TV05","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_28"},{"key":"10.2168\/LMCS-8(1:13)2012_Var07a","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_10"},{"key":"10.2168\/LMCS-8(1:13)2012_Wahl00","unstructured":"David Wahlstedt. Detecting termination using size-change in parameter values. Master's thesis, G\u00f6teborgs Universitet, 2000."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1178\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1178\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:05:35Z","timestamp":1681243535000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1178"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,27]]},"references-count":31,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:13)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1110.6183","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1110.6183","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,27]]},"article-number":"1178"}}