Forward Analysis for WSTS, Part II: Complete WSTS

TL;DR

This paper introduces a simple forward analysis method for infinity-complete WSTS that computes a finite description of reachability sets, extending the applicability of analysis techniques to a new class of systems.

Contribution

It presents a new forward analysis procedure for infinity-complete WSTS, characterizes when it terminates, and applies it to well-structured counter systems, expanding analysis capabilities.

Findings

Procedure terminates in more cases than generalized Karp-Miller.

Characterizes systems where the procedure terminates as clover-flattable.

Applies the method to well-structured counter systems.

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.