基本进程代数的等价性验证

发布时间：2021-11-07 00:33

　　基本进程代数是进程重写系统中基础的顺序进程。相比有限状态系统,它引入了无限状态;相比于基本并行进程,它是顺序执行,控制能力较强;相比于下推自动机,它可以被理解为一种简单的单状态下推自动机。即使基本进程代数的定义和计算结构十分简洁,该模型也有着一定的表达能力和广泛的应用。从语法的角度看,该系统定义的语法对应的语言和下推自动机能接受的语言一致。从计算模型的角度看,该系统也能模拟很多比有限状态机复杂的顺序计算。因此对该模型的代数结构的探索对于基本计算模型的研究有重要的意义。另一方面,自动化验证的核心问题之一是无限状态系统的等价性验证问题,其他还包括了模型检测和定理机器证明。其中,等价性验证可以用以判定程序实现和给定的某设计规范的一致性。等价关系则根据不同的一致性要求来确定其严格程度。Park提出的互模拟,Milner提出的著名的观测等价关系就是这样一类等价关系。1987年,Baeten,Bergstra和Klop证明了一个著名的结论:强互模拟在基本进程代数上是可判定的。这个结论与之前的语言等价的不可判定性,激励了很多研究者往这个方向继续深入研究。van Glabbeek提出的分支互模拟在一定... 

【文章来源】：上海交通大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：121 页

【学位级别】：博士

【部分图文】：

PRS层次


本文编号：3480818