  Regular model checking is a well-established technique for the verification
of infinite-state systems whose configurations can be represented as finite
words over a suitable alphabet. It applies to systems whose set of initial
configurations is regular, and whose transition relation is captured by a
length-preserving transducer. To verify safety properties, regular model
checking iteratively computes automata recognizing increasingly larger regular
sets of reachable configurations, and checks if they contain unsafe
configurations. Since this procedure often does not terminate, acceleration,
abstraction, and widening techniques have been developed to compute a regular
superset of the set of reachable configurations.
  In this paper we develop a complementary approach. Instead of approaching the
set of reachable configurations from below, we start with the set of all
configurations and compute increasingly smaller regular supersets of it. We use
that the set of reachable configurations is equal to the intersection of all
inductive invariants of the system. Since the intersection is in general
non-regular, we introduce $b$-bounded invariants, defined as those
representable by CNF-formulas with at most $b$ clauses. We prove that, for
every $b \geq 0$, the intersection of all $b$-bounded inductive invariants is
regular, and show how to construct an automaton recognizing it. We study the
complexity of deciding if this automaton accepts some unsafe configuration. We
show that the problem is in \textsc{EXPSPACE} for every $b \geq 0$, and
\textsc{PSPACE}-complete for $b=1$. Finally, we study how large must $b$ be to
prove safety properties of a number of benchmarks.
