State of Büchi complementation
From MaRDI portal
Publication:3073645
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 1670781 (Why is no real title available?)
- scientific article; zbMATH DE number 1701356 (Why is no real title available?)
- scientific article; zbMATH DE number 5872401 (Why is no real title available?)
- scientific article; zbMATH DE number 1408338 (Why is no real title available?)
- Antichains for the Automata-Based Approach to Model-Checking
- Automata, logics, and infinite games. A guide to current research
- Automata-Theoretic Model Checking Revisited
- BÜCHI COMPLEMENTATION MADE TIGHTER
- Büchi Complementation and Size-Change Termination
- Büchi complementation made tight
- Complementation, Disambiguation, and Determinization of Büchi Automata Unified
- Efficient Büchi universality checking
- Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
- Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique
- Observations on determinization of Büchi automata
- On complementing nondeterministic Büchi automata
- On minimal odd rankings for Büchi complementation
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- State of Büchi complementation
- The Büchi Complementation Saga
- The complementation problem for Büchi automata with applications to temporal logic
- Weak alternating automata are not that weak
- When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)
Cited in
(14)- Learning to complement Büchi automata
- Unifying Büchi complementation constructions
- Complementing Büchi Automata with Ranker
- Improved Ramsey-based Büchi complementation
- Sky is not the limit. Tighter rank bounds for elevator automata in Büchi automata complementation
- A simple and optimal complementation algorithm for Büchi automata
- Random models for evaluating efficient Büchi universality checking
- Ramsey-based inclusion checking for visibly pushdown automata
- Deciding monadic second order logic over \(\omega \)-words by specialized finite automata
- Büchi Complementation and Size-Change Termination
- State of Büchi complementation
- Unifying Büchi complementation constructions
- Büchi complementation and size-change termination
- On minimal odd rankings for Büchi complementation
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)
