We present Regular Model-checking, a framework for algorithmic verification 
of infinite state systems with, e.g., queues, stacks, integers, or a parametrized
linear topology. States are represented by strings over a finite alphabet and the
transition relation by a regular length-preserving relation on strings. Major 
problems in the verification of parametrized and infinite-state systems are to 
compute the set of states that are reachable from some set of initial states, 
and to compute the transitive closure of the transition relation. We present 
two complementary techniques for these problems. One is a direct automata-theoretic
construction, and the other is based on widening. Both techniques are incomplete
in general, but we give sufficient conditions under which they work.  We also 
present a method for verifying omega-regular properties of parametrized  systems, 
by computtaion of the transitive  closure of a transition relation.