The Reachability Problem for Ground TRS and Some Extensions

Abstract : The reachability problem for term rewriting systems (TRS) is the problem of deciding, for a given TRS S and two terms M and N, whether M can reduce to N by applying the rules of S. We show in this paper by some new methods based on algebraical tools of tree automata, the decidability of this problem for ground TRS's and, for every ground TRS S, we built a decision algorithm. In order to obtain it, we compile the system S and the compiled algorithm works in a real time (as a function of the size of M and N). We establish too some new results for ground TRS modulo different sets of equations : modulo commutativity of an operator sgr, the reachability problem is shown decidable with technics of finite tree automata; modulo associativity, the problem is undecidable; modulo commutativity and associativity, it is decidable with complexity of reachability problem for vector addition systems.
Type de document :
Communication dans un congrès
Proceedings of the International Joint Conference on Theory and Practice of Software Development, TAPSOFT, Vol.1, 1989, Barcelona, Spain. Springer Verlag, 351, pp.227-243, 1989, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00538873
Contributeur : Rémi Gilleron <>
Soumis le : mardi 23 novembre 2010 - 14:47:45
Dernière modification le : mardi 24 avril 2018 - 13:32:51

Identifiants

  • HAL Id : inria-00538873, version 1

Collections

Citation

Aline Deruyver, Rémi Gilleron. The Reachability Problem for Ground TRS and Some Extensions. Proceedings of the International Joint Conference on Theory and Practice of Software Development, TAPSOFT, Vol.1, 1989, Barcelona, Spain. Springer Verlag, 351, pp.227-243, 1989, Lecture Notes in Computer Science. 〈inria-00538873〉

Partager

Métriques

Consultations de la notice

155