One way to perform model checking of a model mu-calculus formula on a linear process is to transform the problem into a parity game. The solution to this parity game also provides an answer to the original model checking question. However, for infinite systems, such as real-time systems, the parity game corresponding to most non-trivial properties is also of infinite size. To still reason about its solution, we developed a technique that can efficiently search for a witness or counter-example in infinite parity games. The search is based on information contained in a given parameterised Boolean equation system (PBES) that encodes our model checking problem.