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) hasbeen successfully applied to LTL symbolic model checking. However, the expressiveness of LTL israther limited, and some important properties cannot be captured by such logic. In this paper, wepresent a semantic BMC encoding approach to deal with the mixture ofETLfandETLl. Sincesuch kind of temporal logic involves both finite and looping automata as connectives, all regularproperties can be succinctly specified with it. The presented algorithm is integrated into the modelchecker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.

[学科分类] 应用数学