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

• Shortest counterexamples for symbolic model checking of LTL with past
• 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
• A note on on-the-fly verification algorithms
• 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
• Model checking of safety properties
• Model Checking Software
• Short Witnesses and Accepting Lassos in ω-Automata
• Shortest counterexamples for symbolic model checking of LTL with past
• Ultimately periodic words of rational ω-languages
• What went wrong: Explaining counterexamples

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)