In this paper we consider the problem of navigating emergency rescuers in buildings. The objective of the rescuer is to reach several critical regions in a building endangered by a spreading hazard and leave safely. We consider stochastic finite state models to capture the dynamics of the rescuer and the hazardous environment. We encode the objective of the rescuer as an automaton specification satisfaction problem. We synthesise a navigation policy for the rescuer that maximises the predicted probability of safely fulfilling the rescue mission. We finally test the proposed method in a simulation environment.