Report
View in EDS

The Tractability Border of Reachability in Simple Vector Addition Systems with States

Bibliographic Details
Title: The Tractability Border of Reachability in Simple Vector Addition Systems with States
Authors: Chistikov, Dmitry, Czerwiński, Wojciech, Mazowiecki, Filip, Orlikowski, Łukasz, Sinclair-Banks, Henry, Węgrzycki, Karol
Publication Year: 2024
Collection: Computer Science
Subject Terms: Computer Science - Formal Languages and Automata Theory, Computer Science - Logic in Computer Science
More Details: Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting state and counter values to a given target state and counter values? When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. In this paper, we comprehensively characterise the tractability border of the problem when the input is encoded in unary. For our main result, we prove that reachability is NP-hard in unary encoded 3-VASS, even when structure is heavily restricted to be a simple linear path scheme. This improves upon a recent result of Czerwi\'nski and Orlikowski (2022), in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazi\'c, and Totzke (2016) and Leroux (2021). The underlying graph structure of a simple linear path scheme (SLPS) is just a path with self-loops at each node. We also study the exceedingly weak model of computation that is SPLS with counter updates in {-1,0,+1}. Here, we show that reachability is NP-hard when the dimension is bounded by O(\alpha(k)), where \alpha is the inverse Ackermann function and k bounds the size of the SLPS. We complement our result by presenting a polynomial-time algorithm that decides reachability in 2-SLPS when the initial and target configurations are specified in binary. To achieve this, we show that reachability in such instances is well-structured: all loops, except perhaps for a constant number, are taken either polynomially many times or almost maximally. This extends the main result of Englert, Lazi\'c, and Totzke (2016) who showed the problem is in NL when the initial and target configurations are specified in unary.
Comment: Full version of FOCS'24 paper. 60 pages, 16 figures
Document Type: Working Paper
DOI: 10.1109/FOCS61266.2024.00086
Access URL: http://arxiv.org/abs/2412.16612
Accession Number: edsarx.2412.16612
Database: arXiv
FullText Text:
  Availability: 0
CustomLinks:
  – Url: http://arxiv.org/abs/2412.16612
    Name: EDS - Arxiv
    Category: fullText
    Text: View this record from Arxiv
    MouseOverText: View this record from Arxiv
  – Url: https://resolver.ebsco.com/c/xy5jbn/result?sid=EBSCO:edsarx&genre=article&issn=&ISBN=&volume=&issue=&date=20241221&spage=&pages=&title=The Tractability Border of Reachability in Simple Vector Addition Systems with States&atitle=The%20Tractability%20Border%20of%20Reachability%20in%20Simple%20Vector%20Addition%20Systems%20with%20States&aulast=Chistikov%2C%20Dmitry&id=DOI:10.1109/FOCS61266.2024.00086
    Name: Full Text Finder (for New FTF UI) (s8985755)
    Category: fullText
    Text: Find It @ SCU Libraries
    MouseOverText: Find It @ SCU Libraries
Header DbId: edsarx
DbLabel: arXiv
An: edsarx.2412.16612
RelevancyScore: 1128
AccessLevel: 3
PubType: Report
PubTypeId: report
PreciseRelevancyScore: 1128.0458984375
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: The Tractability Border of Reachability in Simple Vector Addition Systems with States
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Chistikov%2C+Dmitry%22">Chistikov, Dmitry</searchLink><br /><searchLink fieldCode="AR" term="%22Czerwiński%2C+Wojciech%22">Czerwiński, Wojciech</searchLink><br /><searchLink fieldCode="AR" term="%22Mazowiecki%2C+Filip%22">Mazowiecki, Filip</searchLink><br /><searchLink fieldCode="AR" term="%22Orlikowski%2C+Łukasz%22">Orlikowski, Łukasz</searchLink><br /><searchLink fieldCode="AR" term="%22Sinclair-Banks%2C+Henry%22">Sinclair-Banks, Henry</searchLink><br /><searchLink fieldCode="AR" term="%22Węgrzycki%2C+Karol%22">Węgrzycki, Karol</searchLink>
– Name: DatePubCY
  Label: Publication Year
  Group: Date
  Data: 2024
– Name: Subset
  Label: Collection
  Group: HoldingsInfo
  Data: Computer Science
– Name: Subject
  Label: Subject Terms
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Computer+Science+-+Formal+Languages+and+Automata+Theory%22">Computer Science - Formal Languages and Automata Theory</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+Science+-+Logic+in+Computer+Science%22">Computer Science - Logic in Computer Science</searchLink>
– Name: Abstract
  Label: Description
  Group: Ab
  Data: Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting state and counter values to a given target state and counter values? When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. In this paper, we comprehensively characterise the tractability border of the problem when the input is encoded in unary. For our main result, we prove that reachability is NP-hard in unary encoded 3-VASS, even when structure is heavily restricted to be a simple linear path scheme. This improves upon a recent result of Czerwi\'nski and Orlikowski (2022), in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazi\'c, and Totzke (2016) and Leroux (2021). The underlying graph structure of a simple linear path scheme (SLPS) is just a path with self-loops at each node. We also study the exceedingly weak model of computation that is SPLS with counter updates in {-1,0,+1}. Here, we show that reachability is NP-hard when the dimension is bounded by O(\alpha(k)), where \alpha is the inverse Ackermann function and k bounds the size of the SLPS. We complement our result by presenting a polynomial-time algorithm that decides reachability in 2-SLPS when the initial and target configurations are specified in binary. To achieve this, we show that reachability in such instances is well-structured: all loops, except perhaps for a constant number, are taken either polynomially many times or almost maximally. This extends the main result of Englert, Lazi\'c, and Totzke (2016) who showed the problem is in NL when the initial and target configurations are specified in unary.<br />Comment: Full version of FOCS'24 paper. 60 pages, 16 figures
– Name: TypeDocument
  Label: Document Type
  Group: TypDoc
  Data: Working Paper
– Name: DOI
  Label: DOI
  Group: ID
  Data: 10.1109/FOCS61266.2024.00086
– Name: URL
  Label: Access URL
  Group: URL
  Data: <link linkTarget="URL" linkTerm="http://arxiv.org/abs/2412.16612" linkWindow="_blank">http://arxiv.org/abs/2412.16612</link>
– Name: AN
  Label: Accession Number
  Group: ID
  Data: edsarx.2412.16612
PLink https://login.libproxy.scu.edu/login?url=https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&scope=site&db=edsarx&AN=edsarx.2412.16612
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1109/FOCS61266.2024.00086
    Subjects:
      – SubjectFull: Computer Science - Formal Languages and Automata Theory
        Type: general
      – SubjectFull: Computer Science - Logic in Computer Science
        Type: general
    Titles:
      – TitleFull: The Tractability Border of Reachability in Simple Vector Addition Systems with States
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Chistikov, Dmitry
      – PersonEntity:
          Name:
            NameFull: Czerwiński, Wojciech
      – PersonEntity:
          Name:
            NameFull: Mazowiecki, Filip
      – PersonEntity:
          Name:
            NameFull: Orlikowski, Łukasz
      – PersonEntity:
          Name:
            NameFull: Sinclair-Banks, Henry
      – PersonEntity:
          Name:
            NameFull: Węgrzycki, Karol
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 21
              M: 12
              Type: published
              Y: 2024
ResultId 1