Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification

DOI10.1007/978-3-031-16681-5_17MaRDI QIDQ6160567zbMATH OpenOpenAlexFDO

Authors Edith Hemaspaandra, David E. Narváez

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-16681-5_17

zbMATH Keywords

finite automataformal methodsinteractive theorem provingIsabelle/HOLQBFQSAT

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• A Compact Proof of Decidability for Regular Expression Equivalence
• On Equivalence Checking of Nondeterministic Finite Automata
• Aggregation-based minimization of finite state automata
• On path equivalence of nondeterministic finite automata
• Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata

Cites work

• A First Step Towards a Unified Proof Checker for QBF
• A unified proof system for QBF preprocessing
• Checking NFA equivalence with bisimulations up to congruence
• Circuit-based search space pruning in QBF
• Compressing BMC encodings with QBF
• Decidability and shortest strings in formal languages
• Dependency learning for QBF
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Experimental Evaluation of Classical Automata Constructions
• Formally verifying the solution to the Boolean Pythagorean triples problem
• scientific article; zbMATH DE number 5344975 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3460178 (Why is no real title available?)
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• scientific article; zbMATH DE number 7354705 (Why is no real title available?)
• Non-prenex QBF solving using abstraction
• NONDETERMINISTIC DESCRIPTIONAL COMPLEXITY OF REGULAR LANGUAGES
• On the Bounds for State-Set Size in the Proofs of Equivalence Between Deterministic, Nondeterministic, and Two-Way Finite Automata
• Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae
• Relationships between nondeterministic and deterministic tape complexities
• Solving QBF by abstraction
• State complexity of some operations on binary regular languages
• The state complexities of some basic operations on regular languages

Cited in

(1)

• scientific article; zbMATH DE number 5542982 (Why is no real title available?)

This page was built for publication: Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification

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