形式化验证是计算机科学中的核心课题之一;等价验证是形式化验证中一个主流领域;互模拟等价验证作为等价验证的重要组成部分,起始于上世纪下半叶。互模拟等价验证研究关注的模型大都是无限状态系统,而多数无限状态系统都涵括在一个一般的框架——进程重写系统（Process Rewrite Systems,PRS）中。从上世纪80年代开始,有大量在进程重写系统上互模拟等价验证的工作,主要分成互模拟等价性、互模拟正则性和互模拟有限性三方面。现有的研究表明进程重写系统上的分支互模拟等价验证是比较困难,主要体现在两个方面:其一,大多数无限状态系统,如单计数器网以及之上模型的分支互模拟等价性是不可判定的;其二,在非常基本的无限状态系统——基本进程代数和基本并行代数上,分支模拟等价性的判定性至今仍然是公开的。分支互模拟等价性与分支互模拟正则性和有限性的区别是前者验证同一模型之间的分支互模拟等价,而后两者关注的是给定的一个无限状态系统和有限状态系统之间的等价性。从自动验证角度看,正则性和有限性是比等价性验证要求更强,在工业界中更具有应用价值,而且正则性和有限性的结果也有利于对等价性的结果作进一步的推进。本文的研究聚焦在进程重写系统上分支互模拟有限性和正则性验证问题上,关注的是这类问题的可判定性,算法及复杂性,主要贡献有以下几个方面:下推自动机上的强互模拟和分支互模拟正则性问题的判定性,首先我们改进了下推自动机上强互模拟正则性问题的证明技术,在一阶文法的框架下,从迁移序列见证转换为进程序列见证,提出一种更加简洁易懂的证明强互模拟正则性的方法;其次,进一步将这个判定算法推广到分支互模拟正则性问题上,给出PDA-和PDA+两个受限下推自动机模型上正则性问题是可判定的结果。Petri网上的分支互模拟正则性和有限性问题的判定性,我们证明在Petri网模型上的分支互模拟正则性和有限性是不可判定的。首先是将Petri网上可达集包含这一不可判定问题通过分支互模拟的博弈刻画,规约到Petri网分支互模拟有限性问题上,给出其是不可判定的;其次是将另一个不可判定问题Minsky计数机器的停机问题规约到Petri网的正则性问题,证明后者也是不可判定的。单计数器网和单计数器自动机上分支互模拟有限性问题的下界,先对一个公式的真值表采用哥德尔编码技术,其次在多项式时间内构造从一个公式的满足性问题到一个单计数器网和一个有限状态系统的分支互模拟博弈游戏规约,证明在此模型上分支有限性是NP-难的,再在此基础上将一个DP-完备问题——SAT-UNSAT问题多项式时间内规约到单计数器网有限性问题,从而给提高它的下界到DP-难的。它的正则性问题以及单计数器自动机模型也有这一复杂性下界。本文主要研究进程重写系统上分支互模拟正则性和有限性问题,一是证明Petri网的分支互模拟正则性和有限性是不可判定的,在进程重写系统层次的右半部分划一个线,在其之上的模型这一类问题都是不可判定的;二是给出证明这一类问题复杂性上界的一种框架和方法,利用分支互模拟博弈刻画,将其他问题规约到此问题的博弈游戏中,从而给出其上界;还有提出一种更加简洁的证明正则性问题可判定性的方法。