Model checking -regular properties with decoupled search

DOI10.1007/978-3-030-81688-9_19MaRDI QIDQ832281zbMATH OpenOpenAlexFDO

Authors Daniel Gnad, Jan Eisenhut, Alberto Lluch Lafuente, J. Hoffmann

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81688-9_19

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Star-Topology Decoupling in SPIN
• Star-topology decoupled state space search
• Strong stubborn set pruning for star-topology decoupled state space search
• Local search in model checking
• Combining search space partition and abstraction for LTL model checking

Cites work

• A stubborn attack on state explosion
• An automata-theoretic approach to branching-time model checking
• An improvement of McMillan's unfolding algorithm
• Combining partial-order reductions with on-the-fly model-checking.
• Cunf: a tool for unfolding and verifying Petri nets with read arcs
• Determinization of Büchi-Automata
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 1670845 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 177519 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• scientific article; zbMATH DE number 1744959 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• Nested emptiness search for generalized Büchi automata
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Star-topology decoupled state space search
• Star-Topology Decoupling in SPIN
• Strong stubborn set pruning for star-topology decoupled state space search
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(4)

• Star-topology decoupled state space search
• BFS-based model checking of linear-time properties with an application on GPUs
• Strong stubborn set pruning for star-topology decoupled state space search
• Star-Topology Decoupling in SPIN

Describes a project that uses

Uses Software

• PRISM
• SPIN
• NuSMV
• Cunf

This page was built for publication: Model checking \(\omega \)-regular properties with decoupled search

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