Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
Joint Authors
Mao, Xiaoguang
Wang, Rui
Liu, Wanwei
Li, Tun
Wang, Ji
Source
Journal of Applied Mathematics
Issue
Vol. 2013, Issue 2013 (31 Dec. 2013), pp.1-12, 12 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2013-07-14
Country of Publication
Egypt
No. of Pages
12
Main Subjects
Abstract EN
As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking.
However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic.
In this paper, we present a semantic BMC encoding approach to deal with the mixture of ETLf and ETLl.
Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it.
The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.
American Psychological Association (APA)
Wang, Rui& Liu, Wanwei& Li, Tun& Mao, Xiaoguang& Wang, Ji. 2013. Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives. Journal of Applied Mathematics،Vol. 2013, no. 2013, pp.1-12.
https://search.emarefa.net/detail/BIM-473487
Modern Language Association (MLA)
Wang, Rui…[et al.]. Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives. Journal of Applied Mathematics No. 2013 (2013), pp.1-12.
https://search.emarefa.net/detail/BIM-473487
American Medical Association (AMA)
Wang, Rui& Liu, Wanwei& Li, Tun& Mao, Xiaoguang& Wang, Ji. Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives. Journal of Applied Mathematics. 2013. Vol. 2013, no. 2013, pp.1-12.
https://search.emarefa.net/detail/BIM-473487
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-473487