LIPIcs.STACS.2009.1844.pdf
- Filesize: 158 kB
- 12 pages
Document
Forward Analysis for WSTS, Part I: Completions
Authors
-
Part of:
Volume:
26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution-NoDerivs 3.0 Unported license
- Publication Date: 2009-02-19
Cite AsGet BibTex
Alain Finkel and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 433-444, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
https://doi.org/10.4230/LIPIcs.STACS.2009.1844
https://doi.org/10.4230/LIPIcs.STACS.2009.1844
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
- WSTS
- Forward analysis
- Completion
- Karp-Miller procedure
- Domain theory
- Sober spaces
- Noetherian spaces
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads