On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems

C. Baier, N. Bertrand, Ph. Schnoebelen

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…