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

1、現(xiàn)在很多計算機系統(tǒng)是并發(fā)系統(tǒng)。并發(fā)系統(tǒng)固有的復雜性以及對并發(fā)性的本質沒有全面正確的認識使開發(fā)出的這類系統(tǒng)的可靠性與正確性無法得到保證。 為了解釋并發(fā)性的本質并在此基礎上提出開發(fā)并發(fā)系統(tǒng)的正確方法，R.Milner于2001年提出了雙圖反應系統(tǒng)(Bigraphical reactive system，Brs)理論。在該模型中，用雙圖表示系統(tǒng)狀態(tài)，用反應規(guī)則表示系統(tǒng)的動態(tài)變化。Brs是廣反應系統(tǒng)(Widereactive syste

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

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