Büchi Complementation and Size-Change Termination
From MaRDI portal
Publication:3617751
DOI10.1007/978-3-642-00768-2_2zbMATH Open1234.68256arXiv1110.6183OpenAlexW1548996544MaRDI QIDQ3617751FDOQ3617751
Publication date: 31 March 2009
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/1110.6183
Recommendations
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- The size-change principle for program termination
- Experimental Evaluation of Classical Automata Constructions
- The complementation problem for Büchi automata with applications to temporal logic
- Deciding full branching time logic
- Weak alternating automata are not that weak
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Automata-Theoretic Model Checking Revisited
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- Programming Languages and Systems
Cited In (13)
- Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
- Complementing Büchi Automata with Ranker
- Size-Change Termination and Satisfiability for Linear-Time Temporal Logics
- Ramsey-Based Inclusion Checking for Visibly Pushdown Automata
- Linear temporal logic symbolic model checking
- Coinductive Algorithms for Büchi Automata
- State of Büchi Complementation
- Advanced Ramsey-Based Büchi Automata Inclusion Testing
- Fixed point guided abstraction refinement for alternating automata
- Title not available (Why is that?)
- Sky is not the limit. Tighter rank bounds for elevator automata in Büchi automata complementation
- Simulations in rank-based Büchi automata complementation
- Random Models for Evaluating Efficient Büchi Universality Checking
This page was built for publication: Büchi Complementation and Size-Change Termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3617751)
