[科普中國(guó)]-互模擬等價(jià)

互模擬等價(jià)就是兩個(gè)系統(tǒng)能夠相互模仿對(duì)方 ,從而從觀察者的角度講 ,在某種程度上 ,它們是行為等價(jià)的。因此 ,互模擬等價(jià)是描述行為等價(jià)的一個(gè)數(shù)學(xué)概念 ,它從某個(gè)側(cè)面反映客觀世界兩個(gè)系統(tǒng)行為之間的關(guān)系。互模擬等價(jià)可定義在各種結(jié)構(gòu)上1。

發(fā)展背景在上世紀(jì)80年代左右,人們?cè)谟?jì)算機(jī)科學(xué)、模態(tài)邏輯和集合論中大體上是同時(shí)并且獨(dú)立地發(fā)現(xiàn)互模擬。無(wú)論是在計(jì)算機(jī)科學(xué)中,還是在模態(tài)邏輯和集合論中,互模擬等價(jià)都是通過(guò)對(duì)代數(shù)結(jié)構(gòu)之間態(tài)射概念進(jìn)行提煉而產(chǎn)生。最基本的態(tài)射形式是同態(tài),它給予了我們把一個(gè)結(jié)構(gòu)(源結(jié)構(gòu))嵌入另一個(gè)結(jié)構(gòu)(目標(biāo)結(jié)構(gòu))的方式,使得源結(jié)構(gòu)中的所有關(guān)系保持在目標(biāo)結(jié)構(gòu)中。然而,它的逆不一定成立;鑒于此,需要更強(qiáng)的態(tài)射概念。而常用的一個(gè)這樣的概念是同構(gòu),然而同構(gòu)的概念又太強(qiáng),因?yàn)橥瑯?gòu)的結(jié)構(gòu)本質(zhì)上和形式上都是相同的。于是，人們希望有一個(gè)介于同態(tài)和同構(gòu)之間的概念，在這一探索過(guò)程中，互模擬等價(jià)被引入1。

互模擬等價(jià)定義模態(tài)邏輯中常常把互模擬定義在克里普克模型上。

定義 令 M = (W , R, V ) 和 M ′= (W ′, R′,V′)是兩個(gè)克里普克模型 ,令 Z∈W ×W ′是一個(gè)非空的二元關(guān)系 , 對(duì)于任意的 w ∈W , w′∈W ′, 如果wZw′,那么

( i)對(duì)所有命題字母 p, w∈V (p)當(dāng)且僅當(dāng) w′∈V′(p) ;

( ii)對(duì)于所有的 v∈W ,如果 Rwv,那么存在 v′∈W ′使得 R′w′v′,并且 vZv′; (向前 )

( iii) 對(duì)于所有的 v′∈W ′,如果 R′w′v′,那么存在 v∈W 使得 Rwv,并且 vZv′。 (向后 )

則我們稱 Z是模型 M到模型 M ′上的一個(gè)互模擬1。

互模擬等價(jià)性質(zhì)互模擬具有三個(gè)主要的性質(zhì)，可以根據(jù)互模擬定價(jià)的定義進(jìn)行推到得到：

（1）自返性

（2）對(duì)稱性

（3）傳遞性

互模擬等價(jià)應(yīng)用模態(tài)邏輯中的應(yīng)用互模擬等價(jià)被廣泛地運(yùn)用于模態(tài)邏輯的研究中,比如用它去分析其他類型模態(tài)邏輯的表達(dá)力,如Janin和Walukiewicz證明了μ-演算對(duì)應(yīng)于MSO的互模擬不變的一部分;用它去說(shuō)明什么樣的模型特征在模態(tài)邏輯中是可以表達(dá)的;用它來(lái)定義在模型上保持模態(tài)公式有效性的運(yùn)算;在模型檢測(cè)中互模擬用來(lái)收縮模型,同時(shí)還保持模型的語(yǔ)義。2

計(jì)算機(jī)科學(xué)中的應(yīng)用在理論計(jì)算機(jī)科學(xué)中,互模擬等價(jià)關(guān)系被運(yùn)用于標(biāo)號(hào)遷移系統(tǒng)3。標(biāo)號(hào)遷移系統(tǒng)被用來(lái)描述進(jìn)程:標(biāo)號(hào)遷移系統(tǒng)中的結(jié)點(diǎn)被解釋為進(jìn)程的可能狀態(tài),標(biāo)號(hào)遷移系統(tǒng)中的一元關(guān)系被解釋為狀態(tài)性質(zhì);標(biāo)號(hào)遷移系統(tǒng)中的二元關(guān)系被解釋為進(jìn)程可能執(zhí)行的原子行為。互模擬等價(jià)及其變體可被看作標(biāo)號(hào)遷移系統(tǒng)上的等價(jià)關(guān)系:兩個(gè)互模擬的標(biāo)號(hào)遷移系統(tǒng)描述了相同的進(jìn)程。4

并發(fā)系統(tǒng)中的應(yīng)用互模擬等價(jià)因?yàn)楦鞣N目的被廣泛地用在并發(fā)系統(tǒng)中:·最大互模擬等價(jià)一般被看作是施加于系統(tǒng)上的最精致的行為等價(jià)性。

互模擬等價(jià)證明方法被用來(lái)證明過(guò)程之間的等價(jià)性。

利用最大互模擬等價(jià)檢測(cè)算法的效力和最大互模擬合成性特征使進(jìn)程的狀態(tài)空間最小化。

最大互模擬等價(jià)和它的變體被用來(lái)對(duì)某些系統(tǒng)進(jìn)行抽象化5

本詞條內(nèi)容貢獻(xiàn)者為:

王沛 - 副教授、副研究員 - 中國(guó)科學(xué)院工程熱物理研究所