基于量化布尔公式的超时态计算树逻辑有界模型检测

计算机工程与科学 ›› 2025, Vol. 47 ›› Issue (06): 1062-1070.

基于量化布尔公式的超时态计算树逻辑有界模型检测

明志勇1,2,3,王以松2,3,冯仁艳4

(1.公共大数据国家重点实验室，贵州贵阳 550025；2.贵州大学人工智能研究院，贵州贵阳 550025；
3.贵州大学计算机科学与技术学院，贵州贵阳 550025；4.贵州财经大学信息学院，贵州贵阳 550025)

收稿日期:2024-01-15 修回日期:2024-05-28 出版日期:2025-06-25 发布日期:2025-06-26
基金资助:
国家自然科学基金(61976065,62376066)

Bounded model checking of HyperCTL* based on QBF

MING Zhiyong1,2,3,WANG Yisong2,3,FENG Renyan4

(1.State Key Laboratory of Public Big Data,Guiyang 550025;
2.Institute of Artificial Intelligence,Guizhou University,Guiyang 550025;
3.College of Computer Science and Technology,Guizhou University,Guiyang 550025;
4.School of Information,Guizhou University of Finance and Economics,Guiyang 550025,China)

Received:2024-01-15 Revised:2024-05-28 Online:2025-06-25 Published:2025-06-26

摘要/Abstract

摘要： 超时态属性的模型检测是形式化验证的重要研究课题。超时态计算树逻辑HyperCTL*扩展了计算树逻辑CTL*，以显式地量化系统多个执行路径上的性质。针对HyperCTL*模型检测的高时间复杂度的问题，首先为HyperCTL*提出了有界模型语义，其次提出了基于量化布尔公式的HyperCTL*有界模型检测算法，分析了该算法的正确性，最后实现了HyperCTL*有界模型检测原型工具Hybmc。实验结果表明，Hybmc的有界模型检测效率显著优于HyperLTL有界模型检测工具HyperQube。

关键词: 超时态计算树逻辑, 有界模型检测, 量化布尔公式

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 implemented. Experimental results demonstrate that the efficiency of Hybmc’s bounded model checking significantly outperforms that of HyperQube, a bounded model checking tool for HyperLTL.

Key words: Hyper computation tree logic(HyperCTL*), bounded model checking, quantified Boolean formula(QBF)

明志勇1, 2, 3, 王以松2, 3, 冯仁艳4. 基于量化布尔公式的超时态计算树逻辑有界模型检测[J]. 计算机工程与科学, 2025, 47(06): 1062-1070.

MING Zhiyong1, 2, 3, WANG Yisong2, 3, FENG Renyan4. Bounded model checking of HyperCTL* based on QBF[J]. Computer Engineering & Science, 2025, 47(06): 1062-1070.