Counterexample-Preserving Reduction for Symbolic Model Checking
The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically e...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2014-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2014/702165 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832554175727140864 |
|---|---|
| author | Wanwei Liu Rui Wang Xianjin Fu Ji Wang Wei Dong Xiaoguang Mao |
| author_facet | Wanwei Liu Rui Wang Xianjin Fu Ji Wang Wei Dong Xiaoguang Mao |
| author_sort | Wanwei Liu |
| collection | DOAJ |
| description | The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique “counterexample-preserving reduction” (CePRe, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking. |
| format | Article |
| id | doaj-art-c25210aa99a349a9862a8f495bf2df82 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2014-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-c25210aa99a349a9862a8f495bf2df822025-02-03T05:52:13ZengWileyJournal of Applied Mathematics1110-757X1687-00422014-01-01201410.1155/2014/702165702165Counterexample-Preserving Reduction for Symbolic Model CheckingWanwei Liu0Rui Wang1Xianjin Fu2Ji Wang3Wei Dong4Xiaoguang Mao5School of Computer Science, National University of Defense Technology, Changsha 410073, ChinaSchool of Computer Science, National University of Defense Technology, Changsha 410073, ChinaSchool of Computer Science, National University of Defense Technology, Changsha 410073, ChinaSchool of Computer Science, National University of Defense Technology, Changsha 410073, ChinaSchool of Computer Science, National University of Defense Technology, Changsha 410073, ChinaSchool of Computer Science, National University of Defense Technology, Changsha 410073, ChinaThe cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique “counterexample-preserving reduction” (CePRe, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking.http://dx.doi.org/10.1155/2014/702165 |
| spellingShingle | Wanwei Liu Rui Wang Xianjin Fu Ji Wang Wei Dong Xiaoguang Mao Counterexample-Preserving Reduction for Symbolic Model Checking Journal of Applied Mathematics |
| title | Counterexample-Preserving Reduction for Symbolic Model Checking |
| title_full | Counterexample-Preserving Reduction for Symbolic Model Checking |
| title_fullStr | Counterexample-Preserving Reduction for Symbolic Model Checking |
| title_full_unstemmed | Counterexample-Preserving Reduction for Symbolic Model Checking |
| title_short | Counterexample-Preserving Reduction for Symbolic Model Checking |
| title_sort | counterexample preserving reduction for symbolic model checking |
| url | http://dx.doi.org/10.1155/2014/702165 |
| work_keys_str_mv | AT wanweiliu counterexamplepreservingreductionforsymbolicmodelchecking AT ruiwang counterexamplepreservingreductionforsymbolicmodelchecking AT xianjinfu counterexamplepreservingreductionforsymbolicmodelchecking AT jiwang counterexamplepreservingreductionforsymbolicmodelchecking AT weidong counterexamplepreservingreductionforsymbolicmodelchecking AT xiaoguangmao counterexamplepreservingreductionforsymbolicmodelchecking |