2026-07-25T19:05:24Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1844 2024-03-06T10:33:12Z ddc:004 open_access

Forward Analysis for WSTS, Part I: Completions Finkel, Alain Goubault-Larrecq, Jean WSTS Forward analysis Completion Karp-Miller procedure Domain theory Sober spaces Noetherian spaces 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alain Finkel and Jean Goubault-Larrecq 2009 Is Part Of LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2009.1844 urn:nbn:de:0030-drops-18444 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1844 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode