Abstract of Paper

An algorithm constructing the semilinear post* for 2-dim Reset/Transfer VASS
by A. Finkel, G. Sutre

Abstract:

The main result of this paper is a proof that the reachability set (post*)
of any 2-dim Reset/Transfer Vector Addition System with States is an
effectively computable semilinear set.  Our result implies that numerous
boundedness and reachability properties are decidable for this class.  Since
the traditional Karp and Miller's algorithm does not terminate when applied
to 2-dim Reset/Transfer VASS, we introduce, as a tool for the proof, a new
technique to construct a finite coverability tree for this class.