声明
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。
国内刊号：43-1258/TP
国际刊号：1007-130X
发布日期:
作者：明志勇1, 2, 3, 王以松2, 3, 冯仁艳4
单位：1.公共大数据国家重点实验室，贵州 贵阳 550025；2.贵州大学人工智能研究院，贵州 贵阳 550025；3.贵州大学计算机科学与技术学院，贵州 贵阳 550025；4.贵州财经大学信息学院，贵州 贵阳 550025
关键词：超时态计算树逻辑,有界模型检测,量化布尔公式,
基金：国家自然科学基金(61976065,62376066)
超时态属性的模型检测是形式化验证的重要研究课题。超时态计算树逻辑HyperCTL*扩展了计算树逻辑CTL*，以显式地量化系统多个执行路径上的性质。针对HyperCTL*模型检测的高时间复杂度的问题，首先为HyperCTL*提出了有界模型语义，其次提出了基于量化布尔公式的HyperCTL*有界模型检测算法，分析了该算法的正确性，最后实现了HyperCTL*有界模型检测原型工具Hybmc。实验结果表明，Hybmc的有界模型检测效率显著优于HyperLTL有界模型检测工具HyperQube。
来源：2025年第06期
《计算机工程与科学》期刊编辑部
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。