本文涉及的研究领域是无穷状态系统的验证。无穷状态系统上的验证问题主要包括两个方面:一个方面是等价验证,另一个方面是模型检测。等价验证主要是给定两个无穷状态系统,判定这两个系统是否等价。模型检测则是给定一个无穷状态系统和一个逻辑公式,判定这个系统是否满足这个公式。在实际应用中,我们可以通过等价验证来判定两个系统是否在某个意义下相等;我们也可以通过模型检测来判定一个系统是否满足某个给定的性质。对这个领域的研究使得我们能从一定程度上对安全协议,程序,工业设计等潜在的无穷状态系统进行验证。在等价验证中,通常选择互模拟作为等价关系。其基本思想为,如果一个状态与另一个状态互模拟,则任一个状态的迁移都要能被另一个状态模拟,模拟完以后的两个状态还要互模拟。目前最具代表性的互模拟是由Park提出的强互模拟和由Milner提出的弱互模拟。本文研究的是branching bisimulation的判定,它由van Glabbeek提出。Branching bisimulation通常作为弱互模拟的备选。相较弱互模拟,它保持了系统静态迁移中的中间状态,从而比弱互模拟更细;它还拥有弱互模拟没有的优点,如代数刻画和模态逻辑刻画。在本文中,我们研究BPA与有限状态系统,以及normed BPP与有限状态系统之间branching bisimulation的判定。其中BPA是一个基本的顺序计算模型,BPP是一个基本的并发计算模型,而normed BPP是BPP的一个子类。对于BPA,我们给出一个多项式算法,它改进了之前由Kucˇera et al给出的算法;而对于normedBPP,我们证明它与有限状态系统间的branching bisimilarity是多项式可判定的。模型检测的一个要键是用来描述系统行为的逻辑,其通常是时态逻辑。在这里,我们研究EGF逻辑。EGF逻辑由To et al形式地提出,它由EF逻辑和EGF算子组成。EGF算子与regular model checking有很大的联系。在regular model check-ing中,EGF算子被称为recurrence或recurrent reachability。同时,EGF算子也表示某种fairness的性质,表示“某种好的性质会不断发生”。在本文中,我们研究下推系统和BPP上EGF逻辑的模型检测问题。我们证明这两个模型检测问题都是PSPACE完全的,并在固定公式情形下给出一些结果。