|
Published Articles >> Table of Contents >> Abstract
Sixth International Conference on Quality Software (QSIC'06)
pp. 418-428
LTL Model Checking via Search Space Partition
Fei Pu, Chinese Academy of Sciences, China
Wenhui Zhang, Chinese Academy of Sciences, China
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QSIC.2006.37
Send link to a friend
| Abstract |
|
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.
|
 Additional Information
|
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
|
|
