论文部分内容阅读
分支互模拟等价关系是由van Glabbeek和Weijland提出的进程等价关系。分支互模拟对内部动作采用比较合理的抽象处理,对进程的分支性质作了精确的刻画,是所有合理的语义等价中最精确的一个,一直是并发理论研究的热点。在程序验证中,通过建立系统和系统性质的某种等价关系如互模拟来验证程序的正确性时,分支互模拟关系是一个常用的选择。 在并发系统中,发散性是一个非常重要的性质,它通常涉及的是一个进程有无穷多个内部动作,不能与外界环境交互。对于一个等价关系≡,如果P和Q具有关系P≡Q,P是发散的当且仅当Q也是发散的,则称关系≡是发散性保持的。发散性涉及到程序的终止性和进程的前进属性,因此等价关系发散性保持的研究在并发理论领域和程序验证领域都有非常重要的意义。 首先,本文提出了发散性保持的分支互模拟:归纳分支互模拟前序关系和归纳分支互模拟等价关系。使用归纳定义的方式对分支互模拟关系的内部动作添加一定约束条件,结合分支互模拟概念定义了归纳分支互模拟关系。添加对归纳分支互模拟关系对称性的要求得到归纳分支互模等价关系,并证明了归纳分支互模拟等价关系是一个等价关系,且是发散性保持的,且是一个分支互模拟关系,同时也是具备这些性质中最弱的那个。 其次,我们给出一个关于归纳分支互模拟等价关系的划分算法。在分支互模拟关系划分算法的基础上,结合归纳分支互模拟关系发散性保持的特性,提出了归纳分支互模拟等价关系的划分算法,并证明了算法的正确性。