Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives

Rui Wang, Wanwei Liu, Tun Li, Xiaoguang Mao and Ji Wang

Journal of Applied Mathematics, 2013, vol. 2013, issue 1

Abstract: 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.

Date: 2013
References: Add references at CitEc
Citations:

Downloads: (external link)
https://doi.org/10.1155/2013/462532

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:wly:jnljam:v:2013:y:2013:i:1:n:462532

Access Statistics for this article

More articles in Journal of Applied Mathematics from John Wiley & Sons
Bibliographic data for series maintained by Wiley Content Delivery ().