The Büchi Complementation Saga

DOI10.1007/978-3-540-70918-3_2zbMATH Open1186.03062OpenAlexW1506225460MaRDI QIDQ3590920FDOQ3590920

Authors: Moshe Y. Vardi 

Publication date: 3 September 2007

Published in: STACS 2007 (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.78.6917

Recommendations

• Automated Technology for Verification and Analysis
• BÜCHI COMPLEMENTATION MADE TIGHTER
• Büchi complementation made tight
• Tools and Algorithms for the Construction and Analysis of Systems
• On complementing nondeterministic Büchi automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (28)

• A complete characterization of deterministic regular liveness properties
• Büchi complementation made tight
• \(\omega \)-automata
• A Generalization of Semenov’s Theorem to Automata over Real Numbers
• Unambiguous Büchi Is Weak
• Uncountable automatic classes and learning
• Automata-Based Termination Proofs
• State of Büchi complementation
• On-the-fly emptiness check of transition-based Streett automata
• Random models for evaluating efficient Büchi universality checking
• Title not available (Why is that?)
• On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases
• Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
• When is scalar multiplication decidable?
• An \(O(n^2)\) time algorithm for alternating Büchi games
• Automated Technology for Verification and Analysis
• Uncountable automatic classes and learning
• BÜCHI COMPLEMENTATION MADE TIGHTER
• The mu-calculus and Model Checking
• A practical decision procedure for propositional projection temporal logic with infinite models
• From Monadic Logic to PSL
• Universal first-order quantification over automata
• On complementing nondeterministic Büchi automata
• From Philosophical to Industrial Logics
• Ramsey-based inclusion checking for visibly pushdown automata
• Towards a grand unification of Büchi complementation constructions
• Simulations in rank-based Büchi automata complementation
• Model Checking Quantitative Linear Time Logic

This page was built for publication: The Büchi Complementation Saga

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3590920)