中国科学E辑
中國科學E輯
중국과학E집
SCIENCE IN CHINA (SERIES E)
2004年
2期
139-150
,共12页
模态逻辑%谓词μ-演算%模型检测%移动进程%异步π-演算
模態邏輯%謂詞μ-縯算%模型檢測%移動進程%異步π-縯算
모태라집%위사μ-연산%모형검측%이동진정%이보π-연산
提出了一个用于描述异步π-演算中移动进程的时态和空间性质的模态逻辑.该逻辑具有基于谓词变量的递归构造.建立了这一逻辑的语义理论,并证明了语义的单调性,从而保证了不动点的存在.还设计了一个算法来自动地检测移动进程是否具有用该逻辑公式所描述的性质,并证明了该算法的正确性.
提齣瞭一箇用于描述異步π-縯算中移動進程的時態和空間性質的模態邏輯.該邏輯具有基于謂詞變量的遞歸構造.建立瞭這一邏輯的語義理論,併證明瞭語義的單調性,從而保證瞭不動點的存在.還設計瞭一箇算法來自動地檢測移動進程是否具有用該邏輯公式所描述的性質,併證明瞭該算法的正確性.
제출료일개용우묘술이보π-연산중이동진정적시태화공간성질적모태라집.해라집구유기우위사변량적체귀구조.건립료저일라집적어의이론,병증명료어의적단조성,종이보증료불동점적존재.환설계료일개산법래자동지검측이동진정시부구유용해라집공식소묘술적성질,병증명료해산법적정학성.
