Kumar Neeraj Verma ; Jean Goubault-Larrecq - Karp-Miller Trees for a Branching Extension of VASS

dmtcs:350 - Discrete Mathematics & Theoretical Computer Science, January 1, 2005, Vol. 7 - https://doi.org/10.46298/dmtcs.350
Karp-Miller Trees for a Branching Extension of VASSArticle

Authors: Kumar Neeraj Verma 1; Jean Goubault-Larrecq ORCID2,3

  • 1 Institut für Informatik
  • 2 Laboratoire Spécification et Vérification [Cachan]
  • 3 Security of information systems

We study BVASS (Branching VASS) which extend VASS (Vector Addition Systems with States) by allowing addition transitions that merge two configurations. Runs in BVASS are tree-like structures instead of linear ones as for VASS. We show that the construction of Karp-Miller trees for VASS can be extended to BVASS. This entails that the coverability set for BVASS is computable. This allows us to obtain decidability results for certain classes of equational tree automata with an associative-commutative symbol. Recent independent work by de Groote et al. implies that decidability of reachability in BVASS is equivalent to decidability of provability in MELL (multiplicative exponential linear logic), which is still an open problem. Hence our results are also a step towards answering this question in the affirmative.

Volume: Vol. 7
Published on: January 1, 2005
Imported on: March 26, 2015
Keywords: equational tree automata,branching vector addition systems,Karp-Miller trees,coverability,multiplicative exponential linear logic,[INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM]

9 Documents citing this article

Consultation statistics

This page has been seen 300 times.
This article's PDF has been downloaded 302 times.