Flattability of Priority Vector Addition Systems
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909184638844928 |
|---|---|
| author | Guttenberg, Roland |
| author_facet | Guttenberg, Roland |
| contents | Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_09185 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Flattability of Priority Vector Addition Systems Guttenberg, Roland Formal Languages and Automata Theory F.1.1 Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties. |
| title | Flattability of Priority Vector Addition Systems |
| topic | Formal Languages and Automata Theory F.1.1 |
| url | https://arxiv.org/abs/2402.09185 |