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

DOI10.1007/978-3-030-94583-1_8MaRDI QIDQ2152647zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Model Checking Software
• Partial order reduction for checking LTL formulae with the next-time operator
• Tools and Algorithms for the Construction and Analysis of Systems
• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
• scientific article; zbMATH DE number 2102708

Cites work

• scientific article; zbMATH DE number 177513 (Why is no real title available?)
• scientific article; zbMATH DE number 177519 (Why is no real title available?)
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• scientific article; zbMATH DE number 1852166 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A stubborn attack on state explosion
• Automata-Theoretic Model Checking Revisited
• Depth-First Search and Linear Graph Algorithms
• Fair testing and stubborn sets
• How to calculate symmetries of Petri nets
• LTL to Büchi automata translation: fast and more deterministic
• Model Checking Software
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• Narrowing Petri net state spaces using the state equation
• One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata
• Relaxed visibility enhances partial order reduction
• Simplification of CTL formulae for efficient model checking of Petri nets
• Start pruning when time gets urgent: partial order reduction for timed systems
• Stubborn set reduction for two-player reachability games
• Stubborn sets for simple linear time properties
• Survey on Directed Model Checking
• Symbolic model checking: \(10^{20}\) states and beyond
• TAPAAL 2.0: integrated development environment for timed-arc Petri nets
• Taking Some Burden Off an Explicit CTL Model Checker
• The temporal semantics of concurrent programs

Cited in

(2)

• Partial Order Reduction for State/Event LTL
• scientific article; zbMATH DE number 1361136 (Why is no real title available?)

Describes a project that uses

Uses Software

• ITS-Tools
• SPOT
• SPIN
• TAPAAL

This page was built for publication: Automata-driven partial order reduction and guided search for LTL model checking

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