• Complex
  • Title
  • Keyword
  • Abstract
  • Scholars
  • Journal
  • ISSN
  • Conference
搜索

Author:

苏开乐 (苏开乐.) | 骆翔宇 (骆翔宇.) | 吕关锋 (吕关锋.)

Indexed by:

CQVIP PKU CSCD

Abstract:

提出了一个关于时态逻辑CTL* 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL*规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL*符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL*的子集逻辑(如CTL,LTL)进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL*符号化模型检测是可能的.

Keyword:

模型检测 时态逻辑 有序二值判定图(OBDD)

Author Community:

  • [ 1 ] [苏开乐]中山大学
  • [ 2 ] [骆翔宇]中山大学
  • [ 3 ] [吕关锋]北京工业大学

Reprint Author's Address:

Email:

Show more details

Related Keywords:

Related Article:

Source :

计算机学报

ISSN: 0254-4164

Year: 2005

Issue: 11

Volume: 28

Page: 1798-1806

Cited Count:

WoS CC Cited Count: 0

SCOPUS Cited Count:

ESI Highly Cited Papers on the List: 0 Unfold All

WanFang Cited Count: 85

Chinese Cited Count:

30 Days PV: 2

Affiliated Colleges:

Online/Total:600/5435183
Address:BJUT Library(100 Pingleyuan,Chaoyang District,Beijing 100124, China Post Code:100124) Contact Us:010-67392185
Copyright:BJUT Library Technical Support:Beijing Aegean Software Co., Ltd.