Probabilistic bisimulation is a fundamental notion of process
equivalence for probabilistic systems. It has important applications,
including the formalisation of the anonymity property of several
communication protocols.  While there is a large body of work on
verifying probabilistic bisimulation for finite systems, the problem
is in general undecidable for parameterized systems, i.e., for
infinite families of finite systems with an arbitrary number $n$ of
processes.  In this paper we provide a general framework for reasoning
about probabilistic bisimulation for parameterized systems. Our
approach is in the spirit of software verification, wherein we encode
proof rules for probabilistic bisimulation and use a decidable
first-order theory to specify systems and candidate bisimulation
relations, which can then be checked automatically against the proof
rules.

We work in the framework of regular model checking, and specify an
infinite-state system as a regular relation described by a first-order
formula over a universal automatic structure, i.e., a logical theory
over the string domain.  For probabilistic systems, we show how
probability values (as well as the required operations) can be encoded
naturally in the logic.  Our main result is that one can specify the
verification condition of whether a given regular binary relation is a
probabilistic bisimulation as a regular relation.  Since the
first-order theory of the universal automatic structure is decidable,
we obtain an effective method for verifying probabilistic bisimulation
for infinite-state systems, given a regular relation as a candidate
proof.  As a case study, we show that our framework is sufficiently
expressive for proving the anonymity property of the parameterized
dining cryptographers protocol and the parameterized grades protocol.
Both of these protocols hitherto could not be verified by existing
automatic methods.  Moreover, with the help of standard automata
learning algorithms, we show that the candidate relations can be
synthesized fully automatically, making the verification fully
automated.