Weak alternating automata are not that weak

DOI10.1145/377978.377993zbMath1171.68551OpenAlexW2059045337MaRDI QIDQ3549125

Orna Kupferman, Moshe Y. Vardi

Publication date: 21 December 2008

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Related Items

Trading Bounds for Memory in Games with Counters ⋮ Conjunctive grammars and alternating pushdown automata ⋮ Automata Theory and Model Checking ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL ⋮ Bounded model checking of ETL cooperating with finite and looping automata connectives ⋮ Fuzzy alternating Büchi automata over distributive lattices ⋮ Unnamed Item ⋮ On the power of finite ambiguity in Büchi complementation ⋮ SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA ⋮ Towards a grand unification of Büchi complementation constructions ⋮ Profile trees for Büchi word automata, with application to determinization ⋮ From bidirectionality to alternation. ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ Unnamed Item ⋮ On the translation of automata to linear temporal logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Linear temporal logic symbolic model checking ⋮ The \(\mu\)-calculus alternation hierarchy collapses over structures with restricted connectivity ⋮ Büchi Store: An Open Repository of Büchi Automata ⋮ From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata ⋮ Büchi Automata Can Have Smaller Quotients ⋮ Coinductive Algorithms for Büchi Automata ⋮ Visibly linear temporal logic ⋮ Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces ⋮ From Philosophical to Industrial Logics ⋮ From Monadic Logic to PSL ⋮ Automata-Theoretic Model Checking Revisited ⋮ Lattice Automata ⋮ Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata ⋮ Büchi Complementation and Size-Change Termination ⋮ LR(0) conjunctive grammars and deterministic synchronized alternating pushdown automata ⋮ GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic ⋮ State of Büchi Complementation ⋮ Mediating for reduction (on minimizing alternating Büchi automata) ⋮ Unnamed Item ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Advanced Ramsey-Based Büchi Automata Inclusion Testing ⋮ Random Models for Evaluating Efficient Büchi Universality Checking ⋮ Propositional Dynamic Logic for Hyperproperties ⋮ On the Way to Alternating Weak Automata ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ BÜCHI COMPLEMENTATION MADE TIGHTER ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ \( \omega \)-automata ⋮ Fuzzy alternating automata over distributive lattices ⋮ From complementation to certification