计算机工程与科学2025，Vol.47Issue(6)：1062-1070,9.DOI:10.3969/j.issn.1007-130X.2025.06.012
基于量化布尔公式的超时态计算树逻辑有界模型检测
Bounded model checking of HyperCTL* based on QBF
摘要
Abstract
Model checking of hyperproperties is an important research topic in formal verification.HyperCTL* extends Computation Tree Logic(CTL*)by explicitly quantifying properties over multiple execution paths of a system.To address the issue of high time complexity in HyperCTL* model check-ing,this study first proposes a bounded semantics for HyperCTL*,followed by a bounded model check-ing algorithm based on quantified Boolean formulas.The correctness of this algorithm is analyzed,and finally,a prototype system for HyperCTL* bounded model checking tool,named Hybmc,was imple-mented.Experimental results demonstrate that the efficiency of Hybmc's bounded model checking sig-nificantly outperforms that of HyperQube,a bounded model checking tool for HyperLTL.关键词
超时态计算树逻辑/有界模型检测/量化布尔公式Key words
Hyper computation tree logic(HyperCTL*)/bounded model checking/quantified Boole-an formula(QBF)分类
信息技术与安全科学引用本文复制引用
明志勇,王以松,冯仁艳..基于量化布尔公式的超时态计算树逻辑有界模型检测[J].计算机工程与科学,2025,47(6):1062-1070,9.基金项目
国家自然科学基金(61976065,62376066) （61976065,62376066）
