Symmetry reduction is a well-known approach for alleviating the state
explosion problem in model checking. Automatically identifying
symmetries in concurrent systems, however, is computationally
expensive. We propose a symbolic framework for capturing symmetry
patterns in parameterised systems (i.e. an infinite family of
finite-state systems): two regular word transducers to represent,
respectively, parameterised systems and symmetry patterns. The
framework subsumes various types of ``symmetry relations'' ranging
from weaker notions (e.g. simulation preorders) to the strongest
notion (i.e. isomorphisms). Our framework enjoys two algorithmic
properties: (1) symmetry verification: given a transducer, we can
automatically check whether it is a symmetry pattern of a given
system, and (2) symmetry synthesis: we can automatically generate a
symmetry pattern for a given system in the form of a transducer.
Furthermore, our symbolic language allows additional constraints that
the symmetry patterns need to satisfy to be easily incorporated in the
verification/synthesis. We show how these properties can help identify
symmetry patterns in examples like dining philosopher protocols,
self-stabilising protocols, and prioritised resource-allocator
protocol. In some cases (e.g. Gries's coffee can problem), our
technique automatically synthesises a safety-preserving finite
approximant, which can then be verified for safety solely using a
finite-state model checker.