Deciding the Bisimilarity Relation between Datalog Goals

详细信息    查看全文

• 作者：Philippe Balbiani (1) balbiani@irit.fr
  Antoun Yaacoub (1) yaacoub@irit.fr
• 关键词：Logic programming &#8211 ; Datalog &#8211 ; Equivalence of goals &#8211 ; Bisimulation &#8211 ; Decision method &#8211 ; Computational complexity
• 刊名：Lecture Notes in Computer Science
• 出版年：2012
• 出版时间：2012
• 年：2012
• 卷：7519
• 期：1
• 页码：67-79
• 全文大小：223.2 KB
• 参考文献：1. Bol, R.N.: Loop Checking in Partial Deduction. J. Logic Programming 16, 25–46 (1993)
  2. Bol, R.N., Apt, K.R., Klop, J.W.: An Analysis of Loop Checking Mechanisms for Logic Programs. Theoretical Computer Science 86, 35–79 (1991)
  3. Devienne, P., Leb茅gue, P., Routier, J.-C.: Halting Problem of One Binary Horn Clause is Undecidable. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, pp. 48–57. Springer, Heidelberg (1993)
  4. Gabbrielli, M., Levi, G., Meo, M.C.: Observable Behaviors and Equivalences of Logic Programs 122, 1–29 (1992)
  5. Harland, J.: On Normal Forms and Equivalence for Logic Programs. In: Proceedings of the Joint International Conference and Symposium on Logic Programming, pp. 146–160 (1992)
  6. Hennessy, M., Milner, R.: On Observing Nondeterminism and Concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980)
  7. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21, 666–677 (1978)
  8. Lifschitz, V., Pearce, D., Valverde, A.: Strongly Equivalent Logic Programs. ACM Transactions on Computational Logic (2000)
  9. Lloyd, J.W.: Foundations in Logic Programming. Springer (1984)
  10. Maher, M.: Equivalences of Logic Programs. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 410–424. Springer, Heidelberg (1986)
  11. Milner, R.: Calculi for synchrony and asynchrony. Theoretical Computer Science 25, 267–310 (1983)
  12. Park, D.: Concurrency and Automata on Infinite Sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science, pp. 167–183. Springer, UK (1981)
  13. Sangiorgi, D.: On the origins of bisimulation and coinduction. In: ACM Trans. Program. Lang. Syst., pp. 1–41. ACM, USA (2009)
• 作者单位：1. Institut de Recherche en Informatique de Toulouse, CNRS 鈥?Universit茅 de Toulouse, 118 route de Narbonne, 31062 Toulouse Cedex 9, France
• ISSN：1611-3349

文摘

We introduce the concept of bisimulation between Datalog goals: two Datalog goals are bisimilar with respect to a given Datalog program when their SLD-trees, considered as relational structures, are bisimilar. We address the problem of deciding whether two given goals are bisimilar with respect to given programs. When the given programs are hierarchical or restricted, this problem is decidable in 2EXPTIME.