逻辑LTS框架下预备模拟判定算法的研究

发布时间：2021-04-04 00:00

　　进程代数与时序逻辑是并发理论中应用最为广泛的两类规范系统,其中进程代数支持组合式的规范,而时序逻辑便于描述与验证系统的抽象性质。近来,Gerald Luttgen等人将二者进行结合,提出了逻辑标记转换系统以及该系统下进程项之间的精化关系——LLTS预备模拟关系。逻辑标记转换系统将操作式与逻辑式的规范结合到了统一的框架中,在通常的标记转换系统的基础上引入了进程之间的合取,并以协调性谓词标记由合取所产生的不协调进程,因而在支持组合式推理的同时还具有较强的表达能力。本文在充分考虑LLTS预备模拟相对于协调性谓词以及发散敏感的特性基础上,给出了判定不同逻辑标记转换系统之间是否具有LLTS预备模拟关系的算法,主要工作包括如下方面:1.引入划分对及其稳定性的定义,证明稳定划分对与LLTS预备模拟关系之间的等价性。基于该等价性,将判定不同逻辑标记转换系统之间LLTS预备模拟关系的问题转化为求解“最粗划分”问题,给出求解最粗划分的算子?,并证明其正确性。2.从更加一般化的角度看待LLTS预备模拟关系,提出与LLTS预备模拟关系等价的泛化预备模拟的定义,并证明了这一等价性。进而基于此定义,提出相应的划分... 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：67 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
注释表
缩略词
第一章 绪论
    1.1 引言
    1.2 混成系统规范与逻辑标记转换系统
    1.3 进程间精化关系的判定
    1.4 本文的主要研究工作
第二章 基本概念与定义
    2.1 逻辑标记转换系统
    2.2 LLTS上的逻辑构造
    2.3 协调性谓词的直观
    2.4 LLTS下的预备模拟
第三章 LLTS下的稳定划分对
    3.1 划分对
    3.2 reduct与expand函数的性质
    3.3 划分对的稳定性
    3.4 本章小结
第四章 一般化最粗划分问题及其求解
    4.1 一般化最粗划分问题
    4.2 一般化最粗划分的求解
    4.3 例子
    4.4 本章小结
第五章 LLTS预备模拟的判定算法
    5.1 LLTS泛化预备模拟
    5.2 划分对的泛化稳定性
    5.3 ERS算法
    5.4 算法复杂度
    5.5 例子
    5.6 本章小结
第六章 总结与展望
    6.1 全文总结
    6.2 进一步的工作
参考文献
致谢
在学期间的研究成果及发表的学术论文



本文编号：3117332