# zbMATH — the first resource for mathematics

Complete symbolic reachability analysis using back-and-forth narrowing. (English) Zbl 1110.68058
Summary: We propose a method called back-and-forth narrowing for solving reachability goals of the form $$(\exists \overrightarrow{x}).t_1 \to^*t_1' \land \cdots \land t_n \to^*t_n'$$ in general term rewrite systems. The method is a complete semi-decision procedure in the sense that it is guaranteed to find a solution when one exists, but in general it may not terminate when there are no solutions. The completeness result is very general in that it makes no assumptions about the given term rewrite system. Specifically, the rewrite rules need not be linear, confluent, or terminating, and can even have extra-variables in the right-hand side. Such generality is often essential while modeling concurrent systems or axiomatizing inference systems as rewrite rules, and in such applications back-and-forth narrowing can be used as a sound and complete technique for symbolic reachability analysis or as a deductive procedure for proving existential formulae.

##### MSC:
 68Q42 Grammars and rewriting systems
##### Keywords:
narrowing; soundness; completeness; rewrite systems; reachability
NRL
Full Text:
##### References:
 [1] S. Antoy, Definitional trees, in: Proc. Third Internat. Conf. on Algebraic and Logic Programming ALP’92, Lecture Notes in Computer Science, Vol. 632, Springer, Berlin, 1992, pp. 143-157. [2] S. Antoy, R. Echahed, M. Hanus, Parallel evaluation strategies for functional logic languages, in: Proc. 14th Internat. Conf. on Logic Programming (ICLP’97), MIT Press, Cambridge, MA, 1997, pp. 138-152. [3] Antoy, S.; Echahed, R.; Hanus, M., A needed narrowing strategy, J. ACM, 47, 4, 776-822, (2000) · Zbl 1327.68141 [4] D. Basin, S. Modersheim, L. Vigano. Constraint differentiation: a new reduction technique for constraint-based analysis of security protocols, Technical Report TR-405, Swiss Federal Institute of Technology, Zurich, May 2003. [5] Bockmayr, A., Conditional narrowing modulo of set of equations, Appl. algebra eng. comm. comput., 4, 3, 147-168, (1993) · Zbl 0776.68068 [6] A. Bouajjani, T. Touili, Extrapolating tree transformations, in: Ed Brinksma, K. Larsen (Eds.), 14th Internat. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 2404, Springer, Berlin, 2002. · Zbl 1010.68085 [7] Burkart, O.; Caucal, D.; Moller, F.; Steffen, B., Verification over infinite states, (), 545-623 · Zbl 1035.68067 [8] Dolev, D.; Yao, A., On the security of public key protocols, IEEE trans. inform. theory, 29, 2, 198-208, (1983) · Zbl 0502.94005 [9] S. Escobar, Refining weakly outermost-needed rewriting and narrowing, in: D. Miller (Ed.), Proc. Fifth Internat. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming, PPDP’03, ACM Press, New York, 2003, pp. 113-123. [10] S. Escobar, Implementing natural rewriting and narrowing efficiently, in: Y. Kameyama, P.J. Stuckey (Eds.), Seventh Internat. Symp. on Functional and Logic Programming (FLOPS 2004), Lecture Notes in Computer Science, Vol. 2998, Springer, Berlin, 2004, pp. 147-162. · Zbl 1122.68371 [11] Escobar, S.; Meadows, C.; Meseguer, J., A rewriting-based inference system for the NRL protocol analyzer: grammar generation, () · Zbl 1153.94375 [12] S. Escobar, J. Meseguer, P. Thati, Natural narrowing for general term rewriting systems, in: J. Giesl (Ed.), 16th Internat. Conf. on Rewriting Techniques and Applications, Lecture notes in Computer Science, Vol. 3467, Springer, Berlin, 2005, pp. 279-293. · Zbl 1078.68655 [13] Finkel, A.; Schnoebelen, Ph., Well-structured transition systems everywhere!, Theoret. comput. sci., 256, 1, 63-92, (2001) · Zbl 0973.68170 [14] T. Genet, F. Klay, Rewriting for cryptographic protocol verification, in: D. McAllester (Ed.), Automated Deduction—CADE 17, Lecture Notes in Artificial Intelligence, Vol. 1831, Springer, Berlin, 2000, pp. 271-290. · Zbl 0963.94016 [15] J.M. Hullot, Canonical forms and unification, in: W. Bibel, R. Kowalski (Eds.), Fifth Conf. on Automated Deduction, Lecture Notes in Computer Science, Vol. 87, Springer, Berlin, 1980, pp. 318-334. · Zbl 0441.68108 [16] J.-P. Jouannaud, C. Kirchner, H. Kirchner, Incremental construction of unification algorithms in equational theories, in: 10th Internat. Colloq. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 154, Springer, Berlin, 1983, pp. 361-373. · Zbl 0516.68067 [17] Meadows, C., The NRL protocol analyzer: an overview, J. logic programming, 26, 2, 113-131, (1996) · Zbl 0871.68052 [18] J. Meseguer, C. Talcott. Semantic models for distributed object reflection, in: B. Magnusson (Ed.), Proc. of ECOOP’02, Málaga, Spain, June 2002, Lecture Notes in Computer Science, Vol. 2374, Springer, Berlin, 2002, pp. 1-36. · Zbl 1049.68815 [19] J. Meseguer, P. Thati, Symbolic reachability analysis using narrowing and it application to verification of cryptographic protocols, in: N. Martí-Oliet (Ed.), Internat. Workshop on Rewriting Logic and its Application, WRLA’04, Electronic Notes in Theoretical Computer Science, Vol. 117, Elsevier, Amsterdam, 2004. · Zbl 1115.68079 [20] A. Middeldorp, E. Hamoen, Counterexamples to completeness results for basic narrowing, in: H. Kirchner, G. Levi (Eds.), Third Internat. Conf. on Algebraic and Logic Programming, Lecture Notes in Computer Science, Vol. 632, Springer, Berlin, 1992, pp. 244-258. · Zbl 0810.68088 [21] S. Okui, A. Middeldorp, T. Ida, Lazy narrowing: strong completeness and eager variable elimination, in: P. Moses, M. Nielsen, M. Schwartzbach (Eds.), 20th Colloq. on Trees in Algebra and Programming, Lecture Notes in Computer Science, Vol. 915, Springer, Berlin, 1995, pp. 394-408. · Zbl 0874.68157 [22] Peterson, G.E.; Wegman, M.N., Linear unification, J. comput. systems sci., 16, 158-167, (1978) · Zbl 0371.68013 [23] Sekar, R.C.; Ramakrishnan, I.V., Programming in equational logic: beyond strong sequentiality, Inform. and comput., 104, 1, 78-109, (1993) · Zbl 0803.68060 [24] H. Seki, H. Ohsaki, T. Takai, ACTAS: a system design for associative and commutative tree automata theory, in: Fifth Internat. Workshop on Rule-Based Programming (RULE 2004), Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam, 2004. [25] P. Thati, J. Meseguer, Complete symbolic reachability analysis using back-and-forth narrowing, in: J.L. Fiadeiro, N. Harman, M. Roggenbach, J. Rutten (Eds.), Conf. on Algebra and Co-algebra in Computer Science, Lecture Notes in Computer Science, Vol. 3629, Springer, Berlin, 2005. · Zbl 1151.68452 [26] T. Takai, A verification technique using term rewriting systems and abstract interpretation, in: Halatsis, et al. (Eds.), Proc. RTA 2004, Lecture Notes in Computer Science, Vol. 3091, Springer, Berlin, 2004, pp. 119-133. · Zbl 1187.68319 [27] T.Takai, Y. Kaji, H. Seki, Right-linear finite path overlapping term rewriting systems effectively preserve recognizability, in: L. Bachmair (Ed.), Internat. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 1833, Springer, Berlin, 2000, pp. 246-260. · Zbl 0964.68073 [28] P. Wolper, B. Boigelot, Verifying systems with infinite but regular state spaces, in: Internat. Conf. on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 1998, pp. 88-97.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.