计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2003年
5期
10-12
,共3页
公平性%部分Kripke结构%计算树逻辑%模型检测
公平性%部分Kripke結構%計算樹邏輯%模型檢測
공평성%부분Kripke결구%계산수라집%모형검측
检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术,部分Kripke结构是描述部分状态空间的形式框架.文章主要讨论一类具有公平性约束条件的CTL(计算树逻辑)模型检测问题.定义了部分公平Kripke结构和公平序,分别来表征部分公平状态空间和它们之间的序关系.并给出相应的3值CTL语意和相关定理来说明部分状态空间模型检测技术同样适用于具有公平性约束条件的CTL模型检测问题.
檢測部分狀態空間是近年來齣現的有效解決狀態爆炸的模型檢測技術,部分Kripke結構是描述部分狀態空間的形式框架.文章主要討論一類具有公平性約束條件的CTL(計算樹邏輯)模型檢測問題.定義瞭部分公平Kripke結構和公平序,分彆來錶徵部分公平狀態空間和它們之間的序關繫.併給齣相應的3值CTL語意和相關定理來說明部分狀態空間模型檢測技術同樣適用于具有公平性約束條件的CTL模型檢測問題.
검측부분상태공간시근년래출현적유효해결상태폭작적모형검측기술,부분Kripke결구시묘술부분상태공간적형식광가.문장주요토론일류구유공평성약속조건적CTL(계산수라집)모형검측문제.정의료부분공평Kripke결구화공평서,분별래표정부분공평상태공간화타문지간적서관계.병급출상응적3치CTL어의화상관정리래설명부분상태공간모형검측기술동양괄용우구유공평성약속조건적CTL모형검측문제.
