Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata

DOI10.1007/978-3-030-63461-2_13MaRDI QIDQ6487930zbMATH OpenFDO

Authors Julian Brunner

Publication date 21 March 2023

Full work available at URL https://doi.org/10.1007/978-3-030-63461-2_13

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Büchi complementation made tight
• Automated Technology for Verification and Analysis
• BÜCHI COMPLEMENTATION MADE TIGHTER
• Unifying Büchi complementation constructions
• Büchi automata optimisations formalised in Isabelle/HOL

Cited in

(2)

• Büchi automata optimisations formalised in Isabelle/HOL
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification

This page was built for publication: Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata

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