We consider the problem of verifying liveness for systems with a
finite, but unbounded, number of processes, commonly known as
parameterised systems. Typical examples of such systems include
distributed protocols (e.g.  for the dining philosopher problem).
Unlike the case of verifying safety, proving liveness is still
considered extremely challenging, especially in the presence of
randomness in the system.  In this paper we consider liveness under
arbitrary (including unfair) schedulers, which is often considered a
desirable property in the literature of self-stabilising systems.  We
introduce an automatic method of proving liveness for randomised
parameterised systems under arbitrary schedulers.  Viewing liveness as
a two-player reachability game (between Scheduler and Process), our
method is a CEGAR approach that synthesises a progress relation for
Process that can be symbolically represented as a finite-state
automaton. The method is incremental and exploits both Angluin-style
L*-learning and SAT-solvers.  Our experiments show that our algorithm
is able to prove liveness automatically for well-known randomised
distributed protocols, including Lehmann-Rabin Randomised Dining
Philosopher Protocol and randomised self-stabilising protocols (such
as the Israeli-Jalfon Protocol).  To the best of our knowledge, this
is the first fully-automatic method that can prove liveness for
randomised protocols.