Advertisement

Verifying Dribble Agents

  • Doan Thu Trang
  • Brian Logan
  • Natasha Alechina
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5948)

Abstract

We describe a model-checking based approach to verification of programs written in the agent programming language Dribble. We define a logic (an extension of the branching time temporal logic CTL) which describes transition systems corresponding to a Dribble program, and show how to express properties of the agent program in the logic and how to encode transition systems as an input to a model-checker. We prove soundness and completeness of the logic and a correspondence between the operational semantics of Dribble and the models of the logic.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alechina, N., Dastani, M., Logan, B., Meyer, J.-J.C.: A logic of agent programs. In: Proc. of the 22nd National Conf. on Artificial Intelligence (AAAI 2007), pp. 795–800. AAAI Press, Menlo Park (2007)Google Scholar
  2. 2.
    Alechina, N., Dastani, M., Logan, B., Meyer, J.-J.C.: Reasoning about agent deliberation. In: Proc. of the 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2008), pp. 16–26. AAAI, Menlo Park (2008)Google Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Computer Aided Verification, pp. 521–525 (1998)Google Scholar
  4. 4.
    Bordini, R., Fisher, M., Visser, W., Wooldridge, M.: State-space reduction techniques in agent verification. In: Proceedings of the 3rd Int. Joint Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 2004), pp. 896–903. ACM Press, New York (2004)Google Scholar
  5. 5.
    Bordini, R.H., Dastani, M., Dix, J., Fallah-Seghrouchni, A.E. (eds.): Multi-Agent Programming: Languages, Platforms and Applications. Multiagent Systems, Artificial Societies, and Simulated Organizations, vol. 15. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  6. 6.
    Bordini, R.H., Hübner, J.F., Vieira, R.: Jason and the Golden Fleece of agent-oriented programming. In: Multi-Agent Programming: Languages, Platforms and Applications, ch. 1. Springer, Heidelberg (2005)Google Scholar
  7. 7.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  8. 8.
    Claßen, J., Lakemeyer, G.: A logic for non-terminating Golog programs. In: Proceedings of the 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2008), pp. 589–599. AAAI, Menlo Park (2008)Google Scholar
  9. 9.
    Dastani, M., van Riemsdijk, M.B., Dignum, F., Meyer, J.-J.C.: A programming language for cognitive agents goal directed 3apl. In: Dastani, M.M., Dix, J., El Fallah-Seghrouchni, A. (eds.) PROMAS 2003. LNCS (LNAI), vol. 3067, pp. 111–130. Springer, Heidelberg (2004)Google Scholar
  10. 10.
    Dastani, M., van Riemsdijk, M.B., Meyer, J.-J.C.: A grounded specification language for agent programs. In: Proceedings of the Sixth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2007), pp. 578–585. ACM Press, New York (2007)Google Scholar
  11. 11.
    Dennis, L.A., Farwer, B., Bordini, R.H., Fisher, M.: A flexible framework for verifying agent programs. In: 7th Int. Joint Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2008), IFAAMAS, pp. 1303–1306 (2008)Google Scholar
  12. 12.
    Dennis, L.A., Fisher, M.: Programming verifiable heterogeneous agent systems. In: 6th Int. Workshop on Programming in Multi-Agent Systems (ProMAS 2008), pp. 27–42 (2008)Google Scholar
  13. 13.
    Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1–24 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Fisher, M.: Metatem: The story so far. In: Bordini, R.H., Dastani, M.M., Dix, J., El Fallah Seghrouchni, A. (eds.) PROMAS 2005. LNCS (LNAI), vol. 3862, pp. 3–22. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Morley, D., Myers, K.: The SPARK agent framework. In: Proc. of the 3rd Int. Joint Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2004), pp. 714–721. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  17. 17.
    Thangarajah, J., Harland, J., Morley, D., Yorke-Smith, N.: Aborting tasks in bdi agents. In: Proc. of the 6th Int. Joint Conf. on Autonomous Agents and Multi Agent Systems (AAMAS 2007), pp. 8–15 (2007)Google Scholar
  18. 18.
    van Riemsdijk, B., van der Hoek, W., Meyer, J.-J.C.: Agent programming in dribble: from beliefs to goals using plans. In: Proc. of the 2nd Int. Joint Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2003), pp. 393–400. ACM Press, New York (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Doan Thu Trang
    • 1
  • Brian Logan
    • 1
  • Natasha Alechina
    • 1
  1. 1.School of Computer ScienceThe University of Nottingham 

Personalised recommendations