A paradigm for automatic approximation/refinement in conservative CTL model checking is presented. The approximations are used to verify a given formula conservatively by computing upper and lower bounds to the set of satisfying states at each sub-formula. These approximations attempt to perform conservative verification with less number of BDD variables and BDD nodes than exact method uses.We present new forms of operational graphs to avoid limitations associated With previously used operational graphs. Two new techniques for efficient automatic refinement of approximate system are presented. These methods make it easier to find the locality of the property being verified. We also present a new type of don't cares (Approximate Satisfying Don't Cares) that can make model checking more efficient in time and space. On average, an order of magnitude speedup was achieved.