Vertor Addition Tree Automata

Philippe De Groote 1 Bruno Guillaume 1 Sylvain Salvati 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Communication dans un congrès
19th Annual IEEE Symposium on Logic in Computer Science - LICS'04, 2004, Turku, Finland, pp.64-73, 2004
Liste complète des métadonnées

https://hal.inria.fr/inria-00100081
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:58
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100081, version 1

Collections

Citation

Philippe De Groote, Bruno Guillaume, Sylvain Salvati. Vertor Addition Tree Automata. 19th Annual IEEE Symposium on Logic in Computer Science - LICS'04, 2004, Turku, Finland, pp.64-73, 2004. 〈inria-00100081〉

Partager

Métriques

Consultations de la notice

339