Finkel, Alain and Goubault-Larrecq, Jean - Forward Analysis for WSTS, Part II: Complete WSTS

lmcs:1217 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3
Forward Analysis for WSTS, Part II: Complete WSTS

Authors: Finkel, Alain and Goubault-Larrecq, Jean

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.

DOI : 10.2168/LMCS-8(3:28)2012
Volume: Volume 8, Issue 3
Published on: September 29, 2012
Submitted on: November 24, 2009
Keywords: Computer Science - Logic in Computer Science,D.2.4, F.3.1


Consultation statistics

This page has been seen 205 times.
This article's PDF has been downloaded 114 times.