View in EDS PDF Full Text

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

Saved in:
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
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 186266948
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: 基于量化布尔公式的超时态计算树逻辑有界模型检测.
– Name: TitleAlt
  Label: Alternate Title
  Group: TiAlt
  Data: Bounded model checking of HyperCTL based on QBF.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22明志勇%22">明志勇</searchLink><relatesTo>1,2,3</relatesTo><br /><searchLink fieldCode="AR" term="%22王以松%22">王以松</searchLink><relatesTo>2,3</relatesTo><i> yswang@gzu.edu.cn</i><br /><searchLink fieldCode="AR" term="%22冯仁艳%22">冯仁艳</searchLink><relatesTo>4</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Computer+Engineering+%26+Science+%2F+Jisuanji+Gongcheng+yu+Kexue%22">Computer Engineering & Science / Jisuanji Gongcheng yu Kexue</searchLink>. Jun2025, Vol. 47 Issue 6, p1062-1070. 9p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Time+complexity%22">Time complexity</searchLink><br /><searchLink fieldCode="DE" term="%22Checks%22">Checks</searchLink><br /><searchLink fieldCode="DE" term="%22Semantics%22">Semantics</searchLink><br /><searchLink fieldCode="DE" term="%22Algorithms%22">Algorithms</searchLink><br /><searchLink fieldCode="DE" term="%22Logic%22">Logic</searchLink>
– Name: Abstract
  Label: Abstract (English)
  Group: Ab
  Data: 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]
– Name: Abstract
  Label: Abstract (Chinese)
  Group: Ab
  Data: 超时态属性的模型检测是形式化验证的重要研究课题。超时态计算树逻辑 HyperCTL”扩展了计算树逻辑CTL”, 以显式地量化系统多个执行路径上的性质。针对HyperCTL”模型检测的高时间复杂度的问题, 首先为HyperCTL”提出了有界模型语义, 其次提出了基于量化布尔公式的HyperCTL”有界模型检测算法, 分析了该算法的正确性, 最后实现了HyperCTL”有界模型检测原型工具Hybmc。实验结果表明, Hybme的有界模型检测效率显著优于HyperLTL有界模型检测工具 HyperQube. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=186266948
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.3969/j.issn.1007-130X.2025.06.012
    Languages:
      – Code: chi
        Text: Chinese
    PhysicalDescription:
      Pagination:
        PageCount: 9
        StartPage: 1062
    Subjects:
      – SubjectFull: Time complexity
        Type: general
      – SubjectFull: Checks
        Type: general
      – SubjectFull: Semantics
        Type: general
      – SubjectFull: Algorithms
        Type: general
      – SubjectFull: Logic
        Type: general
    Titles:
      – TitleFull: 基于量化布尔公式的超时态计算树逻辑有界模型检测.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: 明志勇
      – PersonEntity:
          Name:
            NameFull: 王以松
      – PersonEntity:
          Name:
            NameFull: 冯仁艳
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 1007130X
          Numbering:
            – Type: volume
              Value: 47
            – Type: issue
              Value: 6
          Titles:
            – TitleFull: Computer Engineering & Science / Jisuanji Gongcheng yu Kexue
              Type: main
ResultId 1