On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems
<|reference_start|>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.<|reference_end|>
@article{baier2006on,
    title={On computing fixpoints in well-structured regular model checking, with
  applications to lossy channel systems},
    author={C. Baier, N. Bertrand, Ph. Schnoebelen},
    journal={Proc. LPAR 2006, LNCS 4246, pp. 347-361, Springer 2006},
    year={2006},
    doi={10.1007/11916277_24},
    archivePrefix={arXiv},
    eprint={cs/0606091},
    primaryClass={cs.SC cs.GT}
}