Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Verifying Protocol Conformance for Logic-Based Communicating Agents

  • Conference paper
  • First Online:
Computational Logic in Multi-Agent Systems (CLIMA 2004)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3487))

Included in the following conference series:

Abstract

Communication plays a fundamental role in multi-agents systems. One of the main issues in the design of agent interaction protocols is the verification that a given protocol implementation is “conformant” w.r.t. the abstract specification of it. In this work we tackle those aspects of the conformance verification issue, that regard the dependence/independence of conformance from the agent private state in the case of logic, individual agents, set in a multi-agent framework. We do this by working on a specific agent programming language, DyLOG, and by focussing on interaction protocol specifications described by AUML sequence diagrams. By showing how AUML sequence diagrams can be translated into regular grammars and, then, by interpreting the problem of conformance as a problem of language inclusion, we describe a method for automatically verifying a form of “structural” conformance; such a process is shown to be decidable and an upper bound of its complexity is given. We also give a set of properties that describes the influence of the agent private information on the conformance of its communication policies to protocol specifications.

This research is partially supported by MIUR Cofin 2003 “Logic-based development and verification of multi-agent systems (MASSiVE)” national project and by the European Commission and by the Swiss Federal Office for Education and Science within the 6th Framework Programme project REWERSE number 506779.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Alberti, M., Daolio, D., Torroni, P., Gavanelli, M., Lamma, E., Mello, P.: Specification and verification of agent interaction protocols in a logic-based system. In: Haddad, H., Omicini, A., Wainwright, R.L., Liebrock, L.M. (eds.) Proc. of the 2004 ACM Symposium on Applied Computing, SAC 2004, Nicosia, Cyprus, pp. 72–78. ACM, New York (2004)

    Google Scholar 

  2. Baldoni, M.: Normal Multimodal Logics with Interaction Axioms. In: Basin, D., D’Agostino, M., Gabbay, D.M., Matthews, S., Viganò, L. (eds.) Labelled Deduction. Applied Logic Series, vol. 17, pp. 33–53. Kluwer Academic Publisher, Dordrecht (2000)

    Chapter  Google Scholar 

  3. Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Reasoning about self and others: communicating agents in a modal action logic. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol. 2841, pp. 228–241. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Baldoni, M., Giordano, L., Martelli, A.: A Tableau Calculus for Multimodal Logics and Some (un)Decidability Results. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 44–59. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  5. Baldoni, M., Giordano, L., Martelli, A., Patti, V.: Programming Rational Agents in a Modal Action Logic. Annals of Mathematics and Artificial Intelligence, Special issue on Logic-Based Agent Implementation 41(2-4), 207–257 (2004)

    Article  MathSciNet  Google Scholar 

  6. Barbuceanu, M., Fox, M.S.: Cool: a language for describing coordination in multiagent systems. In: The 1st Int. Conf. on Multi-Agent Systems (ICMAS 1995). AAAI Press, Menlo Park (1995)

    Google Scholar 

  7. Bentahar, J., Moulin, B., Meyer, J.J.C., Chaib-Draa, B.: A computational model for conversation policies for agent communication. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS (LNAI), vol. 3487, pp. 178–195. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Bouajjani, A., Esparza, J., Finkel, A., Maler, O., Rossmanith, P., Willems, B., Wolper, P.: An efficient automata approach to some problems on context-free grammars. Information Processing Letters 74(5–6), 221–227 (2000)

    Article  MathSciNet  Google Scholar 

  9. Bracciali, A., Mancarella, P., Stathis, K., Toni, F.: On modelling declaratively multiagent systems. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 76–92. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Cabac, L., Moldt, D.: Formal semantics for auml agent interaction protocol diagrams. In: Odell, J.J., Giorgini, P., Müller, J.P. (eds.) AOSE 2004. LNCS, vol. 3382, pp. 47–61. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Cost, R.S., Chen, Y., Finin, T., Labrou, Y., Peng, Y.: Modeling agent conversation with colored petri nets. In: Autonomous Agents Workshop on Conversation Policies (1999)

    Google Scholar 

  12. Endriss, U., Maudet, N., Sadri, F., Toni, F.: Logic-based agent communication protocols. In: Dignum, F.P.M. (ed.) ACL 2003. LNCS (LNAI), vol. 2922, pp. 91–107. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Esparza, J., Rossmanith, P., Schwoon, S.: A uniform framework for problems on context-free grammars. EATCS Bulletin 72, 169–177 (2000)

    MathSciNet  MATH  Google Scholar 

  14. Fariñas del Cerro, L., Penttonen, M.: Grammar Logics. Logique et Analyse, 121–122, 123–134 (1988)

    Google Scholar 

  15. Finger, M., Fisher, M., Owens, R.: Metatem: modeling reactive systems using executable temporal logic. In: The Int. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, IEA-AIE (1993)

    Google Scholar 

  16. Fisher, M., Wooldridge, M.J.: Specifying and executing protocols for cooperative actions. In: The Int. Working Conf. on Cooperative Knowledge-Based Systems, CKBS 1994 (1994)

    Google Scholar 

  17. Foundation for InteroPerable Agents. Fipa modeling: Interaction diagrams. Technical report. Working Draft Version 2003-07-02 (2003)

    Google Scholar 

  18. Giordano, L., Martelli, A., Schwind, C.: Verifying communicating agents by model checking in a temporal action logic. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 57–69. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Guerin, F., Pitt, J.: Verification and compliance testing. In: Huget, M.-P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 98–112. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, Reading (1979)

    MATH  Google Scholar 

  21. Kacprzak, M., Lomuscio, A., Penczek, W.: Verification of multiagent systems via unbounded model checking. In: Proc. of the 3rd Int. Joint Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2004), New York, NY, USA (2004)

    Google Scholar 

  22. Huget, M.P., Koning, J.L.: Interaction Protocol Engineering. In: Huget, H.P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 179–193. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  23. Koning, J.-L., Franois, G., Demazeau, Y.: Formalization and pre-validation for interaction protocols in multiagent systems. In: The 13th European Conference on Artificial Intelligence, ECAI 1998 (1998)

    Google Scholar 

  24. Kuwabara, K., Ishida, T., Osato, N.: Agentalk: describing multiagent coordination protocols with inheritance. In: 7th Int. Conf. on Tools for Artificial Intelligence, ICTAI 1995 (1995)

    Google Scholar 

  25. Leite, J., Omicini, A., Torroni, P., Yolum, P. (eds.): DALT 2004. LNCS (LNAI), vol. 3476. Springer, Heidelberg (2005)

    Google Scholar 

  26. Levesque, H.J., Reiter, R., Lespérance, Y., Lin, F., Scherl, R.B.: GOLOG: A Logic Programming Language for Dynamic Domains. J. of Logic Programming 31, 59–83 (1997)

    Article  MathSciNet  Google Scholar 

  27. Odell, J., Parunak, H.V.D., Bauer, B.: Extending UML for agents. In: Proceedings of the Agent-Oriented Information System Workshop at the 17th National Conference on Artificial Intelligence (2000)

    Google Scholar 

  28. Pokorny, L.R., Ramakrishnan, C.R.: Modeling and verification of distributed autonomous agents using logic programming. In: Leite, J., Omicini, A., Torroni, P., Yolum, P. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 172–187. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  29. Singh, M.P.: A social semantics for agent communication languages. In: Proc. of IJCAI 1998 Workshop on Agent Communication Languages. Springer, Berlin (2000)

    Google Scholar 

  30. Walton, C.: Model checking agent dialogues. In: Leite, J., Omicini, A., Torroni, P., Yolum, P. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 156–171. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Torino, C.so Svizzera, 185, I-10149, Torino, Italy

    Matteo Baldoni, Cristina Baroglio, Alberto Martelli, Viviana Patti & Claudio Schifanella

Authors
  1. Matteo Baldoni
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cristina Baroglio
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Martelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Viviana Patti
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Claudio Schifanella
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Informática, Universidade Nova de Lisboa, 2829-516, Caparica, Portugal

    João Leite

  2. DEIS, University of Bologna, V.le Risorgimento 2Q, 40136, Bologna, Italy

    Paolo Torroni

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C. (2005). Verifying Protocol Conformance for Logic-Based Communicating Agents. In: Leite, J., Torroni, P. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2004. Lecture Notes in Computer Science(), vol 3487. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11533092_12

Download citation

  • DOI: https://doi.org/10.1007/11533092_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28060-6

  • Online ISBN: 978-3-540-31857-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation