Abstract
Verifying the safety property of a transition system given by a term rewriting system is an undecidable problem. In this paper, we give an abstraction for the problem which is automatically generated from a given TRS by using abstract interpretation. Then we show that there are some cases in which the problem can be decided. Also we show a new decidable subclass of term rewriting systems which effectively preserves recognizability.
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
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Comon, H.: Equational Formulas in Order-Sorted Algebras. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 674–688. Springer, Heidelberg (1990)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (1997), http://www.grappa.univ-lille3.fr/tata/
Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of 4th POPL, pp. 238–252. ACM Press, New York (1977)
Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 271–290. Springer, Heidelberg (2000)
Gyenizse, P., Vágvölgyi, S.: Linear Generalized Semi-Monadic Rewrite Systems Effectively Preserve Recognizability. Theoretical Computer Science 194(1–2), 87–122 (1998)
Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational Abstractions. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 2–16. Springer, Heidelberg (2003)
Monniaux, D.: Abstracting Cryptographic Protocols with Tree Automata. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 149–163. Springer, Heidelberg (1999)
Nielson, F., Nielson, H.R., Hankin, C.: Abstract Interpretation. In: Principles of Program Analysis, ch. 4, Springer, Heidelberg (1999)
Salomaa, K.: Decidability of Confluence and Termination of Monadic Term Rewriting Systems. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 275–286. Springer, Heidelberg (1991)
Takai, T., Kaji, Y., Seki, H.: Right-linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 246–260. Springer, Heidelberg (2000)
Takai, T., Kaji, Y., Seki, H.: Right-linear Finite-Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability. Scienticae Mathematicae Japonicae (to appear)
Takai, T., Seki, H., Fujinaka, Y., Kaji, Y.: Layered Transducing Term Rewriting System and Its Recognizability Preserving Property. IEICE Transactions on Information and Systems E86-D(2), 285–295 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Takai, T. (2004). A Verification Technique Using Term Rewriting Systems and Abstract Interpretation. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive