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

DOI10.1007/978-3-030-30942-8_16zbMath1539.68159MaRDI QIDQ6535953

Rüdiger Ehlers

Publication date: 14 March 2024

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)

Cites Work

• Unnamed Item
• Unnamed Item
• Flash memory efficient LTL model checking
• Short Witnesses and Accepting Lassos in ω-Automata
• Model Checking Software
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
• Depth-First Search and Linear Graph Algorithms
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Ultimately periodic words of rational ω-languages
• Correct Hardware Design and Verification Methods
• A fragment of linear temporal logic for universal very weak automata

Related Items (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?