Journal of Applied Mathematics
Volume 2013 (2013), Article ID 462532, 12 pages
Research Article

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

College of Computer Science, National University of Defense Technology, Changsha, Hunan 410073, China

Received 8 March 2013; Accepted 14 June 2013

Academic Editor: Xiaoyu Song

Copyright © 2013 Rui Wang et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.


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 and . 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.