Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910952663810048 |
|---|---|
| author | Guttenberg, Roland Czerwiński, Wojciech Lasota, Sławomir |
| author_facet | Guttenberg, Roland Czerwiński, Wojciech Lasota, Sławomir |
| contents | Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_07660 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests Guttenberg, Roland Czerwiński, Wojciech Lasota, Sławomir Formal Languages and Automata Theory Logic in Computer Science F.1.1 Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS. |
| title | Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests |
| topic | Formal Languages and Automata Theory Logic in Computer Science F.1.1 |
| url | https://arxiv.org/abs/2502.07660 |