λ-互模擬的研究.pdf

1、進(jìn)程代數(shù)作為描述和分析并發(fā)與分布式系統(tǒng)的重要工具之一是并發(fā)理論的主流研究方向。互模擬是進(jìn)程代數(shù)中刻畫行為等價(jià)的核心概念，而模態(tài)邏輯特征是它的一個(gè)重要性質(zhì)。隨著進(jìn)程代數(shù)的發(fā)展，許多不同的互模擬概念相繼被提出。為了描述進(jìn)程間的近似等價(jià)，最近文獻(xiàn)中提出了λ -互模擬的概念，并將其性質(zhì)與度量ρ聯(lián)系在一起，給出了ρ為超度量時(shí) -互模擬的模態(tài)邏輯特征。但由于ρ不為超度量時(shí) -互模擬一般不為等價(jià)關(guān)系，所以無法得到一個(gè)具有HML經(jīng)典形式的邏輯特征。由于

2、在復(fù)合下 -互模擬不能保持同余性，文獻(xiàn)中引入了CCS ，并初步討論了 -互模擬在CCS 中一些有用的性質(zhì)。 本文將就λ -互模擬模態(tài)邏輯特征的開問題和CCS 做一些研究。研究?jī)?nèi)容主要包括以下幾個(gè)方面： （1）給出用于描述ρ不要求為超度量時(shí) -互模擬模態(tài)邏輯特征的新刻畫形式。 （2）引入一個(gè)新模態(tài)詞，并在此基礎(chǔ)上使用新的模態(tài)邏輯語言給出一個(gè)更具一般性的 -互模擬的模態(tài)邏輯特征。 （3）討論CCS 所描述的系