State of Büchi complementation
From MaRDI portal
Publication:3073645
DOI10.1007/978-3-642-18098-9_28zbMATH Open1297.68168arXiv1406.4575OpenAlexW1562442213MaRDI QIDQ3073645FDOQ3073645
Authors: Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay 
Publication date: 11 February 2011
Published in: Implementation and Application of Automata (Search for Journal in Brave)
Abstract: Complementation of B"uchi 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.
Full work available at URL: https://arxiv.org/abs/1406.4575
Recommendations
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Formal languages and automata (68Q45)
Cites Work
- Automata, logics, and infinite games. A guide to current research
- When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)
- Observations on determinization of Büchi automata
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- The complementation problem for Büchi automata with applications to temporal logic
- Title not available (Why is that?)
- Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique
- Weak alternating automata are not that weak
- Büchi complementation made tight
- Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
- Complementation, Disambiguation, and Determinization of Büchi Automata Unified
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- Büchi Complementation and Size-Change Termination
- Automata-Theoretic Model Checking Revisited
- Title not available (Why is that?)
- On complementing nondeterministic Büchi automata
- The Büchi Complementation Saga
- Title not available (Why is that?)
- Efficient Büchi universality checking
- BÜCHI COMPLEMENTATION MADE TIGHTER
- GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
- Antichains for the Automata-Based Approach to Model-Checking
- Title not available (Why is that?)
- State of Büchi complementation
- On minimal odd rankings for Büchi complementation
Cited In (14)
- State of Büchi complementation
- Büchi Complementation and Size-Change Termination
- Deciding monadic second order logic over \(\omega \)-words by specialized finite automata
- Complementing Büchi Automata with Ranker
- Random models for evaluating efficient Büchi universality checking
- A simple and optimal complementation algorithm for Büchi automata
- Unifying Büchi complementation constructions
- Büchi complementation and size-change termination
- Improved Ramsey-based Büchi complementation
- Ramsey-based inclusion checking for visibly pushdown automata
- On minimal odd rankings for Büchi complementation
- Unifying Büchi complementation constructions
- Sky is not the limit. Tighter rank bounds for elevator automata in Büchi automata complementation
- Learning to complement Büchi automata
This page was built for publication: State of Büchi complementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3073645)
