Abstract. Probabilistic model checking is a method for automatically verifying that a probabilistic system satisfies a property with a given likelihood, with the probabilistic temporal logic PCTL being a common choice for the property specification language. In this paper, we explore methods for model checking PCTL properties of infinite-state systems in which probabilistic and nondeterministic behaviour coexist. Building on previous work on computing the maximum probability with which a state set is reached in such systems, we utilize symbolic operations on the state sets to generate a finite-state version of the system on which the PCTL model checking problem can be answered. As in the non-probabilistic case, our model checking algorithm is semi-decidable for infinite-state systems. We illustrate our technique using the formalism of probabilistic timed automata, for which previous PCTL model checking techniques were based on an unnecessarily fine subdivisions of the state space.