On the Separability Problem of VASS Reachability Languages
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913983551766528 |
|---|---|
| author | Keskin, Eren Meyer, Roland |
| author_facet | Keskin, Eren Meyer, Roland |
| contents | We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_ω$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the $\mathbb{Z}$-versions of the VASS, a regular separator for the $\mathbb{N}$-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_16095 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On the Separability Problem of VASS Reachability Languages Keskin, Eren Meyer, Roland Formal Languages and Automata Theory We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_ω$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the $\mathbb{Z}$-versions of the VASS, a regular separator for the $\mathbb{N}$-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition. |
| title | On the Separability Problem of VASS Reachability Languages |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2401.16095 |