Counterexample-Preserving Reduction for Symbolic Model Checking
Joint Authors
Wang, Ji
Mao, Xiaoguang
Fu, Xianjin
Dong, Wei
Wang, Rui
Liu, Wanwei
Source
Journal of Applied Mathematics
Issue
Vol. 2014, Issue 2014 (31 Dec. 2014), pp.1-13, 13 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2014-05-14
Country of Publication
Egypt
No. of Pages
13
Main Subjects
Abstract EN
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.
American Psychological Association (APA)
Liu, Wanwei& Wang, Rui& Fu, Xianjin& Wang, Ji& Dong, Wei& Mao, Xiaoguang. 2014. Counterexample-Preserving Reduction for Symbolic Model Checking. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-13.
https://search.emarefa.net/detail/BIM-491705
Modern Language Association (MLA)
Liu, Wanwei…[et al.]. Counterexample-Preserving Reduction for Symbolic Model Checking. Journal of Applied Mathematics No. 2014 (2014), pp.1-13.
https://search.emarefa.net/detail/BIM-491705
American Medical Association (AMA)
Liu, Wanwei& Wang, Rui& Fu, Xianjin& Wang, Ji& Dong, Wei& Mao, Xiaoguang. Counterexample-Preserving Reduction for Symbolic Model Checking. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-13.
https://search.emarefa.net/detail/BIM-491705
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-491705