面向逻辑标记转换系统的进程演算CLL_R的研究

发布时间：2017-10-14 02:18

  本文关键词：面向逻辑标记转换系统的进程演算CLL_R的研究

  更多相关文章： 形式化方法 并发系统 混合规范 逻辑标记转换系统 进程演算 计算树逻辑 公理化

【摘要】：为了形式化规范、验证和分析反应式并发系统,学术界提出并发展了多种形式化规范方法。这些方法大体上可分为两类：基于动作的和基于状态的。基于动作的规范方法以进程代数(演算)最具代表性；基于状态的方法通常以模态逻辑或μ-演算描述系统规范。这两类方法基于不同的观点,对形式规范和验证进行了深入而广泛的研究,具有互补的优点：前者支持规范的组合式(compositional)构造、分析和推理；后者擅长描述系统整体和抽象性质。十余年来,学术界期望构建一种允许上述两种不同风格规范并存且混合使用的架构,以此实现可以同时利用它们各自长处的目的。在此愿景驱使下,多种所谓混合规范方法被相继提出,其中,Luttgen和’Vogler近年提出的逻辑标记转换系统(简记为LLTS)克服了其它方法的缺陷,是一个允许自由混合使用通常进程算子和逻辑算子进行规范的语义框架。本文旨在基于纯演算的方法针对LITS在理论研究上的空白和缺陷开展工作,主要工作包括如下方面：(1)构建面向LLTS的进程演算系统CLLR该工作不但将Luttgen和’Vogle r的工作(不含隐藏算子)提升到纯演算的风格,更主要的贡献在于深入研究了他们没有涉及的递归算子。在深入研究环境(context)递归进程的展开与进程转换之间的内在联系基础上,我们较为系统地发展了CLLR的行为理论,证明了Luttgen和’Vogler提出的预备模拟关系相对CLLR所有算子的前同余性(preoongruence)从而在理论上保证了CLLR可以支持规范组合式的构造、分析和推理。作为面向LLTS的演算系统CLLR包含了逻辑合取和析取算子,并需要处理逻辑复合所带来的进程协调性问题。正因为进程协调性对进程行为的发散所具有的敏感性,使得CLLR中的递归算子处理较之通常进程演算要相对困难和复杂许多。(2)在充分考虑协调进程与非协调进程行为差异的基础上,提出了CLLR的公理系统AXCLL,并证明了该系统的可靠性以及相对无递归进程的基完备性,从而揭示了通常进程算子与逻辑合取及析取算子在预备模拟关系下所遵循的代数律。(3)研究了CLLR中形如X=RStx方程的解,证明了唯一解定理和最大解定理。前者给出了这类方程存在唯一解的充分条件；后者揭示了递归进程X X=tx与X=Rs tx的解之间的内在联系：若X是tx的强有卫变元,则X X=tx是满足等式X=RStx的最“粗糙”的规范。(4)作为递归算子与方程最大解定理的应用,我们研究了将基于动作的计算树逻辑ACTL表示安全性质的语言片段在CLLR中进行编码的问题。该研究在理论上保证了CLLR具有描述安全性质的表达能力,同时将判定进程是否满足(表示安全性的)ACTL公式的模型检测问题归约为判定进程之间是否具有精化关系的验证问题。由于递归算子的使用,该工作所提供的编码极大简化了Luttgen和、Voler的原有编码。总之,上述研究将LLTS框架上原有的工作演算化(未包括隐藏算子),在此基础上较深入研究了LUttgen和’Vogler原有工作中没有涉及的若干重要的理论问题,包括：递归算子及其行为理论、方程解以及公理化等,并且本文在ACTL公式编码方面的工作极大简化了他们原有处理方式。与通常进程演算系统比较CLLR的特点在于考虑了进程的逻辑复合以及逻辑复合所带来的协调性问题,允许自由地混合使用通常的进程操作算子、递归算子、逻辑合取和析取算子以及模态词unless和unless(weak until)进行规范描述,并且支持规范组合式构造、推理和分析。
【关键词】：形式化方法 并发系统 混合规范 逻辑标记转换系统 进程演算 计算树逻辑 公理化
【学位授予单位】：南京航空航天大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP301
【目录】：

