Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reachability in VASS Extended with Integer Counters

Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, Antoni Puch, Henry Sinclair-Banks

TL;DR

It is shown that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding, and it is proved that reachability in d-VASS+Z lies in the complexity class $\mathcal{F}_{d+2}$.

Abstract

We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative and the Z-counters do not have this restriction. We study the complexity of the reachability problem for VASS+Z when the number of N-counters is fixed. We show that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding. For $d \geq 2$, using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class $\mathcal{F}_{d+2}$. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the Z-counters with N-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of N-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+Z is PSPACE-hard; without Z-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+Z is TOWER-hard. Without Z-counters, reachability in 3-VASS has elementary complexity and TOWER-hardness is only known in dimension 8.

Reachability in VASS Extended with Integer Counters

TL;DR

It is shown that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding, and it is proved that reachability in d-VASS+Z lies in the complexity class .

Abstract

We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative and the Z-counters do not have this restriction. We study the complexity of the reachability problem for VASS+Z when the number of N-counters is fixed. We show that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding. For , using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class . Our upper bound improves on the naively obtained Ackermannian complexity by simulating the Z-counters with N-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of N-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+Z is PSPACE-hard; without Z-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+Z is TOWER-hard. Without Z-counters, reachability in 3-VASS has elementary complexity and TOWER-hardness is only known in dimension 8.
Paper Structure (7 sections, 15 theorems, 8 equations)

This paper contains 7 sections, 15 theorems, 8 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Reachability in 1VASS+$\mathbb{Z}$$1$-VASS+$\mathbb{Z}$
  4. Lower bounds for 2VASS+$\mathbb{Z}$$2$-VASS+$\mathbb{Z}$ and 3VASS+$\mathbb{Z}$$3$-VASS+$\mathbb{Z}$
  5. Reachability in unary 2VASS+$\mathbb{Z}$$2$-VASS+$\mathbb{Z}$ is PSpace-hard.
  6. Missing Proofs of \ref{['sec:dimension-one']}
  7. Missing Proofs of \ref{['sec:lower-bounds']}

Key Result

Theorem 1

Reachability in binary 1VASS+$\mathbb{Z}$$1$-VASS+$\mathbb{Z}$ is in NP.

Theorems & Definitions (19)

  • Theorem 1
  • Lemma 1
  • Corollary 1
  • Lemma 1
  • Corollary 2: c.f. EisenbrandS06
  • Corollary 3
  • Remark 4: Reachability in binary 1-VASS is in NP
  • Lemma 4
  • Theorem 5
  • Theorem 6
  • ...and 9 more