Counter-Boundedness for One-Dimensional Pushdown VASS

Location: LaBRI (Computer Science Research Laboratory of Bordeaux), University of Bordeaux, France
Team: Formal Methods and Models / Modelling and Technologies for Verification
Contact: Jérôme Leroux and Grégoire Sutre
Keywords: Boundedness Problem, Context-Free Languages, Verification, Pushdown Vector Addition Systems, Presburger Arithmetic, Semilinear Sets
Requirements: Background in theoretical computer science, readiness to acquire basic knowledge on pushdown vector addition systems and semilinear sets
Duration: 5 months

Summary

The boundedness problem asks whether the reachability set of a given system starting from a given configuration is finite. The first decision procedure to solve boundedness for vector addition system with states (VASS for short) was given in 1967 by Karp and Miller [1]. In fact, the algorithm of Karp and Miller does much more than just solve boundedness. In short, their algorithm unwinds the system to analyze into a reachability tree, and, at each step, pumps the positive cycles that have been traversed thus far. This pumping is represented by putting a special symbol ∞, which intuitively denotes a very large number, in the components that are increased by the cycle. Termination of the algorithm is guaranteed by the fact that the component-wise extension of the usual order on natural numbers is a wqo. The Karp and Miller algorithm has been adapted to the boundedness problem for pushdown VASS in [2]. Here, by pushdown VASS, we mean a VASS equipped with a pushdown stack.

For pushdown VASS, several variants of the boundedness problem arise naturally since unboundedness may come from the stack or from the counters. Some of these variants are more difficult than others. For instance, boundedness of the stack can be decided with an extension of the algorithm à la Karp and Miller introduced in [2], but boundedness of the counters is still open. In dimension one, this last problem is shown to be solvable in exponential time in [3] using techniques similar to the ones introduced in [4] for solving the coverability problem. In this approach, the problem is decided by providing witnesses of unboundedness given as good prefixes of executions that contain patterns that can be iterated to increment the counter to arbitrary large values. This approach cannot be extended to the boundedness problem in a particular final control state since we have no guarantee that such a prefix witness can be extended to a full computation ending in the final control state.

The objective of this internship is to investigate counter-boundedness problems for pushdown VASS. Our conjecture is that two natural extensions of the one-dimensional problem solved in [3] are decidable : (1) the extension with final control states, and (2) the multi-dimensional case (without final control state). We will not try during this internship to combine those two extensions since the multi-dimensional case with final control states is at least as hard as the reachability problem, a long standing open problem for pushdown VASS [5].

References

  1. R. M. Karp and R. E. Miller. “Parallel Program Schemata”. In: Journal of Computer and System Sciences 3.2 (1969), pp. 147–195.
  2. J. Leroux, M. Praveen, and G. Sutre. “Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems“. In: LICS 2014. ACM, 2014, pp. 63:1-63:10.
  3. J. Leroux, G. Sutre, and P. Totzke. “On Boundedness Problems for Pushdown Vector Addition Systems”. In: RP 2015. Springer, 2015, pp. 101–113.
  4. J. Leroux, G. Sutre, and P. Totzke. “On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension”. In: ICALP 2015. Springer, 2015, pp. 324–336.
  5. R. Lazic. “The reachability problem for vector addition systems with a stack is not elementary”. In: CoRR abs/1310.1767 (2013), pp. 1-4.