| author: | Kumar Neeraj Verma and Jean Goubault-Larrecq |
|---|---|
| title: | Karp-Miller Trees for a Branching Extension of VASS |
| keywords: | branching vector addition systems, Karp-Miller trees, coverability, multiplicative exponential linear logic, equational tree automata |
| abstract: | 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. |
| If your browser does not display the abstract correctly (because of the different mathematical symbols) you may look it up in the PostScript or PDF files. | |
| reference: | Kumar Neeraj Verma and Jean Goubault-Larrecq (2005), Karp-Miller Trees for a Branching Extension of VASS, Discrete Mathematics and Theoretical Computer Science 7, pp. 217-230 |
| bibtex: | For a corresponding BibTeX entry, please consider our BibTeX-file. |
| ps.gz-source: | dm070113.ps.gz (100 K) |
| ps-source: | dm070113.ps (280 K) |
| pdf-source: | dm070113.pdf (296 K) |
The first source gives you the `gzipped' PostScript, the second the plain PostScript and the third the format for the Adobe accrobat reader. Depending on the installation of your web browser, at least one of these should (after some amount of time) pop up a window for you that shows the full article. If this is not the case, you should contact your system administrator to install your browser correctly.
Due to limitations of your local software, the two formats may show up differently on your screen. If eg you use xpdf to visualize pdf, some of the graphics in the file may not come across. On the other hand, pdf has a capacity of giving links to sections, bibliography and external references that will not appear with PostScript.