Forward analysis for WSTS, Part I: Completions
Logic in Computer Science
2009-02-11 v1
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.
Keywords
Cite
@article{arxiv.0902.1587,
title = {Forward analysis for WSTS, Part I: Completions},
author = {Alain Finkel and Jean Goubault-Larrecq},
journal= {arXiv preprint arXiv:0902.1587},
year = {2009}
}