The Well Structured Problem for Presburger Counter Machines
Alain Finkel (LSV), Ekanshdeep Gupta
TL;DR
This paper investigates the decidability of the well structured problem in Presburger counter machines, showing undecidability in general but providing algorithms for specific subclasses like 1-Affine VASS.
Contribution
It establishes decidability results for the well structured problem in Presburger counter machines and introduces algorithms for 1-Affine VASS.
Findings
Undecidability for most Presburger counter machines
Decidability of the strong well structured problem for all Presburger counter machines
Algorithm to compute predecessors in 1-Affine VASS
Abstract
We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.