Sixth International Conference on Quality Software (QSIC'06)
LTL Model Checking via Search Space Partition
Beijing, China
October 27-October 28
ISBN: 0-7695-2718-3
DOI Bookmark:
http://doi.ieeecomputersociety.org/10.1109/QSIC.2006.37
The applicability of model checking is often limited by the size of the industrial system. This is known as state space explosion problem. Compositional verification has been particularly successful in this regard. This paper presents an approach based on a refinement of search space partition for reducing the complexity in verification of models with non-deterministic choices and open environment. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get better reduction. As reported in the case studies, search space partition improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of the original one.
Citation:
Fei Pu, Wenhui Zhang, "LTL Model Checking via Search Space Partition," qsic, pp.418-428, Sixth International Conference on Quality Software (QSIC'06), 2006
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||