Seth Fogarty ; Moshe Y. Vardi - Büchi Complementation and Size-Change Termination

lmcs:1178 - Logical Methods in Computer Science, February 27, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:13)2012
Büchi Complementation and Size-Change Termination

Authors: Seth Fogarty ; Moshe Y. Vardi

    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. 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üchi 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.


    Volume: Volume 8, Issue 1
    Published on: February 27, 2012
    Accepted on: June 25, 2015
    Submitted on: December 2, 2011
    Keywords: Computer Science - Formal Languages and Automata Theory,D.2.4
    Fundings :
      Source : OpenAIRE Research Graph
    • SOD:HCER: A Theory of Automated Design; Funder: National Science Foundation; Code: 0613889
    • MRI: Acquisition of CITI Terascale Cluster (CTC); Funder: National Science Foundation; Code: 0216467
    • Automata-Theoretic Approach to Design Verification; Funder: National Science Foundation; Code: 0311326
    • An Automata-Theoretic Approach to Design Synthesis; Funder: National Science Foundation; Code: 0728882

    Linked data

    Source : ScholeXplorer HasVersion DOI 10.48550/arxiv.1110.6183
    • 10.48550/arxiv.1110.6183
    B��chi Complementation and Size-Change Termination
    Fogarty, Seth ; Vardi, Moshe Y. ;

    4 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 350 times.
    This article's PDF has been downloaded 200 times.