Forward Analysis for WSTS, Part I: Completions

Finkel, Alain; Goubault-Larrecq, Jean

doi:10.4230/LIPIcs.STACS.2009.1844

Document

Forward Analysis for WSTS, Part I: Completions

Authors Alain Finkel, Jean Goubault-Larrecq

Part of: Volume: 26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Symposium on Theoretical Aspects of Computer Science (STACS)
License: Creative Commons Attribution-NoDerivs 3.0 Unported license
Publication Date: 2009-02-19

PDF

File

PDF

LIPIcs.STACS.2009.1844.pdf

Filesize: 158 kB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.STACS.2009.1844
URN: urn:nbn:de:0030-drops-18444

Subject Classification

Keywords

WSTS
Forward analysis
Completion
Karp-Miller procedure
Domain theory
Sober spaces
Noetherian spaces

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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

Author Details

Alain Finkel

Jean Goubault-Larrecq

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail