Michael Blondin ; Mikhail Raskin - The Complexity of Reachability in Affine Vector Addition Systems with States

lmcs:6872 - Logical Methods in Computer Science, July 20, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:3)2021
The Complexity of Reachability in Affine Vector Addition Systems with StatesArticle

Authors: Michael Blondin ORCID; Mikhail Raskin ORCID

    Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations with respect to arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS. We also consider the reachability problem parameterized by a fixed affine VASS, rather than a class, and we show that the complexity landscape is arbitrary in this setting.

    Volume: Volume 17, Issue 3
    Published on: July 20, 2021
    Accepted on: May 29, 2021
    Submitted on: October 30, 2020
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,Computer Science - Formal Languages and Automata Theory
      Source : OpenAIRE Graph
    • Funder: Natural Sciences and Engineering Research Council of Canada
    • Parametrized Verification and Synthesis; Funder: European Commission; Code: 787367

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1032 times.
    This article's PDF has been downloaded 294 times.