计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2011年
9期
70-75
,共6页
可能的Kripke结构%可能性测度%可能性计算树逻辑%一致性
可能的Kripke結構%可能性測度%可能性計算樹邏輯%一緻性
가능적Kripke결구%가능성측도%가능성계산수라집%일치성
首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到；依据可能的Kripke结构所定义的可能性测度具有其合理性等等.其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性.最后,证明了PoCTL公式有与CTL*公式中“一致性”相对应的公式.
首先,提齣瞭可能的Kripke結構的定義,建立瞭可能的Kripke結構的可能性測度空間,併分析瞭可能的Kripke結構的一繫列性質,即任一路徑轉移的可能性可由其初始狀態的可能性分佈與各轉移的可能性取下確界而得到；依據可能的Kripke結構所定義的可能性測度具有其閤理性等等.其次,給齣瞭可能性計算樹邏輯(PoCTL)的概唸,討論瞭兩箇PoCTL狀態公式以及PoCTL與經典計算樹邏輯(CTL)公式的等價性.最後,證明瞭PoCTL公式有與CTL*公式中“一緻性”相對應的公式.
수선,제출료가능적Kripke결구적정의,건립료가능적Kripke결구적가능성측도공간,병분석료가능적Kripke결구적일계렬성질,즉임일로경전이적가능성가유기초시상태적가능성분포여각전이적가능성취하학계이득도；의거가능적Kripke결구소정의적가능성측도구유기합이성등등.기차,급출료가능성계산수라집(PoCTL)적개념,토론료량개PoCTL상태공식이급PoCTL여경전계산수라집(CTL)공식적등개성.최후,증명료PoCTL공식유여CTL*공식중“일치성”상대응적공식.
