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 constraints 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.
This work has been supported by the ERC research project FoX under grant agreement FP7-ICT-233599 and by the INRIA ARC project ACCESS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abdulla, P.A., Jonsson, B., Mahata, P., d’Orso, J.: Regular tree model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 555–568. Springer, Heidelberg (2002)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)
Borovansky, P., Kirchner, H., Kirchner, C., Ringeissen, C.: Rewriting with strategies in elan: a functional semantics. International Journal of Foundations of Computer Science (IJFCS) 12(1), 69–95 (2001)
Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 52–70. Springer, Heidelberg (2006)
Chabin, J., Réty, P.: Visibly pushdown languages and term rewriting. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 252–266. Springer, Heidelberg (2007)
Chamberlin, D., Robie, J.: Xquery update facility 1.0. W3C Candidate Recommendation (2009), http://www.w3.org/TR/xquery-update-10/
Comon, H.: Sequentiality, second order monadic logic and tree automata. In: Proc. 10th IEEE Symposium on Logic in Computer Science (LICS), pp. 508–517. IEEE Computer Society, Los Alamitos (1995)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Löding, C., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2007), http://tata.gforge.inria.fr
Dassow, J., Paun, G., Salomaa, A.: Grammars with Controlled Derivations. In: Handbook of Formal Languages, vol. 2, pp. 101–154. Springer, Heidelberg (1997)
Durand, I., Middeldorp, A.: Decidable call-by-need computations in term rewriting. Information and Computation 196(2), 95–126 (2005)
Engelfriet, J.: Top-down tree transducers with regular look-ahead. Mathematical Systems Theory 10, 289–303 (1977)
Feuillade, G., Genet, T., Tong, V.V.T.: Reachability analysis over term rewriting systems. J. Autom. Reasoning 33(3-4), 341–383 (2004)
Frick, M., Grohe, M., Koch, C.: Query evaluation on compressed trees. In: Proc. of the 18th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, Los Alamitos (2003)
Gottlob, G., Koch, C.: Monadic datalog and the expressive power of languages for web information extraction. Journal of the ACM 51(1), 74–113 (2004)
Guessarian, I.: Pushdown tree automata. Mathematical Systems Theory 16(1), 237–263 (1983)
Hofbauer, D., Waldmann, J.: Deleting string rewriting systems preserve regularity. Theor. Comput. Sci. 327(3), 301–317 (2004)
Jacquemard, F., Rusinowitch, M.: Rewrite-based verification of XML updates. In: Proc. 12th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 119–130. ACM, New York (2010)
Jones, N.D., Andersen, N.: Flow analysis of lazy higher-order functional programs. Theoretical Computer Science 375(1-3), 120–136 (2007)
Kojima, Y., Sakai, M.: Innermost reachability and context sensitive reachability properties are decidable for linear right-shallow term rewriting systems. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 187–201. Springer, Heidelberg (2008)
Kuroda, S.Y.: Classes of languages and linear-bounded automata. Information and Control 7, 207–223 (1964)
Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178, 294–343 (2002)
Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. J. of Comp. Syst. Sci. 66(1), 66–97 (2003)
Nagaya, T., Toyama, Y.: Decidability for left-linear growing term rewriting systems. Inf. Comput. 178(2), 499–514 (2002)
Neven, F., Schwentick, T.: Query automata over finite trees. Theoretical Computer Science 275(1-2), 633–674 (2002)
Penttonen, M.: One-sided and two-sided context in formal grammars. Information and Control 25, 371–392 (1974)
Réty, P., Vuotto, J.: Tree automata for rewrite strategies. J. Symb. Comput. 40, 749–794 (2005)
Salomaa, K.: Deterministic tree pushdown automata and monadic tree rewriting systems. J. Comput. Syst. Sci. 37(3), 367–394 (1988)
Sénizergues, G.: Formal languages and word-rewriting. In: Comon, H., Jouannaud, J.-P. (eds.) TCS School 1993. LNCS, vol. 909, pp. 75–94. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacquemard, F., Kojima, Y., Sakai, M. (2011). Controlled Term Rewriting. In: Tinelli, C., Sofronie-Stokkermans, V. (eds) Frontiers of Combining Systems. FroCoS 2011. Lecture Notes in Computer Science(), vol 6989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24364-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-24364-6_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24363-9
Online ISBN: 978-3-642-24364-6
eBook Packages: Computer ScienceComputer Science (R0)