Reachability in Two-Dimensional Branching 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: 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

Summary

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.

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. K. N. Verma and J. Goubault-Larrecq. “Karp-Miller Trees for a Branching Extension of VASS”. In: Discrete Mathematics and Theoretical Computer Science 7 (2005), pp. 217–230.
  3. P. Hofman, S. Lasota, R. Lazic, J. Leroux, S. Schmitz, and P. Totzke. “Coverability Trees for Petri Nets with Unordered Data”. In: FOSSACS 2016. Springer, 2016, pp. 445–461.
  4. J. Hopcroft and J.-J. Pansiot. “On the reachability problem for 5-dimensional vector addition systems”. In: Theoretical Computer Science 8.2 (1979), pp. 135–159.
  5. C. Dufourd, P. Jancar and P. Schnoebelen. “Boundedness of Reset P/T Nets”. In: ICALP 1999. Springer, 1999, pp. 301–310.
  6. A. Finkel and G. Sutre. “An Algorithm Constructing the Semilinear Post* for 2-Dim Reset/Transfer VASS”. In: MFCS 2000. Springer, 2000, pp. 353–362.
  7. A. Finkel, J. Leroux, and G. Sutre. “Reachability for Two-Counter Machines with One Test and One Reset”. In: FSTTCS 2018. Springer, 2018, pp. 31:1–31:14.
  8. J. Leroux, G. Sutre, and P. Totzke. “On Boundedness Problems for Pushdown Vector Addition Systems”. In: RP 2015. Springer, 2015, pp. 101–113.
  9. S. Göller, C. Haase, R. Lazic, and P. Totzke. “A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One”. In: ICALP 2016. LZI, 2016, 105:1–105:13.
  10. D. Figueira, R. Lazic, J. Leroux, F. Mazowiecki, and G. Sutre. “Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One”. In: ICALP 2017. LZI, 2017, 119:1–119:14.