Automata-driven partial order reduction and guided search for LTL model checking

DOI10.1007/978-3-030-94583-1_8zbMath1498.68160OpenAlexW4205458663MaRDI QIDQ2152647

Jiří Srba, Nikolaj Jensen Ulrik, Simon Mejlby Virenfeldt, Peter Gjøl Jensen

Publication date: 8 July 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-94583-1_8

Mathematics Subject Classification ID

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

Uses Software

• TAPAAL
• SPIN
• SPOT
• ITS-Tools

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A stubborn attack on state explosion
• The temporal semantics of concurrent programs
• Symbolic model checking: \(10^{20}\) states and beyond
• How to calculate symmetries of Petri nets
• Simplification of CTL formulae for efficient model checking of Petri nets
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• Fair Testing and Stubborn Sets
• LTL to Büchi Automata Translation: Fast and More Deterministic
• TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets
• Stubborn Sets for Simple Linear Time Properties
• Survey on Directed Model Checking
• One Theorem to Rule Them All
• Automata-Theoretic Model Checking Revisited
• Depth-First Search and Linear Graph Algorithms
• Model Checking Software
• Relaxed visibility enhances partial order reduction
• Start pruning when time gets urgent: partial order reduction for timed systems
• Taking Some Burden Off an Explicit CTL Model Checker