广反应系统中的行为同余问题研究

发布时间：2020-04-08 16:10

【摘要】： 现在很多计算机系统是并发系统。并发系统固有的复杂性以及对并发性的本质没有全面正确的认识使开发出的这类系统的可靠性与正确性无法得到保证。 为了解释并发性的本质并在此基础上提出开发并发系统的正确方法，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中这些关系的同余性结果。
【图文】：

2.1双图反应系统模型中的双图示例为了对Brs模型有一个直观认识，我们先来看一些双图示例。例1图2.1用双图G来表示楼宇环境内主体及计算机之间进行通信，比如说进行电话会议。双图是Br:中s范畴的箭。图中用粗实线图形表示节点困ode)，用细实线表示节点间的链接(Link)，最外边的大方形表示区域(Region);A、B、C、R等大写字母标明了节点的控制(Co咖l)，也就是节点的种类;y，z等小写字母表示名字(Name)，名字包括内部名和外部名。具体来说，这里B表示楼房;R表示房间;A表示主体，比如可以是配备设备的人;C表示计算机。图中用链接来表示主体及计算机之间的通信;y和z是外部名

可“放人，其伯双田的上下文双图F
【学位授予单位】：青岛大学
【学位级别】：硕士
【学位授予年份】：2007
【分类号】：TP302

【相似文献】

相关期刊论文 前10条

1 陈韬略;李斌;胡昊;吕建;;一个移动进程演算的互模拟同余定义框架[J];计算机科学;2004年01期

2 陈韬略,韩婷婷,颜锋,吕建;多元χ演算运行时错误的不可判定性[J];武汉大学学报(理学版);2004年05期

3 胡国定;王永革;;面向对象并发程序设计的基础理论[J];计算机科学;1993年04期

4 刘海燕;陈火旺;;并发模型分析[J];计算机科学;1995年03期

5 江华;谭新星;李祥;;基于π-演算的安全协议描述与验证[J];韶关学院学报;2008年03期

6 王飓安,李未;Σ-演算的范畴模型[J];北京航空航天大学学报;1992年03期

7 陈洪龙;李仁发;;基于Bigraph理论的动态演化软件相关特性分析与验证方法[J];小型微型计算机系统;2010年12期

8 ;勇攀计算机科学理论新高峰——记“并发进程的代数理论及验证工具”项目主要完成人林惠民研究员[J];中国科技奖励;2000年02期

9 常志明;毛新军;齐治昌;;Bigraph理论在自适应软件体系结构上的应用[J];计算机学报;2009年01期

10 吴刚;面向网络计算的移动智能体研究与实现[J];计算机工程与科学;2001年04期

相关博士学位论文 前5条

1 何超栋;CCS的基本问题研究[D];上海交通大学;2011年

2 曹木亮;基于π-演算的Petri网和密码协议的形式化分析[D];上海交通大学;2007年

3 吴刚;面向网络计算的移动智能体研究与实现[D];中国人民解放军国防科学技术大学;2000年

4 吴鹏;并发系统的模型检测与测试[D];中国科学院研究生院（软件研究所）;2005年

5 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

相关硕士学位论文 前3条

1 鞠文广;广反应系统中的行为同余问题研究[D];青岛大学;2007年

2 万金龙;基于π演算的并发分布式语言的设计与原型实现[D];吉林大学;2007年

3 张严;一种高阶进程代数的弱互模拟研究[D];南京航空航天大学;2008年

本文编号：2619555