计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2008年
z1期
169-174
,共6页
梁爱丽%朱嘉奇%王捍贫%屈婉玲
樑愛麗%硃嘉奇%王捍貧%屈婉玲
량애려%주가기%왕한빈%굴완령
模型检测%CTL*%QDDC%NP-完全
模型檢測%CTL*%QDDC%NP-完全
모형검측%CTL*%QDDC%NP-완전
在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的.
在Pandya提齣的CTL*[DC]邏輯的基礎上,對其語法和語義進行擴展,併對路徑長度進行限製,定義瞭一箇新的邏輯CTL*[k-QDDC],它可應用于實時繫統的描述和驗證.給齣瞭在Kripke結構中直接驗證CTL*[k-QDDC]邏輯公式在某狀態是否成真的基本算法.在某些假設下,也證明瞭CTL*[k-QDDC]中的某箇邏輯運算符的驗證問題是NP完全的,這就說明CTL*[k-QDDC]的驗證問題至少是NP難的.
재Pandya제출적CTL*[DC]라집적기출상,대기어법화어의진행확전,병대로경장도진행한제,정의료일개신적라집CTL*[k-QDDC],타가응용우실시계통적묘술화험증.급출료재Kripke결구중직접험증CTL*[k-QDDC]라집공식재모상태시부성진적기본산법.재모사가설하,야증명료CTL*[k-QDDC]중적모개라집운산부적험증문제시NP완전적,저취설명CTL*[k-QDDC]적험증문제지소시NP난적.
