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 |
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].