逻辑lts框架下预备模拟判定算法的研究-计算机科学与技术专业毕业论文.docx

承诺书本人声明所呈交的博/硕士学位论文是本人在导师指导下进行的研究工作及取得的研究成果。除了文中特别加以标注和致谢的地方外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含为获得南京航空航天大学或其他教育机构的学位或证书而使用过的材料。本人授权南京航空航天大学可以将学位论文的全部或部分内容编入有关数据库进行检索,可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。(保密的学位论文在解密后适用本承诺书)作者签名: 日 期: 摘 要进程代数与时序逻辑是并发理论中应用最为广泛的两类规范系统,其中进程代数支持组合式的规范,而时序逻辑便于描述与验证系统的抽象性质。近来,GeraldLuttgen等人将二者进行结合,提出了逻辑标记转换系统以及该系统下进程项之间的精化关系——LLTS预备模拟关系。逻辑标记转换系统将操作式与逻辑式的规范结合到了统一的框架中,在通常的标记转换系统的基础上引入了进程之间的合取,并以协调性谓词标记由合取所产生的不协调进程,因而在支持组合式推理的同时还具有较强的表达能力。本文在充分考虑LLTS预备模拟相对于协调性谓词以及发散敏感的特性基础上,给出了判定不同逻辑标记转换系统之间是否具有LLTS预备模拟关系的算法,主要工作包括如下方面:,证明稳定划分对与LLTS预备模拟关系之间的等价性。基于该等价性,将判定不同逻辑标记转换系统之间LLTS预备模拟关系的问题转化为求解“最粗划分”问题,给出求解最粗划分的算子r,并证明其正确性。,提出与LLTS预备模拟关系等价的泛化预备模拟的定义,并证明了这一等价性。进而基于此定义,提出相应的划分对泛化稳定性以及最粗泛化稳定精化的概念,并证明了泛化稳定划分对与泛化预备模拟之间存在对应性。“划分稳定性”与“关系稳定性”,并给出满足划分稳定性的等价条件,从而给出相对高效的划分对稳定性判别方法,并由此给出判定LLTS预备模拟的算法ERS,证明了该算法的正确性,并讨论了其时间及空间的复杂度。关键词:逻辑标记转换系统,预备模拟,划分对,稳定性,最粗划分,划分精化问题,,binedbothtoproposethenotionoflogiclabeledtransitionsystemandcorrespondingrefinementrelation——,,:Introducethenotionofstabilityofthepartitionpair,,wetranslatetheproblemfordecidingLLTSreadysimulationintosolvingthesocalled“coarsestpartition”problem,andgiveaoperatorrwhichcouldbeusedtosolveourproblem;