Combining search space partition and abstraction for LTL model checking

DOI10.1007/s11432-007-0073-yzbMath1142.68522OpenAlexW1964632015MaRDI QIDQ2465733

Fei Pu, Wen-Hui 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

refinementabstractionLTL model checkingsearch 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)

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Property preserving abstractions for the verification of concurrent systems
• Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation
• Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
• Making abstract interpretations complete
• Automated Technology for Verification and Analysis
• Tools and Algorithms for the Construction and Analysis of Systems

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