Logic in Computer Science (LICS 2004)

Paper: Vector Addition Tree Automata (at LICS 2004)

Authors: Philippe de Groote Bruno Guillaume Sylvain Salvati

Abstract

We introduce a new class of automata, which we call vector addition tree automata. These automata are a natural generalization of vector addition systems with states, which are themselves equivalent to Petri nets. Then, we prove that the decidability of provability in multiplicative exponential linear logic (which is an open problem)is equivalent to the decidability of the reachability relation for vector addition tree automata. This result generalizes the well-known connection existing between Petri nets and the !-Horn fragment of multiplicative exponential linear logic.

BibTeX

  @InProceedings{deGrooteGuillaumeSa-VectorAdditionTreeA,
    author = 	 {Philippe de Groote and Bruno Guillaume and Sylvain Salvati},
    title = 	 {Vector Addition Tree Automata},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {64--73},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }