Deciding Polynomial Termination Complexity for VASS Programs
| Autoři | |
|---|---|
| Rok publikování | 2021 |
| Druh | Článek ve sborníku |
| Konference | 32nd International Conference on Concurrency Theory (CONCUR 2021) |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | Dagstuhl website |
| Doi | http://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.30 |
| Klíčová slova | VASS; termination complexity |
| Přiložené soubory | |
| Popis | We show that for every fixed degree k ? 3, the problem whether the termination/counter complexity of a given demonic VASS is O(n^k), ?(n^k), and ?(n^k) is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for k ? 2. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for k ? 2. Tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds. |
| Související projekty: |