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: | Verification, Branching Vector Addition Systems, Presburger Arithmetic, Semilinear Sets |
Requirements: | Background in theoretical computer science, readiness to acquire basic knowledge on branching vector addition systems and semilinear sets |
Duration: | 4.5 months |
The first decision procedure to solve coverability for VASS was given in 1967 by Karp and Miller [1]. In fact, the algorithm of Karp and Miller does much more than just solve coverability. It computes a finite representation of the downward closure of the reachability set. This provides a tight over-approximation of the reachability set that is extremely useful to decide various problems on VASS. 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-Miller algorithm has been adapted to BVASS [2], to UDPN [3], and to several other VASS extensions.
One of the first subclasses of VASS for which reachability was shown decidable is the class of 2-dimensional VASS. For this class, Hopcroft and Pansiot devised an algorithm that computes a finite description (more precisely, a semilinear presentation) of the reachability set [4]. As an immediate consequence, they obtained that reachability is decidable for this class. In fact, the algorithm of Hopcroft and Pansiot can be viewed as a refinement of the Karp-Miller algorithm where the abstract pumping of cycles (putting ∞ in some components) is replaced by an exact acceleration of cycles (adding new vectors to the current set of periods). This idea has been pushed further for VASS extensions in small dimensions [5,6,7].
The idea of cycle acceleration was also used recently to solve coverability in 1-dimensional PVASS [8] and reachability in 1-dimensional BVASS [9,10]. But the decidability status of these two problems is still open in dimension 2. The objective of this internship is to investigate the question on 2-dimensional BVASS. Our conjecture is that this problem is decidable and that it can be solved using cycle acceleration.