Verifiable agent interaction in abductive logic programming: The SCIFF framework

ABSTRACT

SCIFF is a framework thought to specify and verify interaction in open agent societies. The SCIFF language is equipped with a semantics based on abductive logic programming; SCIFF's operational component is a new abductive logic programming proof procedure, also named SCIFF, for reasoning with expectations in dynamic environments. In this article we present the declarative and operational semantics of the SCIFF language, and the termination, soundness, and completeness results of the SCIFF proof procedure, and we demonstrate SCIFF's possible application in the multiagent domain.

REFERENCES

• 1: Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM (JACM), v.52 n.1, p.102-146, January 2005 [doi>10.1145/1044731.1044735]
• 2: Alberti, M. and Chesani, F. 2005. The computational behaviour of the SCIFF abductive proof procedure and the SOCS-SI system. Intelligenza Artificiale II, 3 (Sept.), 45--51.
• 3: Alberti, M., Chesani, F., Gavanelli, M., and Lamma, E. 2005. The CHR-based implementation of a system for generation and confirmation of hypotheses, A. Wolf, T. Frühwirth, and M. Meister, Eds. Ulmer Informatik-Berichte, vol. 2005-01, Ulm University, Ulm, Germany, 111--122.
• 4: Marco Alberti , Marco Gavanelli , Evelina Lamma , Federico Chesani , Paola Mello , Marco Montali, An abductive framework for a-priori verification of web services, Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy [doi>10.1145/1140335.1140342]
• 5: Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., and Torroni, P. 2006b. Compliance verification of agent interaction: A logic-based tool. Appl. Artific. Intell. 20, 2-4 (Feb.-Apr.), 133--157.
• 6: Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., and Torroni, P. 2006c. Security protocols verification in abductive logic programming: A case study. In ESAW 2005 Post-proceedings, O. Dikenelli, M.-P. Gleizes, and A. Ricci, Eds. Lecture Notes in Artificial Intelligence, vol. 3963. Springer-Verlag, Berlin, Germany, 106--124.
• 7: Marco Alberti , Marco Gavanelli , Evelina Lamma , Paola Mello , Paolo Torroni , Giovanni Sartor, Mapping deontic operators to abductive expectations, Computational & Mathematical Organization Theory, v.12 n.2-3, p.205-225, October 2006 [doi>10.1007/s10588-006-9544-8]
• 8: Alberti, M., Gavanelli, M., Lamma, E., Mello, P., and Torroni, P. 2003. An abductive interpretation for open agent societies. In AI*IA 2003: Advances in Artificial Intelligence, Proceedings of the 8th Congress of the Italian Association for Artificial Intelligence, Pisa, A. Cappelli and F. Turini, Eds. Lecture Notes in Artificial Intelligence, vol. 2829. Springer-Verlag, Berlin, Germany, 287--299.
• 9: José Júlio Alferes , Luís Moniz Pereira , Terrance Swift, Abduction in well-founded semantics and generalized stable models via tabled dual programs, Theory and Practice of Logic Programming, v.4 n.4, p.383-428, July 2004 [doi>10.1017/S1471068403001960]
• 10: José Júlio Alferes , Antonio Brogi , João Alexandre Leite , Luís Moniz Pereira, Evolving Logic Programs, Proceedings of the European Conference on Logics in Artificial Intelligence, p.50-61, September 23-26, 2002
• 11: Anderson, A. 1958. A reduction of deontic logic to alethic modal logic. Mind 67, 100--103.
• 12: Apt, K. R. and Bezem, M. 1991. Acyclic programs. New Gen. Comput. 9, 3/4, 335--364.
• 13: Apt, K. R. and Bol, R. N. 1994. Logic programming and negation: A survey. J. Log. Program. 19/20, 9--71.
• 14: Khaled A. Arisha , Fatma Ozcan , Robert Ross , V. s. Subrahmanian , Thomas Eiter , Sarit Kraus, Impact: A Platform for Collaborating Agents, IEEE Intelligent Systems, v.14 n.2, p.64-72, March 1999 [doi>10.1109/5254.757633]
• 15: Alexander Artikis , Jeremy Pitt , Marek Sergot, Animated specifications of computational societies, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 3, July 15-19, 2002, Bologna, Italy [doi>10.1145/545056.545070]
• 16: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 17: Rafael H. Bordini , Michael Fisher , Willem Visser , Michael Wooldridge, Verifying Multi-agent Programs by Model Checking, Autonomous Agents and Multi-Agent Systems, v.12 n.2, p.239-256, March 2006 [doi>10.1007/s10458-006-5955-7]
• 18: Hans-Jürgen Bürckert, A resolution principle for constrained logics, Artificial Intelligence, v.66 n.2, p.235-271, April 1994 [doi>10.1016/0004-3702(94)90027-2]
• 19: Castelfranchi, C. 1995. Commitments: From individual intentions to groups and organizations. In Proceedings of the First International Conference on Multiagent Systems, San Francisco, California, USA. AAAI Press, Menlo Porle, CA, 41--48.
• 20: Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996 [doi>10.1145/227595.227597]
• 21: Clark, K. L. 1978. Negation as failure. In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, NY, 293--322.
• 22: Cohen, P. R. and Perrault, C. R. 1979. Elements of a plan-based theory of speech acts. Cog. Sci. 3, 3.
• 23: Colombetti, M., Fornara, N., and Verdicchio, M. 2004. A social approach to communication in multiagent systems. In Declarative Agent Languages and Technologies, J. A. Leite, A. Omicini, L. Sterling, and P. Torroni, Eds. Lecture Notes in Artificial Intelligence, vol. 2990. Springer-Verlag, Berlin, Germany, 191--220. First International Workshop, DALT 2003. Melbourne, Australia, July 2003. Revised selected and invited papers.
• 24: Console, L., Dupré, D. T., and Torasso, P. 1991. On the relationship between abduction and deduction. J. Log. Computat. 1, 5, 661--690.
• 25: Pierangelo Dell'Acqua , Fariba Sadri , Francesca Toni, Combining Introspection and Communication with Rationality and Reactivity in Agents, Proceedings of the European Workshop on Logics in Artificial Intelligence, p.17-32, October 12-15, 1998
• 26: Denecker, M. and De Schreye, D. 1992. SLDNFA: An abductive procedure for normal abductive programs. In Proceedings of the Joint International Conference and Symposium on Logic Programming, Washington, USA, K. R. Apt, Ed. MIT Press, Cambridge, MA, 686--702.
• 27: Marc Denecker , Danny De Schreye, Representing incomplete knowledge in abductive logic programming, Proceedings of the 1993 international symposium on Logic programming, p.147-163, December 1993, Vancouver, British Columbia, Canada
• 28: Denecker, M. and De Schreye, D. 1998. SLDNFA: An abductive procedure for abductive logic programs. J. Log. Program. 34, 2, 111--167.
• 29: Virginia Dignum , John-Jules Meyer , Hans Weigand, Towards an organizational model for agent societies using contracts, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544909]
• 30: Thomas Eiter , V. S. Subrahmanian , George Pick, Heterogeneous active agents, I: semantics, Artificial Intelligence, v.108 n.1-2, p.179-255, March 1999 [doi>10.1016/S0004-3702(99)00005-3]
• 31: Endriss, U., Mancarella, P., Sadri, F., Terreni, G., and Toni, F. 2004. The CIFF proof procedure for abductive logic programming with constraints. In Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27--30, 2004, Proceedings, J. J. Alferes and J. A. Leite, Eds. Lecture Notes in Artificial Intelligence, vol. 3229. Springer-Verlag, Berlin, Germany, 31--43.
• 32: Eshghi, K. and Kowalski, R. A. 1989. Abduction compared with negation by failure. In Proceedings of the 6th International Conference on Logic Programming, G. Levi and M. Martelli, Eds. MIT Press, Cambridge, MA, 234--255.
• 33: Evans, C. and Kakas, A. 1992. Hypotheticodeductive reasoning. In Proceedings of the International Conference on Fifth Generation Computer Systems (Tokyo). 546--554.
• 34: FIPA. 2001. FIPA Communicative Act Library Specification. Experimental specification XC00037H, Foundation for Intelligent Physical Agents. Aug. Published on August 10, 2001; available for download from the FIPA Web site, http://www.fipa.org.
• 35: FIPA. 2002. FIPA Request Interaction Protocol Specification. Standard SC00026H, Foundation for Intelligent Physical Agents. Dec. Published on December 3, 2002; available for download from the FIPA Web site, http://www.fipa.org.
• 36: Nicoletta Fornara , Marco Colombetti, Operational specification of a commitment-based agent communication language, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544868]
• 37: Nicoletta Fornara , Marco Colombetti, Defining interaction protocols using a commitment-based agent communication language, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia [doi>10.1145/860575.860659]
• 38: Frühwirth, T. 1998. Theory and practice of constraint handling rules. J. Log. Program. 37, 1-3 (Oct.), 95--138.
• 39: Fung, T. H. 1996. Abduction by deduction. Ph.D. dissertation, Imperial College London, London, U.K.
• 40: Fung, T. H. and Kowalski, R. A. 1997. The IFF proof procedure for abductive logic programming. J. Log. Program. 33, 2 (Nov.), 151--165.
• 41: Gavanelli, M., Lamma, E., and Mello, P. 2005a. Proof of completeness of the SCIFF proof-procedure. Tech. rep. CS-2005-02. Dipartimento di Ingegneria, Università di Ferrara, Ferrara, Italy. Available at online http://www.ing.unife.it/informatica/tr/CS-2005-02.pdf.
• 42: Gavanelli, M., Lamma, E., and Mello, P. 2005b. Proof of properties of the SCIFF proof-procedure. Tech. rep. CS-2005-01. Dipartimento di Ingegneria, Università di Ferrara, Ferrara, Italy. Available online at http://www.ing.unife.it/informatica/tr/CS-2005-01.pdf.
• 43: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 44: Jaffar, J. and Maher, M. 1994. Constraint logic programming: A survey. J. Log. Program. 19-20, 503--582.
• 45: Kakas, A., Mancarella, P., Sadri, F., Stathis, K., and Toni, F. 2004. The KGP model of agency. In Proceedings of the Sixteenth European Conference on Artificial Intelligence, Valencia, Spain (ECAI 2004), R. Lopez de Mantaras and L. Saitta, Eds. IOS Press, Amsterdam, The Netherlands.
• 46: Kakas, A. C., Kowalski, R. A., and Toni, F. 1993. Abductive logic programming. J. Log. Computat. 2, 6, 719--770.
• 47: Kakas, A. C. and Mancarella, P. 1990. On the relation between truth maintenance and abduction. In Proceedings of the 1st Pacific Rim International Conference on Artificial Intelligence, PRICAI-90, Nagoya, Japan, T. Fukumura, Ed. Ohmsha Ltd., Tokyo, Japan, 438--443.
• 48: Kakas, A. C., Michael, A., and Mourlas, C. 2000. ACLP: Abductive constraint logic programming. J. Log. Program. 44, 1-3 (July), 129--177.
• 49: Kakas, A. C., van Nuffelen, B., and Denecker, M. 2001. A-System: Problem solving through abduction. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, Seattle, Washington, USA (IJCAI-01), B. Nebel, Ed. Morgan Kaufmann Publishers, San Francisco, CA, 591--596.
• 50: Robert A. Kowalski , Francesca Toni , Gerhard Wetzel, Executing suspended logic programs, Fundamenta Informaticae, v.34 n.3, p.203-224, June 1, 1998
• 51: Kowalski, R. A. 2006. The logical way to be artificially intelligent. In Computational Logic in Multi-Agent Systems, 6th International Workshop, CLIMA VI, London, UK, June 27--29, 2005, Revised Selected and Invited Papers, P. Torroni and F. Toni, Eds. Lecture Notes in Artificial Intelligence, vol. 3900. Springer-Verlag, Berlin, Germany.
• 52: Robert Kowalski , Fariba Sadri, From logic programming towards multi-agent systems, Annals of Mathematics and Artificial Intelligence, v.25 n.3-4, p.391-419, 1999 [doi>10.1023/A:1018934223383]
• 53: Kowalski, R. A., Sadri, F., and Toni, F. 1998b. An agent architecture that combines backward and forward reasoning. In Proceedings of the CADE-15 Workshop on Strategies in Automated Deduction, B. Gramlich and F. Pfenning, Eds. 49--56.
• 54: Kenneth Kunen, Negation in logic programming, Journal of Logic Programming, v.4 n.4, p.289-308, December 1, 1987 [doi>10.1016/0743-1066(87)90007-0]
• 55: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 56: Mancarella, P. and Terreni, G. 2003. An abductive proof procedure handling active rules. In AI*IA 2003: Advances in Artificial Intelligence, Proceedings of the 8th Congress of the Italian Association for Artificial Intelligence, Pisa, A. Cappelli and F. Turini, Eds. Lecture Notes in Artificial Intelligence, vol. 2829. Springer-Verlag, Berlin, Germany, 105--117.
• 57: Meyer, J. J. C. 1988. A different approach to deontic logic: Deontic logic viewed as a variant of dynamic logic. Notre Dame J. Form. Log. 29, 1, 109--136.
• 58: Prakken, H. and Sergot, M. 1996. Contrary-to-duty obligations. Studia Logica 57, 1, 91--115.
• 59: Reiter, R. 1978. On closed-word data bases. In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, NY, 55--76.
• 60: Young U. Ryu , Ronald M. Lee, Defeasible deontic reasoning: a logic programming model, Deontic logic in computer science: normative system specification, John Wiley and Sons Ltd., Chichester, UK, 1994
• 61: Fariba Sadri , Francesca Toni, Abduction with Negation as Failure for Active and Reactive Rules, Proceedings of the 6th Congress of the Italian Association for Artificial Intelligence on Advances in Artificial Intelligence, p.49-60, September 14-17, 1999
• 62: Fariba Sadri , Francesca Toni , Paolo Torroni, An Abductive Logic Programming Architecture for Negotiating Agents, Proceedings of the European Conference on Logics in Artificial Intelligence, p.419-431, September 23-26, 2002
• 63: Sartor, G. 2005. Legal Reasoning: A Cognitive Approach to the Law. Springer, Berlin, Germany.
• 64: Speculative Computation by Abduction under Incomplete Communication Environments, Proceedings of the Fourth International Conference on MultiAgent Systems (ICMAS-2000), p.263, July 10-12, 2000
• 65: Satoh, K. and Iwayama, N. 1992. A query evaluation method for abductive logic programming. In Proceedings of the Joint International Conference and Symposium on Logic Programming, Washington, USA, K. Apt, Ed. MIT Press, Cambridge, MA, 671--685.
• 66: Murray Shanahan, Reinventing Shakey, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2001
• 67: SICStus 2006. SICStus Prolog user manual, release 3.12.7. Available online at http://www.sics.se/isl/sicstus/.
• 68: Munindar P. Singh, Agent Communication Languages: Rethinking the Principles, Computer, v.31 n.12, p.40-47, December 1998 [doi>10.1109/2.735849]
• 69: SOCS. 2002--2005. Societies Of ComputeeS (SOCS): A computational logic model for the description, analysis and verification of global and open societies of heterogeneous computees. IST-2001-32530. http://lia.deis.unibo.it/research/socs/.
• 70: SOCS-PR. 2005. The SOCS protocol repository. Available online at http://edu59.deis.unibo.it:8079/SOCSProtocolsRepository/jsp/index.jsp.
• 71: SOCS-SI 2006. SOCS-SI home page. Available online at http://lia.deis.unibo.it/research/socs_si/.
• 72: Peter J. Stuckey, Negation and constraint logic programming, Information and Computation, v.118 n.1, p.12-33, April 1995 [doi>10.1006/inco.1995.1048]
• 73: van der Torre, L. W. N. and Tan, Y.-H. 1999. Diagnosis and decision making in normative reasoning. Artific. Intell. Law 7, 1, 51--67.
• 74: van Hentenryck, P. and Deville, Y. 1991. The Cardinality Operator: A new logical connective for constraint logic programming. In Logic Programming, Proceedings of the Eigth International Conference (Paris, France), K. Furukawa, Ed. Vol. 2. 745--759.
• 75: Pascal Van Hentenryck , Vijay Saraswat , Yves Deville, Design, Implementation, and Evaluation of the Constraint Language cc(FD), Brown University, Providence, RI, 1993
• 76: van Nuffelen, B. and Denecker, M. 2000. Problem solving in ID-logic with aggregates. In Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (NMR'00, Breckenridge, CO). 1--9.
• 77: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 78: Michael Woolridge , Michael J. Wooldridge, Introduction to Multiagent Systems, John Wiley & Sons, Inc., New York, NY, 2001
• 79: Wooldridge, M., Huget, M.-P., Fisher, M., and Parsons, S. 2006. Model checking for multiagent systems: The MABLE language and its applications. Int. J. Artific. Intell. Tools 15, 2, 195--226.
• 80: Wright, G. 1951. Deontic logic. Mind 60, 1--15.
• 81: Xanthakos, I. 2003. Semantic integration of information by abduction. Ph.D. dissertation. Imperial College London, London, U.K. Available online at http://www.doc.ic.ac.uk/~ix98/PhD.zip.
• 82: Pinar Yolum , Munindar P. Singh, Flexible protocol specification and execution: applying event calculus planning using commitments, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544867]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems
      I.2.3 Deduction and Theorem Proving
          Subjects: Inference engines

General Terms:
Languages, Theory, Verification

Keywords:
Abductive logic programming, IFF proof procedure, SCIFF, SOCS (SOcieties of ComputeeS), agent interaction protocols, declarative semantics, formal properties, proof-procedures