Model checking structured infinite Markov chains by