2010/07/21 by Cong Tian, Zhenhua Duan, Tian, Cong +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1007.3569
openalex publication_date 2010/07/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, although the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. And the abstract model needs to be further refined where an NP-hard state separation problem is often involved. In this paper, a novel method is presented by adding extra variables to the abstract model for the refinement. With this method, not only the NP-hard state separation problem is avoided, but also a smaller refined abstract model is obtained.