Forward analysis for WSTS. I: Completions. (English) Zbl 1236.68183

Finkel, Alain; Goubault-Larrecq, Jean

Albers, Susanne (ed.) et al., STACS 2009. 26th international symposium on theoretical aspects of computer science, Freiburg, Germany, February 26–28, 2009. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-09-5). LIPIcs – Leibniz International Proceedings in Informatics 3, 433-444, electronic only (2009).

Summary: 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.
For the entire collection see [Zbl 1213.68019].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

WSTS; forward analysis; completion; Karp-Miller procedure; domain theory; sober spaces; Noetherian spaces