Forward Analysis for WSTS, Part II: Complete WSTS
Abstract
We describe a simple, conceptual forward analysis procedure for infinity-complete WSTS S. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set. We show that such completions are infinity-complete exactly when X is an omega-2-WSTS, a new robust class of WSTS. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets and on lossy channel systems. We characterize the WSTS where our procedure terminates as those that are clover-flattable. Finally, we apply this to well-structured counter systems.
Cite
@article{arxiv.1208.4549,
title = {Forward Analysis for WSTS, Part II: Complete WSTS},
author = {Alain Finkel and Jean Goubault-Larrecq},
journal= {arXiv preprint arXiv:1208.4549},
year = {2015}
}
Comments
35 pages, 6 figures. An extended abstract already appeared in Proc. 36th Intl. Coll. Automata, Languages and Programming (ICALP'09)