How hard is finding shortest counter-example lassos in model checking?

DOI10.1007/978-3-030-30942-8_16MaRDI QIDQ6535953zbMATH OpenFDO

Authors Rüdiger Ehlers

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_16

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Counterexamples in Probabilistic Model Checking
• Optimal proofs for linear temporal logic on lasso words
• Minimal counterexamples for linear-time probabilistic verification

Cites work

• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
• A fragment of linear temporal logic for universal very weak automata
• Depth-First Search and Linear Graph Algorithms
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Flash memory efficient LTL model checking
• scientific article; zbMATH DE number 1982201 (Why is no real title available?)
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• Model Checking Software
• Short Witnesses and Accepting Lassos in ω-Automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Ultimately periodic words of rational ω-languages

Cited in

(1)

• Tighter construction of tight Büchi automata

This page was built for publication: How hard is finding shortest counter-example lassos in model checking?

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