Forward analysis for WSTS, Part I: Completions

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.

Cited by in corpus (6)

• Demystifying Reachability in Vector Addition Systems
• Model Checking Vector Addition Systems with one zero-test
• Decision Problems for Petri Nets with Names
• Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
• Cost Automata, Safe Schemes, and Downward Closures
• Reachability Games on Extended Vector Addition Systems with States