  Model checking is the process of deciding whether a system satisfies a given
specification. Often, when the setting comprises multiple processes, the
specifications are over sets of input and output signals that correspond to
individual processes. Then, many of the properties one wishes to specify are
symmetric with respect to the processes identities. In this work, we consider
the problem of deciding whether the given system exhibits symmetry with respect
to the processes' identities. When the system is symmetric, this gives insight
into the behaviour of the system, as well as allows the designer to use only
representative specifications, instead of iterating over all possible process
identities.
  Specifically, we consider probabilistic systems, and we propose several
variants of symmetry. We start with precise symmetry, in which, given a
permutation $\pi$, the system maintains the exact distribution of permuted
outputs, given a permuted inputs. We proceed to study approximate versions of
symmetry, including symmetry induced by small $L_\infty$ norm, variants of
Parikh-image based symmetry, and qualitative symmetry. For each type of
symmetry, we consider the problem of deciding whether a given system exhibits
this type of symmetry.
