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

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.

16 pages

References in corpus (1)

• Verifying nondeterministic probabilistic channel systems against $\omega$-regular linear-time properties

Cited by in corpus (1)

• Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor