基本介紹
- 中文名：互模擬等價
- 外文名：Bisimulation
- 領域：計算機科學、模態邏輯、集合論
- 套用：模態邏輯、並發系統
發展背景,定義,性質,套用,
發展背景
在上世紀80年代左右,人們在計算機科學、模態邏輯和集合論中大體上是同時並且獨立地發現互模擬。無論是在計算機科學中,還是在模態邏輯和集合論中,互模擬等價都是通過對代數結構之間態射概念進行提煉而產生。最基本的態射形式是同態,它給予了我們把一個結構(源結構)嵌入另一個結構(目標結構)的方式,使得源結構中的所有關係保持在目標結構中。然而,它的逆不一定成立;鑒於此,需要更強的態射概念。而常用的一個這樣的概念是同構,然而同構的概念又太強,因為同構的結構本質上和形式上都是相同的。於是，人們希望有一個介於同態和同構之間的概念，在這一探索過程中，互模擬等價被引入。
定義
模態邏輯中常常把互模擬定義在克里普克模型上。
定義 令 M = (W , R, V ) 和 M ′= (W ′, R′,V′)是兩個克里普克模型 ,令 Z∈W ×W ′是一個非空的二元關係 , 對於任意的 w ∈W , w′∈W ′, 如果wZw′,那么
( i)對所有命題字母 p, w∈V (p)若且唯若 w′∈V′(p) ;
( ii)對於所有的 v∈W ,如果 Rwv,那么存在 v′∈W ′使得 R′w′v′,並且 vZv′; (向前 )
( iii) 對於所有的 v′∈W ′,如果 R′w′v′,那么存在 v∈W 使得 Rwv,並且 vZv′。 (向後 )
則我們稱 Z是模型 M到模型 M ′上的一個互模擬。
性質
互模擬具有三個主要的性質，可以根據互模擬定價的定義進行推到得到：
（1）自返性
（2）對稱性
（3）傳遞性
套用
模態邏輯中的套用
互模擬等價被廣泛地運用於模態邏輯的研究中,比如用它去分析其他類型模態邏輯的表達力,如Janin和Walukiewicz證明了μ-演算對應於MSO的互模擬不變的一部分;用它去說明什麼樣的模型特徵在模態邏輯中是可以表達的;用它來定義在模型上保持模態公式有效性的運算;在模型檢測中互模擬用來收縮模型,同時還保持模型的語義。
計算機科學中的套用
在理論計算機科學中,互模擬等價關係被運用於標號遷移系統。標號遷移系統被用來描述進程:標號遷移系統中的結點被解釋為進程的可能狀態,標號遷移系統中的一元關係被解釋為狀態性質;標號遷移系統中的二元關係被解釋為進程可能執行的原子行為。互模擬等價及其變體可被看作標號遷移系統上的等價關係:兩個互模擬的標號遷移系統描述了相同的進程。
並發系統中的套用
互模擬等價因為各種目的被廣泛地用在並發系統中:·最大互模擬等價一般被看作是施加於系統上的最精緻的行為等價性。
- 互模擬等價證明方法被用來證明過程之間的等價性。
- 利用最大互模擬等價檢測算法的效力和最大互模擬合成性特徵使進程的狀態空間最小化。
- 最大互模擬等價和它的變體被用來對某些系統進行抽象化
