Abstract
We present a technique based on the construction of finite automata to prove termination of string rewriting systems. Using this technique the tools Matchbox and TORPA are able to prove termination of particular string rewriting systems completely automatically for which termination was considered to be very hard until recently.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Book, R.V., Jantzen, M., Wrathall, C.: Monadic Thue systems. Theoret. Comput. Sci. 19, 231–251 (1982)
Book, R.V., Otto, F.: Cancellation rules and extended word problems. Inform. Process. Lett. 20, 5–11 (1985)
Book, R.V., Otto, F.: String-Rewriting Systems. In: Texts and Monographs in Computer Science. Springer, New York (1993)
Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 449–459. Springer, Heidelberg (2003)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. NIA Report 2003-09, National Institute of Aerospace, Hampton, VA, USA, Available at: http://research.nianet.org/~geser/papers/nia-matchbounded.html ; Accepted for Appl. Algebra Engrg. Comm. Comput.
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004), Tool and description available at: http://www-i2.informatik.rwth-aachen.de/AProVE/
Hibbard, T.N.: Context-limited grammars. J. ACM 21(3), 446–453 (1974)
Hofbauer, D., Waldmann, J.: Deleting string rewriting systems preserve regularity. In: Ésik, Z., Fülöp, Z. (eds.) DLT 2003. LNCS, vol. 2710. Springer, Heidelberg (2003); Accepted for Theoret. Comput. Sci.
Ravikumar, B.: Peg-solitaire, string rewriting systems and finite automata. In: Leong, H.-V., Jain, S., Imai, H. (eds.) ISAAC 1997. LNCS, vol. 1350, pp. 233–242. Springer, Heidelberg (1997)
Tahhan Bittar, E.: Complexité linéaire du probléme de Zantema. C. R. Acad. Sci. Paris Sér. I Inform. Théor., t. 323, 1201–1206 (1996)
Waldmann, J.: Matchbox: a tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004), Tool and description available at: http://theo1.informatik.uni-leipzig.de/matchbox/
Zantema, H., Geser, A.: A complete characterization of termination of 0p1q → 1r0s. Appl. Algebra Engrg. Comm. Comput. 11(1), 1–25 (2000)
Zantema, H.: Termination. In: Term Rewriting Systems, by Terese, pp. 181–259. Cambridge University Press, Cambridge (2003)
Zantema, H.: TORPA: Termination of Rewriting Proved Automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 95–104. Springer, Heidelberg (2004), Tool and description available at: http://www.win.tue.nl/~hzantema/torpa.html
Zantema, H.: Termination of string rewriting proved automatically. Accepted for J. Automat. Reason. (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geser, A., Hofbauer, D., Waldmann, J., Zantema, H. (2005). Finding Finite Automata That Certify Termination of String Rewriting. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds) Implementation and Application of Automata. CIAA 2004. Lecture Notes in Computer Science, vol 3317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30500-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-30500-2_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24318-2
Online ISBN: 978-3-540-30500-2
eBook Packages: Computer ScienceComputer Science (R0)