We present a general formulation of approximate model-checking, in which both under- and over-approximations are propagated to give two-sided approximations of the denotation set. Technically, our discussion is set within modal mu-calculus, and, hence, includes standard linear and branching temporal logics over transition systems like LTL, CTL and CTL*. The state-space discretization via an A/D-map and the induced Alexandroff topology are established as the constructive basis for a topological approximation scheme, for which we provide classical as well as intuitionistic topological semantics. Finally, we show that under natural coherence conditions any approximation can be refined to a topological one.