Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
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 semanti...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/462532 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832555089051516928 |
|---|---|
| author | Rui Wang Wanwei Liu Tun Li Xiaoguang Mao Ji Wang |
| author_facet | Rui Wang Wanwei Liu Tun Li Xiaoguang Mao Ji Wang |
| author_sort | Rui Wang |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-f923258bbaec47adb02f661300df545f |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-f923258bbaec47adb02f661300df545f2025-02-03T05:49:44ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/462532462532Bounded Model Checking of ETL Cooperating with Finite and Looping Automata ConnectivesRui Wang0Wanwei Liu1Tun Li2Xiaoguang Mao3Ji Wang4College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, ChinaCollege of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, ChinaCollege of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, ChinaCollege of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, ChinaCollege of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, ChinaAs 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.http://dx.doi.org/10.1155/2013/462532 |
| spellingShingle | Rui Wang Wanwei Liu Tun Li Xiaoguang Mao Ji Wang Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives Journal of Applied Mathematics |
| title | Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives |
| title_full | Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives |
| title_fullStr | Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives |
| title_full_unstemmed | Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives |
| title_short | Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives |
| title_sort | bounded model checking of etl cooperating with finite and looping automata connectives |
| url | http://dx.doi.org/10.1155/2013/462532 |
| work_keys_str_mv | AT ruiwang boundedmodelcheckingofetlcooperatingwithfiniteandloopingautomataconnectives AT wanweiliu boundedmodelcheckingofetlcooperatingwithfiniteandloopingautomataconnectives AT tunli boundedmodelcheckingofetlcooperatingwithfiniteandloopingautomataconnectives AT xiaoguangmao boundedmodelcheckingofetlcooperatingwithfiniteandloopingautomataconnectives AT jiwang boundedmodelcheckingofetlcooperatingwithfiniteandloopingautomataconnectives |