Controlled Term Rewriting

Florent Jacquemard 1 Yoshiharu Kojima 2 Masahiko Sakai 2
1 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Motivated by the problem of verification of imperative tree transformation programs, we study the combination, called controlled term rewriting systems (CntTRS), of term rewriting rules with con- straints selecting the possible rewrite positions. These constraints are specified, for each rewrite rule, by a selection automaton which defines a set of positions in a term based on tree automata computations. We show that reachability is PSPACE-complete for so-called monotonic CntTRS, such that the size of every left-hand-side of every rewrite rule is larger or equal to the size of the corresponding right-hand-side, and also for the class of context-free non-collapsing CntTRS, which transform Context-Free (CF) tree language into CF tree languages. When allowing size-reducing rules, reachability becomes undecidable, even for flat CntTRS (both sides of rewrite rules are of depth at most one) when restricting to words (i.e. function symbols have arity at most one), and for ground CntTRS (rewrite rules have no variables). We also consider a restricted version of the control such that a position is selected if the sequence of symbols on the path from that position to the root of the tree belongs to a given regular language. This restriction enables decision results in the above cases.
Type de document :
Communication dans un congrès
C. Tinelli and V. Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems (FroCoS 2011), Oct 2011, Saarbrücken, Germany. Springer, 6989, pp.179-194, 2011, Lecture Notes in Artificial Intelligence
Liste complète des métadonnées

https://hal.inria.fr/hal-00643160
Contributeur : Florent Jacquemard <>
Soumis le : lundi 21 novembre 2011 - 14:12:03
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : mercredi 22 février 2012 - 02:26:39

Fichiers

Identifiants

  • HAL Id : hal-00643160, version 1

Collections

Citation

Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai. Controlled Term Rewriting. C. Tinelli and V. Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems (FroCoS 2011), Oct 2011, Saarbrücken, Germany. Springer, 6989, pp.179-194, 2011, Lecture Notes in Artificial Intelligence. 〈hal-00643160〉

Partager

Métriques

Consultations de la notice

466

Téléchargements de fichiers

179