Reachability in One-Dimensional Pushdown Vector Addition Systems is Decidable
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912104875819008 |
|---|---|
| author | Bizière, Clotilde Czerwiński, Wojciech |
| author_facet | Bizière, Clotilde Czerwiński, Wojciech |
| contents | We consider the model of one-dimensional Pushdown Vector Addition Systems (1-PVAS), a fundamental computational model simulating both recursive and concurrent behaviours. Our main result is decidability of the reachability problem for 1-PVAS, an important open problem investigated for at least a decade. In the algorithm we actually consider an equivalent model of Grammar Vector Addition Systems (GVAS). We prove the main result by showing that for every one-dimensional GVAS (1-GVAS) one can compute another 1-GVAS, which has the same reachability relation as the original one and additionally has the so-called thin property. Due to the work of Atig and Ganty from 2011, thin 1-GVAS have decidable reachability problem, therefore our construction implies decidability of the problem for all 1-GVAS. Moreover, we also show that if reachability in thin 1-GVAS can be decided in elementary time then also reachability in all 1-GVAS can be decided in elementary time. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_02386 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Reachability in One-Dimensional Pushdown Vector Addition Systems is Decidable Bizière, Clotilde Czerwiński, Wojciech Formal Languages and Automata Theory We consider the model of one-dimensional Pushdown Vector Addition Systems (1-PVAS), a fundamental computational model simulating both recursive and concurrent behaviours. Our main result is decidability of the reachability problem for 1-PVAS, an important open problem investigated for at least a decade. In the algorithm we actually consider an equivalent model of Grammar Vector Addition Systems (GVAS). We prove the main result by showing that for every one-dimensional GVAS (1-GVAS) one can compute another 1-GVAS, which has the same reachability relation as the original one and additionally has the so-called thin property. Due to the work of Atig and Ganty from 2011, thin 1-GVAS have decidable reachability problem, therefore our construction implies decidability of the problem for all 1-GVAS. Moreover, we also show that if reachability in thin 1-GVAS can be decided in elementary time then also reachability in all 1-GVAS can be decided in elementary time. |
| title | Reachability in One-Dimensional Pushdown Vector Addition Systems is Decidable |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2411.02386 |