Mechanizing the Powerset Construction for Restricted Classes of ω-Automata

DOI10.1007/978-3-540-75596-8_17zbMath1141.68430OpenAlexW1541872673MaRDI QIDQ3510798

Felix Klaedtke, Christian Dax, Jochen Eisinger

Publication date: 3 July 2008

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-75596-8_17

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items

Dissecting \texttt{ltlsynt} ⋮ Unnamed Item ⋮ Generic Emptiness Check for Fun and Profit

Uses Software

• MONA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Alternating finite automata on \(\omega\)-words
• Verifying a signature architecture: a comparative case study
• Complementing deterministic Büchi automata in polynomial time
• On syntactic congruences for \(\omega\)-languages
• Efficient minimization of deterministic weak \(\omega\)-automata
• Formalization and validation of the general inter-ORB protocol (GIOP) using PROMELA and SPIN
• MONA IMPLEMENTATION SECRETS
• Weak alternating automata are not that weak
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning
• An effective decision procedure for linear arithmetic over the integers and reals
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Mathematical Foundations of Computer Science 2003
• TYPENESS FOR ω-REGULAR AUTOMATA
• Decision problems forω-automata
• Don’t Care Words with an Application to the Automata-Based Approach for Real Addition
• Correct Hardware Design and Verification Methods