Some Results On Games For Bisimulation And Modal μ-calculus

The thesis consists of two parts. In the first part we give a simpler characterization for the bisimulation for normed context-free processes through a notion of D-bisimulation, and based on D-bisimulation we give an algorithm for the bisimulation for normed context-free processes in the context of game theory. In the second part we give a game-theoretic characterization for modal mu-calculus's satisfiability problem. Based on the satisfiablity game, we explore the possibility of new algorithm for model checking on a special class of modal mu-calculus formulas.