進(jìn)程演算是刻畫并發(fā)與交互式反應(yīng)系統(tǒng)行為的原型規(guī)范語言,它們通過進(jìn)程項(xiàng)來描述反應(yīng)式系統(tǒng)的規(guī)范及實(shí)現(xiàn),實(shí)現(xiàn)是否滿足規(guī)范則由行為等價或者精化關(guān)系來刻畫。經(jīng)典的模擬（simulation）關(guān)系主要是針對反應(yīng)式系統(tǒng)間的精化關(guān)系的刻畫,這類系統(tǒng)只具有被動的行為。對于具有主動行為的系統(tǒng),經(jīng)典的模擬關(guān)系將不再適用。為此,學(xué)術(shù)界將模擬和互模擬（bisimulation）概念推廣,提出共變-異變模擬（Covariant-Contravariant simulation,CC-模擬）的概念,它通過區(qū)分動作類型,刻畫了規(guī)范與實(shí)現(xiàn)對系統(tǒng)主動、被動和通訊動作在精化關(guān)系中的不同要求。由于行為關(guān)系相對演算系統(tǒng)中算子的（前）同余性（（pre）congruence）是對規(guī)范進(jìn)行模塊化構(gòu)造、分析及推理的根本基礎(chǔ),建立行為關(guān)系的（前）同余性是進(jìn)程演算研究的重要內(nèi)容之一。除此之外,行為關(guān)系的（不）等式公理的刻畫是進(jìn)程演算代數(shù)特性的集中體現(xiàn),它為進(jìn)程間的等價（或精化）關(guān)系的機(jī)器定理證明奠定了不可或缺的理論基礎(chǔ)。行為關(guān)系（前）同余性的證明以及公理刻畫均依賴于演算系統(tǒng)中算子的結(jié)構(gòu)化操作語義（structural operationa... 

【文章來源】：南京航空航天大學(xué)江蘇省 211工程院校

【文章頁數(shù)】：77 頁

【學(xué)位級別】：碩士

【部分圖文】：

SOS 規(guī)則形式間的包含關(guān)系

圖 2.1 證明樹示例圖設(shè) S ( Σ,R)是一正 TSS，S 是 S 的相關(guān)模型，對任意轉(zhuǎn)且僅當(dāng) |S 。理可自然的得出這樣一個事實(shí)：正 TSS S 的最小模型也是 S

文獻(xiàn)[53]將符號S 的含義拓展到表示一個可分層的 TSS S 的相間的關(guān)系給出了下圖 2.2 的說明，其中 A B表示 A 結(jié)構(gòu)類包含于 B 結(jié)個正 TSS S 的 A 和 B 是一致的。

【參考文獻(xiàn)】：
碩士論文
[1]可觀測共變—逆變模擬及其公理系統(tǒng)的研究[D]. 張威.南京航空航天大學(xué) 2014



本文編號：3364856