山东大学学报（理学版）
山東大學學報（理學版）
산동대학학보（이학판）
Journal of Shandong University (Natural Science)
2015年
10期
32-39,46
,共9页
线性时序逻辑%DTMC%满足度%计量逻辑%逻辑度量空间
線性時序邏輯%DTMC%滿足度%計量邏輯%邏輯度量空間
선성시서라집%DTMC%만족도%계량라집%라집도량공간
linear temporal logic%DTMC%satisfaction degree%quantitative logic%logic metric space
考虑随机 Kripke 模型离散时间马尔可夫链 DTMC，并利用 DTMC 建立线性时序逻辑 LTL 中公式的满足度理论。首先在 DTMC 的全体无穷路径之集上引入某种适当的概率测度，考虑任一 DTMC D 中满足某个 LTL 公式φ的无穷初始路径占总路径的比例，以此为基础定义 D 关于公式φ的满足度概念；讨论满足度的若干性质，并指出这一概念体现了 DTMC 满足某个 LTL 公式的程度，故可将其作为模型检测理论中“D 满足φ”这一概念的计量化推广；引入 LTL 公式之间的相似度，并诱导全体 LTL 公式之集上的伪度量，从而构建 LTL 逻辑度量空间。
攷慮隨機 Kripke 模型離散時間馬爾可伕鏈 DTMC，併利用 DTMC 建立線性時序邏輯 LTL 中公式的滿足度理論。首先在 DTMC 的全體無窮路徑之集上引入某種適噹的概率測度，攷慮任一 DTMC D 中滿足某箇 LTL 公式φ的無窮初始路徑佔總路徑的比例，以此為基礎定義 D 關于公式φ的滿足度概唸；討論滿足度的若榦性質，併指齣這一概唸體現瞭 DTMC 滿足某箇 LTL 公式的程度，故可將其作為模型檢測理論中“D 滿足φ”這一概唸的計量化推廣；引入 LTL 公式之間的相似度，併誘導全體 LTL 公式之集上的偽度量，從而構建 LTL 邏輯度量空間。
고필수궤 Kripke 모형리산시간마이가부련 DTMC，병이용 DTMC 건립선성시서라집 LTL 중공식적만족도이론。수선재 DTMC 적전체무궁로경지집상인입모충괄당적개솔측도，고필임일 DTMC D 중만족모개 LTL 공식φ적무궁초시로경점총로경적비례，이차위기출정의 D 관우공식φ적만족도개념；토론만족도적약간성질，병지출저일개념체현료 DTMC 만족모개 LTL 공식적정도，고가장기작위모형검측이론중“D 만족φ”저일개념적계양화추엄；인입 LTL 공식지간적상사도，병유도전체 LTL 공식지집상적위도량，종이구건 LTL 라집도량공간。
The present paper aims to construct a quantitative approach for linear temporal logic by means of DTMC,a stochastic Kripke structure efficiently used in model checking.Based on a certain kind of probabilistic measure under the frame of DTMC,we compare the set of infinite initial paths satisfying some LTL formula φwith the set of all infinite initial paths,and consider their ratio to be the satisfaction degree of φwith respect to the DTMC D,as defined in this paper.It is pointed out that this satisfaction degree quantitatively extends the notion of D φ,the classical case in model checking.Furthermore,the concept of similarity degree between LTL formulas is presented,and a corresponding pseudo-metric on the set of all LTL formulas is induced,which enables the LTL logic metric space to be constructed.
