基本进程代数是进程重写系统中基础的顺序进程。相比有限状态系统,它引入了无限状态;相比于基本并行进程,它是顺序执行,控制能力较强;相比于下推自动机,它可以被理解为一种简单的单状态下推自动机。即使基本进程代数的定义和计算结构十分简洁,该模型也有着一定的表达能力和广泛的应用。从语法的角度看,该系统定义的语法对应的语言和下推自动机能接受的语言一致。从计算模型的角度看,该系统也能模拟很多比有限状态机复杂的顺序计算。因此对该模型的代数结构的探索对于基本计算模型的研究有重要的意义。另一方面,自动化验证的核心问题之一是无限状态系统的等价性验证问题,其他还包括了模型检测和定理机器证明。其中,等价性验证可以用以判定程序实现和给定的某设计规范的一致性。等价关系则根据不同的一致性要求来确定其严格程度。Park提出的互模拟,Milner提出的著名的观测等价关系就是这样一类等价关系。1987年,Baeten,Bergstra和Klop证明了一个著名的结论:强互模拟在基本进程代数上是可判定的。这个结论与之前的语言等价的不可判定性,激励了很多研究者往这个方向继续深入研究。van Glabbeek提出的分支互模拟在一定程度上约束了内部动作的行为,使得这种等价关系有了更直观的和合理的背景。而传统的观测等价由于其对内部动作并不做约束,使得判定过程中十分重要的有限分支性质不成立,从而导致很多算法的失效。本文聚焦在赋范基本进程代数和分支互模拟,对赋范基本进程代数的分支互模拟验证问题和正则性问题进行研究。赋范基本进程代数的分支互模拟验证问题是第一个被证明为可判定的在顺序无限状态系统下考虑内部动作的等价关系验证的问题。本文试图在对已有的工作认真理解和总结的基础上,对赋范基本进程代数的分支互模拟进行全面的性质分析和算法研究。本文的主要创新点如下:一、对赋范基本进程代数的分支互模拟得到了:1.验证问题是EXPTIME-完备问题的结论;2.正则性问题是指数时间可解的并且是PSPACE-难的结论。二、本文技术上:1.给予了范数在进程中的更加数学化的一般推广,详细考察了语义范数,并定义了下降互模拟;2.通过严格定义相对互模拟并挖掘其基本性质,得到了此问题所具备的特殊的代数性质,相对化版本的唯一分解性;3.以唯一分解性为基础,使用全局的贪心策略并应用了考虑扩张的下降互模拟技术来给出了正确的精细化算法,并得到关于生成分支互模拟的分解基,以此分别得到赋范基本进程代数的分支互模拟验证问题和正则性问题的指数时间算法。由分解基的指数因子,本文构造了对于算法最难的例子,并以此为基础可以归约和验证问题EXPTIME-难的下界以及正则性问题的PSPACE-难下界。4.本文的大部分技术难点在于对相对互模拟性质的挖掘,以及应用了考虑扩张的下降互模拟以保证算法的正确性。这些技术可应用于其他相关问题的高效算法研究。