廣反應(yīng)系統(tǒng)中的行為同余問(wèn)題研究.pdf

1、現(xiàn)在很多計(jì)算機(jī)系統(tǒng)是并發(fā)系統(tǒng)。并發(fā)系統(tǒng)固有的復(fù)雜性以及對(duì)并發(fā)性的本質(zhì)沒(méi)有全面正確的認(rèn)識(shí)使開發(fā)出的這類系統(tǒng)的可靠性與正確性無(wú)法得到保證。 為了解釋并發(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)的動(dòng)態(tài)變化。Brs是廣反應(yīng)系統(tǒng)(Widereactive syste

2、m,Wrs)的特例。為了在系統(tǒng)開發(fā)中能使用逐步精化方法及在分析系統(tǒng)行為時(shí)能使用合成方法，希望由反應(yīng)規(guī)則所導(dǎo)出的行為關(guān)系是同余的。R.Milner證明了有足夠的RPO的Wrs中雙相似是同余的，進(jìn)而證明了具體Brs中雙相似是同余的。 本文對(duì)三種常用的行為關(guān)系(跡預(yù)序、弱雙相似和失敗預(yù)序)在Wrs和其支持商中以及具體Brs中是否是同余的問(wèn)題進(jìn)行了研究。在J.J.Leifer和R.Milner提出的理論基礎(chǔ)上，證明了在有足夠相對(duì)推出(R

3、elative pushout，RPO)的Wrs及其支持商中跡預(yù)序是同余，弱雙相似和失敗預(yù)序在其反應(yīng)上下文子s范疇中是同余：進(jìn)而得出在任何Brs中跡預(yù)序是同余，弱雙相似和失敗預(yù)序在其反應(yīng)上下文子s范疇中是同余的結(jié)論。 得到這些結(jié)果的證明過(guò)程為：證明Wrs的支持商是反應(yīng)系統(tǒng)，從而得到函子反應(yīng)系統(tǒng)。在軌跡函子概念基礎(chǔ)上證明了Wrs有足夠的RPO等價(jià)于由它生成的函子反應(yīng)系統(tǒng)有足夠的RPO。由于Wrs的標(biāo)記變遷與函子反應(yīng)系統(tǒng)中的不同，本