Forward analysis for WSTS, Part I: Completions

TL;DR

This paper introduces a theoretical framework for computing finite representations of successor sets in well-structured transition systems, addressing a previously unresolved problem using domain theory and topology insights.

Contribution

It develops a novel theoretical approach for manipulating downward-closed sets in WSTS, filling a gap in the existing framework.

Findings

Established a new domain-theoretic framework for downward-closed sets

Provided insights into the notion of adequate domains of limits

Advanced the understanding of successor computations in WSTS

Abstract

Well-structured transition systems provide the right foundation to compute a finite basis of the set of predecessors of the upward closure of a state. The dual problem, to compute a finite representation of the set of successors of the downward closure of a state, is harder: Until now, the theoretical framework for manipulating downward-closed sets was missing. We answer this problem, using insights from domain theory (dcpos and ideal completions), from topology (sobrifications), and shed new light on the notion of adequate domains of limits.