Ming-Hsien Tsai ; Seth Fogarty ; Moshe Y. Vardi ; Yih-Kuen Tsay - State of Büchi Complementation

lmcs:1059 - Logical Methods in Computer Science, December 18, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:13)2014
State of Büchi ComplementationArticle

Authors: Ming-Hsien Tsai ; Seth Fogarty ; Moshe Y. Vardi ; Yih-Kuen Tsay ORCID

    Complementation of Büchi automata has been studied for over five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. Regarding the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all of the four approaches to see how they perform in practice. In this paper, we review the four approaches, propose several optimization heuristics, and perform comparative experimentation on four representative constructions that are considered the most efficient in each approach. The experimental results show that (1) the determinization-based Safra-Piterman construction outperforms the other three in producing smaller complements and finishing more tasks in the allocated time and (2) the proposed heuristics substantially improve the Safra-Piterman and the slice-based constructions.


    Volume: Volume 10, Issue 4
    Published on: December 18, 2014
    Imported on: April 10, 2013
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE 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
    • Deep Drug Discovery and Deployment; Funder: National Science Foundation; Code: PTDC/CCI-BIO/29266/2017
    • An Automata-Theoretic Approach to Design Synthesis; Funder: National Science Foundation; Code: 0728882
    • EAPSI: Efficient Buechi Containment Testing; Funder: National Science Foundation; Code: 0913807

    13 Documents citing this article

    Consultation statistics

    This page has been seen 1593 times.
    This article's PDF has been downloaded 338 times.