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

来源：计算机工程与科学杂志2025年第06期北京时间：

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

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

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

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

基金资助：国家自然科学基金(61976065,62376066)