Abstract. We interpret modal mu­calculus formulas in a non­standard way as expectations over labeled Markov chains. In this semantics fixed­points are computed in an iterative incremental/decremental fashion. This provides the foundation for a symbolic model checking algorithm for CTL over labeled Markov chains using Multi­Terminal Binary Decision Diagrams, where expectations of until­formulas are calculated via suitable fixed­point approximations. We compare this non­standard semantics of CTL to the standard one for the probabilis­ tic logic PCTL by specifying a translation phi -> phi^b of the positive existential fragment CTL+ of CTL into PCTL, where PCTL probability thresholds are supplied by the non­standard semantics. Finally, we show soundness of our non­standard semantics of CTL+ with respect to the one for PCTL in the following sense: if our semantics computes a positive evidence for phi at state s then s satisfies the translated PCTL formula phi^b.