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

TL;DR

This paper introduces a finite convergence theorem for fixpoint expressions in well-structured systems, enabling new decidability results for lossy channel systems in regular model checking.

Contribution

It provides a general finite convergence theorem for upward-guarded fixpoints in well-quasi-ordered sets, advancing the analysis of well-structured systems.

Findings

Proves a finite convergence theorem for upward-guarded fixpoints.

Applies theorem to establish new decidability results for lossy channel systems.

Enhances the understanding of fixpoint computations in well-structured model checking.

Abstract

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.