近年来，无限状态系统的验证成为了一个十分热门的研究领域。其中研究的重要问题不仅仅有对系统间等价的判定，还包括对系统和特定有限系统的等价性和系统的有限性判定。有限性问题所研究的是，给定一个系统，是否存在一个有限状态系统与之关于某个给定的等价关系相等。通常在研究系统间等价性判定的同时一起研究其对应的有限性问题是对我们大有裨益的。有限性问题在模型检测和程序分析的领域都扮演了非常重要的角色。在实际应用中，如果存在一个可行的方法，能检测一个正则系统与一个有限系统的等价性，那么我们就可以这个过程来检测一个系统与有限系统的等价性，假设我们可以检测系统的有限性，即正则性。该问题十分依赖于我们选择研究的等价关系。我们通常会使用互模拟等价的概念，它是一种语义上的观测等价。它和语言等价相比更有区分性，同时为我们提供了强大的计算可行性和一个优美的博弈论描述。对于强互模拟关系，我们通过研究得到了大量关于它的可判定性和计算复杂性结论。然而，类似于弱互模拟和分支互模拟关系的互模拟关系，在定义中考虑了系统内部的不可见动作。不可见动作的引入，既为等价关系提供了更精确的描述，也为它的判定带来了更大的难度。验证问题的研究，大多数都是在进程重写系统中的范围内进行的。这是一个包含了很多无限状态系统的一般的模型。比如基本进程代数(BPA)，基本并发进程(BPP)，下推自动机(PDA)，Petri网(PN)和进程代数(PA)。在本文中，我们对现阶段进程重写系统中的有限性问题的研究做了总结。我们罗列了现有的结论，并分析了一些一般性的技术。更进一步的，我们给出了一个关于Petri网关于分支互模拟的有限性的不可判定性的推论。本文的主要贡献是解决了完全正规化的进程代数的关于弱互模拟和分支互模拟的有限性问题。其中完全正规化是对于进程系统输入规则的一个限制。在文中，我们证明了完全正规化进程代数无限性的一个等价条件。我们给出了判定这个条件的算法。它的时间复杂度为O+，其中是转换规则的条数，是最长规则的长度。进程代数是一个一般的上下文无关模型，所以这个算法对完全正规化的基本进程代数和基本并发进程都是适用的。另外，本文中还讨论了正规化的基本并发进程关于分支互模拟的有限性，以及完全正规化的Petri网关于弱互模拟和分支互模拟的有限性问题。本文中讨论了一些有用的引理和证明思路。最后，本文还涉及了进程重写系统有限性问题的不可判定性和计算复杂性下界的证明。我们罗列了一些问题和猜想，作为未来的工作。总的来说，本文为一个具有挑战性的理论问题，进程重写系统关于考虑系统内部动作的互模拟等价关系的有限性问题，给出了一个创新的解决方案。对于未来的工作，在应用上，我们可以将多项式时间算法进行实现；在理论上，我们可以对更多这一系列问题中的可判定性和复杂性结论进行证明。