  In this contribution we revisit regular model checking, a powerful framework
that has been successfully applied for the verification of infinite-state
systems, especially parameterized systems (concurrent systems with an arbitrary
number of processes). We provide a reformulation of regular model checking with
length-preserving transducers in terms of existential second-order theory over
automatic structures. We argue that this is a natural formulation that enables
us tap into powerful synthesis techniques that have been extensively studied in
the software verification community. More precisely, in this formulation the
first-order part represents the verification conditions for the desired
correctness property (for which we have complete solvers), whereas the
existentially quantified second-order variables represent the relations to be
synthesized. We show that many interesting correctness properties can be
formulated in this way, examples being safety, liveness, bisimilarity, and
games. More importantly, we show that this new formulation allows new
interesting benchmarks (and old regular model checking benchmarks that were
previously believed to be difficult), especially in the domain of parameterized
system verification, to be solved.
