2:00 -2:30pm,LH 802
Well Structured Problem for Presburger Counter Machines
Ekanshdeep Gupta
Chennai Mathematical Institute.
19-11-19

---

Abstract

Well Structured Transition Systems (WSTS) are a well-known framework to solve termination, boundedness, control-state reachability, and coverability problems. It is well known that Petri nets and Vector Addition Systems with States (VASS) are WSTS and that Minsky machines are not. But the characterization of which counter machines obey well structuredness is unknown. In this talk, we introduce the Well Structured Problem as the question of whether or not a model is well structured. We show the undecidability of this problem for even very restricted classes of Presburger counter machines and also show that the Strong Well Structured Problem is decidable for all Presburger counter machines. While affine VASS of dimension one are not well structured in general, we give an algorithm that computes the set of predecessors of a configuration as a Presburger formula. This is used to show the decidablity of the Well Structured Problem for 1-Affine VASS.