Combining search space partition and abstraction for LTL model checking

DOI10.1007/S11432-007-0073-YMaRDI QIDQ2465733zbMATH OpenOpenAlexFDO

Authors Fei Pu, Wenhui Zhang

Publication date 7 January 2008

Published in Science in China. Series F (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11432-007-0073-y

zbMATH Keywords

abstractionLTL model checkingrefinementsearch space partition

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 898449
• scientific article; zbMATH DE number 1948409
• Efficient patterns for model checking partial state spaces in CTL \(\cap\) LTL
• LTL-model-checking via model composition
• Automated Technology for Verification and Analysis
• Combining Abstraction Refinement and SAT-Based Model Checking
• LTL Generalized Model Checking Revisited
• An efficient approach for abstraction-refinement in model checking
• Parallel nested depth-first searches for LTL model checking

Cites work

• Automated Technology for Verification and Analysis
• Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1693039 (Why is no real title available?)
• scientific article; zbMATH DE number 1948409 (Why is no real title available?)
• scientific article; zbMATH DE number 1487866 (Why is no real title available?)
• scientific article; zbMATH DE number 2086523 (Why is no real title available?)
• scientific article; zbMATH DE number 2087639 (Why is no real title available?)
• Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation
• Making abstract interpretations complete
• Property preserving abstractions for the verification of concurrent systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(4)

• Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
• Automated Technology for Verification and Analysis
• FM 2005: Formal Methods
• Model checking \(\omega \)-regular properties with decoupled search

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Combining search space partition and abstraction for LTL model checking

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