【摘要】： 現(xiàn)在很多計算機系統(tǒng)是并發(fā)系統(tǒng)。并發(fā)系統(tǒng)固有的復(fù)雜性以及對并發(fā)性的本質(zhì)沒有全面正確的認識使開發(fā)出的這類系統(tǒng)的可靠性與正確性無法得到保證。 為了解釋并發(fā)性的本質(zhì)并在此基礎(chǔ)上提出開發(fā)并發(fā)系統(tǒng)的正確方法，R.Milner于2001年提出了雙圖反應(yīng)系統(tǒng)(Bigraphical reactive system，，Brs)理論。在該模型中，用雙圖表示系統(tǒng)狀態(tài)，用反應(yīng)規(guī)則表示系統(tǒng)的動態(tài)變化。Brs是廣反應(yīng)系統(tǒng)(Wide reactive system，Wrs)的特例。為了在系統(tǒng)開發(fā)中能使用逐步精化方法及在分析系統(tǒng)行為時能使用合成方法，希望由反應(yīng)規(guī)則所導(dǎo)出的行為關(guān)系是同余的。R.Milner證明了有足夠的RPO的Wrs中雙相似是同余的，進而證明了具體Brs中雙相似是同余的。 本文對三種常用的行為關(guān)系(跡預(yù)序、弱雙相似和失敗預(yù)序)在Wrs和其支持商中以及具體Brs中是否是同余的問題進行了研究。在J.J.Leifer和R.Milner提出的理論基礎(chǔ)上，證明了在有足夠相對推出(Relative pushout，RPO)的Wrs及其支持商中跡預(yù)序是同余，弱雙相似和失敗預(yù)序在其反應(yīng)上下文子s范疇中是同余；進而得出在任何Brs中跡預(yù)序是同余，弱雙相似和失敗預(yù)序在其反應(yīng)上下文子s范疇中是同余的結(jié)論。 得到這些結(jié)果的證明過程為：證明Wrs的支持商是反應(yīng)系統(tǒng)，從而得到函子反應(yīng)系統(tǒng)。在軌跡函子概念基礎(chǔ)上證明了Wrs有足夠的RPO等價于由它生成的函子反應(yīng)系統(tǒng)有足夠的RPO。由于Wrs的標記變遷與函子反應(yīng)系統(tǒng)中的不同，本文在J.J.Leifer的同余性證明基礎(chǔ)上，針對Wrs的標記變遷得到了Wrs的支持商中這些關(guān)系的同余性結(jié)果。在證明Wrs的支持商與Wrs中的這些關(guān)系的對應(yīng)性基礎(chǔ)上，得到Wrs中這些關(guān)系的同余性結(jié)果。再進一步得到了具體Brs中這些關(guān)系的同余性結(jié)果。
【圖文】：

2.1雙圖反應(yīng)系統(tǒng)模型中的雙圖示例為了對Brs模型有一個直觀認識，我們先來看一些雙圖示例。例1圖2.1用雙圖G來表示樓宇環(huán)境內(nèi)主體及計算機之間進行通信，比如說進行電話會議。雙圖是Br:中s范疇的箭。圖中用粗實線圖形表示節(jié)點困ode)，用細實線表示節(jié)點間的鏈接(Link)，最外邊的大方形表示區(qū)域(Region);A、B、C、R等大寫字母標明了節(jié)點的控制(Co咖l)，也就是節(jié)點的種類;y，z等小寫字母表示名字(Name)，名字包括內(nèi)部名和外部名。具體來說，這里B表示樓房;R表示房間;A表示主體，比如可以是配備設(shè)備的人;C表示計算機。圖中用鏈接來表示主體及計算機之間的通信;y和z是外部名

可“放人，其伯雙田的上下文雙圖F
【學(xué)位授予單位】：青島大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2007
【分類號】：TP302

【相似文獻】

相關(guān)期刊論文 前10條

1 陳韜略;李斌;胡昊;呂建;;一個移動進程演算的互模擬同余定義框架[J];計算機科學(xué);2004年01期

2 陳韜略,韓婷婷,顏鋒,呂建;多元χ演算運行時錯誤的不可判定性[J];武漢大學(xué)學(xué)報(理學(xué)版);2004年05期

3 胡國定;王永革;;面向?qū)ο蟛l(fā)程序設(shè)計的基礎(chǔ)理論[J];計算機科學(xué);1993年04期

4 劉海燕;陳火旺;;并發(fā)模型分析[J];計算機科學(xué);1995年03期

5 江華;譚新星;李祥;;基于π-演算的安全協(xié)議描述與驗證[J];韶關(guān)學(xué)院學(xué)報;2008年03期

6 王颶安,李未;Σ-演算的范疇模型[J];北京航空航天大學(xué)學(xué)報;1992年03期

7 陳洪龍;李仁發(fā);;基于Bigraph理論的動態(tài)演化軟件相關(guān)特性分析與驗證方法[J];小型微型計算機系統(tǒng);2010年12期

8 ;勇攀計算機科學(xué)理論新高峰——記“并發(fā)進程的代數(shù)理論及驗證工具”項目主要完成人林惠民研究員[J];中國科技獎勵;2000年02期

9 常志明;毛新軍;齊治昌;;Bigraph理論在自適應(yīng)軟件體系結(jié)構(gòu)上的應(yīng)用[J];計算機學(xué)報;2009年01期

10 吳剛;面向網(wǎng)絡(luò)計算的移動智能體研究與實現(xiàn)[J];計算機工程與科學(xué);2001年04期

相關(guān)博士學(xué)位論文 前5條

1 何超棟;CCS的基本問題研究[D];上海交通大學(xué);2011年

2 曹木亮;基于π-演算的Petri網(wǎng)和密碼協(xié)議的形式化分析[D];上海交通大學(xué);2007年

3 吳剛;面向網(wǎng)絡(luò)計算的移動智能體研究與實現(xiàn)[D];中國人民解放軍國防科學(xué)技術(shù)大學(xué);2000年

4 吳鵬;并發(fā)系統(tǒng)的模型檢測與測試[D];中國科學(xué)院研究生院（軟件研究所）;2005年

5 劉劍;傳值進程與移動進程的模型檢測方法[D];中國科學(xué)院研究生院（軟件研究所）;2005年

相關(guān)碩士學(xué)位論文 前3條

1 鞠文廣;廣反應(yīng)系統(tǒng)中的行為同余問題研究[D];青島大學(xué);2007年

2 萬金龍;基于π演算的并發(fā)分布式語言的設(shè)計與原型實現(xiàn)[D];吉林大學(xué);2007年

3 張嚴;一種高階進程代數(shù)的弱互模擬研究[D];南京航空航天大學(xué);2008年

本文編號：2619555