论文部分内容阅读
现在很多计算机系统是并发系统。并发系统固有的复杂性以及对并发性的本质没有全面正确的认识使开发出的这类系统的可靠性与正确性无法得到保证。为了解释并发性的本质并在此基础上提出开发并发系统的正确方法,R.Milner于2001年提出了双图反应系统(Bigraphical reactive system,Brs)理论。在该模型中,用双图表示系统状态,用反应规则表示系统的动态变化。Brs是广反应系统(Wide reactive system,Wrs)的特例。为了在系统开发中能使用逐步精化方法及在分析系统行为时能使用合成方法,希望由反应规则所导出的行为关系是同余的。R.Milner证明了有足够的RPO的Wrs中双相似是同余的,进而证明了具体Brs中双相似是同余的。本文对三种常用的行为关系(迹预序、弱双相似和失败预序)在Wrs和其支持商中以及具体Brs中是否是同余的问题进行了研究。在J.J.Leifer和R.Milner提出的理论基础上,证明了在有足够相对推出(Relative pushout,RPO)的Wrs及其支持商中迹预序是同余,弱双相似和失败预序在其反应上下文子s范畴中是同余;进而得出在任何Brs中迹预序是同余,弱双相似和失败预序在其反应上下文子s范畴中是同余的结论。得到这些结果的证明过程为:证明Wrs的支持商是反应系统,从而得到函子反应系统。在轨迹函子概念基础上证明了Wrs有足够的RPO等价于由它生成的函子反应系统有足够的RPO。由于Wrs的标记变迁与函子反应系统中的不同,本文在J.J.Leifer的同余性证明基础上,针对Wrs的标记变迁得到了Wrs的支持商中这些关系的同余性结果。在证明Wrs的支持商与Wrs中的这些关系的对应性基础上,得到Wrs中这些关系的同余性结果。再进一步得到了具体Brs中这些关系的同余性结果。