  We introduce a framework for approximate analysis of Markov decision
processes (MDP) with bounded-, unbounded-, and infinite-horizon properties. The
main idea is to identify a "core" of an MDP, i.e., a subsystem where we
provably remain with high probability, and to avoid computation on the less
relevant rest of the state space. Although we identify the core using
simulations and statistical techniques, it allows for rigorous error bounds in
the analysis. Consequently, we obtain efficient analysis algorithms based on
partial exploration for various settings, including the challenging case of
strongly connected systems.
