Bibliographic Details
| Title: |
基于量化布尔公式的超时态计算树逻辑有界模型检测. |
| Alternate Title: |
Bounded model checking of HyperCTL based on QBF. |
| Authors: |
明志勇1,2,3, 王以松2,3 yswang@gzu.edu.cn, 冯仁艳4 |
| Source: |
Computer Engineering & Science / Jisuanji Gongcheng yu Kexue. Jun2025, Vol. 47 Issue 6, p1062-1070. 9p. |
| Subjects: |
Time complexity, Checks, Semantics, Algorithms, Logic |
| Abstract (English): |
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 checking, this study first proposes a bounded semantics for HyperCTL, followed by a bounded model checking 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. [ABSTRACT FROM AUTHOR] |
| Abstract (Chinese): |
超时态属性的模型检测是形式化验证的重要研究课题。超时态计算树逻辑 HyperCTL”扩展了计算树逻辑CTL”, 以显式地量化系统多个执行路径上的性质。针对HyperCTL”模型检测的高时间复杂度的问题, 首先为HyperCTL”提出了有界模型语义, 其次提出了基于量化布尔公式的HyperCTL”有界模型检测算法, 分析了该算法的正确性, 最后实现了HyperCTL”有界模型检测原型工具Hybmc。实验结果表明, Hybme的有界模型检测效率显著优于HyperLTL有界模型检测工具 HyperQube. [ABSTRACT FROM AUTHOR] |
|
Copyright of Computer Engineering & Science / Jisuanji Gongcheng yu Kexue is the property of Computer Engineering & Science and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