• 摘要4-6
• ABSTRACT6-12
• 第一章 绪论12-20
• 1.1 反应式并发系统及其形式化规范12-14
• 1.2 混合规范14-15
• 1.3 逻辑标记转换系统15-17
• 1.4 本文的主要工作17-18
• 1.5 本文的内容安排18-20
• 第二章 预备知识20-26
• 2.1 记号约定20
• 2.2 逻辑标记转换系统与预备模拟关系20-23
• 2.3 转换系统规范理论23-26
• 第三章 CLL_R及其操作语义26-40
• 3.1 CLL_R的语法及结构化操作语义规则26-29
• 3.2 CLL_R的稳固模型与标记转换系统29-31
• 3.3 CLL_R转换模型的基本性质31-38
• 3.4 本章小结38-40
• 第四章 展开、环境与转换40-58
• 4.1 展开及其基本性质40-42
• 4.2 环境与单步转换42-50
• 4.3 τ转换序列和典范路径50-57
• 4.4 本章小结57-58
• 第五章 CLL_R的前同余性58-78
• 5.1 若干引理58-71
• 5.2 (?)RS的前同余性71-76
• 5.3 本章小结76-78
• 第六章 CLL_R的公理系统78-96
• 6.1 公理系统AX_(CLL)78-81
• 6.2 AX_(CLL)的可靠性81-86
• 6.3 范式定理与基完备性86-94
• 6.4 本章小结94-96
• 第七章 CLL_R中一类方程的解96-112
• 7.1 唯一解定理96-105
• 7.2 最大解定理105-110
• 7.3 本章小结110-112
• 第八章 CLL_R与基于动作的计算树逻辑112-126
• 8.1 基于动作的计算树逻辑的一个片段在CLL_R中的编码112-113
• 8.2 编码的正确性113-121
• 8.3 例子121-124
• 8.4 本章小结124-126
• 第九章 总结与展望126-128
• 参考文献128-138
• 致谢138-140
• 在学期间的研究成果及发表的学术论文140

【相似文献】

中国期刊全文数据库 前10条

1 段国旺;毕秋阁;张风光;张洪峰;;温度多路转换系统在延迟焦化加热炉改造中的应用[J];科技信息;2012年31期

2 左渝斌,冯生荣;一种光学转换系统的实际应用[J];红外技术;2001年01期

3 张帅;贾珈;杨大利;徐明星;蔡莲红;;方言转换系统中的音节切分算法研究[J];计算机技术与发展;2009年07期

4 董子刚;李严;张元亭;;一种新的模拟到信息转换系统[J];电子学报;2013年09期

5 钱玉趾 ,杨永玲;转换系统——一个美丽的梦[J];中文信息;1994年02期

6 伍剑;;自动语音转换系统[J];金色少年;2009年03期

7 朱泽彬,黄会群,何锫;转换系统的设计及其应用[J];长沙理工大学学报(自然科学版);2005年03期

8 沈达阳;孙茂松;;汉字简繁体智能化转换系统[J];中文信息;1996年06期

9 张孝存;字本位和语本位——谈键盘输入和“转换系统”[J];中文信息;1996年05期

10 何铭;严克勤;;自动化播出的又一新课题——节目串联单管理与转换系统[J];电视工程;2000年02期

中国重要会议论文全文数据库 前1条

1 张运森;刘保国;刘珂;;STEP与XML转换系统设计与实现[A];全国先进制造技术高层论坛暨第八届制造业自动化与信息化技术研讨会论文集[C];2009年

中国重要报纸全文数据库 前2条

1 教育部语信司;“简繁汉字智能转换系统”通过结项鉴定[N];语言文字周报;2014年

2 记者 万玉凤;《汉字简繁文本智能转换系统》发布[N];中国教育报;2014年

中国博士学位论文全文数据库 前3条

1 张严;面向逻辑标记转换系统的进程演算CLL_R的研究[D];南京航空航天大学;2015年

2 张晋津;转换系统行为近似等价性的研究[D];南京航空航天大学;2010年

3 蒋泽甫;风电转换系统可靠性评估及其薄弱环节辨识[D];重庆大学;2012年

中国硕士学位论文全文数据库 前8条

1 戴健文;面向真实感渲染的材质转换系统与优化[D];浙江大学;2016年

2 周莹;高质量语音转换系统中关键技术的研究[D];南京邮电大学;2012年

3 李淑卿;移动数据实时转换系统的设计与实现[D];北京邮电大学;2008年

4 张宇奇;基于FPGA的信息交联转换系统的设计与实现[D];西安电子科技大学;2014年

5 陈志锋;通信协议转换系统的实现[D];苏州大学;2005年

6 范忠锋;Ada83/95转换系统——后端设计与实现[D];西安电子科技大学;2002年

7 郑麒;Ada83/95转换系统前端的研究与实现[D];西安电子科技大学;2002年

8 童波;特定对象汉语语音转换系统的研究[D];华北电力大学（北京）;2010年

，

本文编号：1028426