On computing fixpoints in well-structured regular model checking, with   applications to lossy channel systems
  We prove a general finite convergence theorem for "upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems. 
C. Baier, N. Bertrand, Ph. Schnoebelen