Institute of Information Science, Academia Sinica

Model checking is a fully automatic technique for the verication of finite state concurrent systems, and has been regarded as one of the most successful formal methods. Inventing efficient algorithms lies in the heart of the research in this filed. In recent years game-based approaches have been introduced for model checking in various temporal logics, and given rise to interesting algorithms. In this talk I will first review the basic ideas of model checking, emphasizing the roles of fix-points in expressing temporal behaviours of concurrent systems. I will then focus on a particular temporal logic, the propositional μ-calculus, and show how the model checking problem for this logic can be transformed into an equivalent problem of solving parity games. I will go on to demonstrate that some interesting structures exist in parity games which can be exploited to design new model checking algorithms for the μ-calculus.