Skip Navigation



Journal of Logic and Computation Advance Access published online on June 16, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp029
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bordini, R. H.
Right arrow Articles by Visser, W.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Property-based Slicing for Agent Verification

Rafael H. Bordini

Department of Computer Science, University of Durham, Durham, UK.
E-mail: R.Bordini{at}inf.ufrgs.br
Present Address: Institute of Informatics, Federal University of Rio Grande do Sul, Porto Alegre, Brazil.

Michael Fisher and Michael Wooldridge

Department of Computer Science, University of Liverpool, Liverpool, UK.
E-mail: MFisher{at}liverpool.ac.uk; mjw{at}liverpool.ac.uk

Willem Visser

Department of Mathematical Sciences, Computer Science Division, Stellenbosch University, Stellenbosch, South Africa.
E-mail: wvisser{at}cs.sun.ac.za

Received 1 May 2009.

Programming languages designed specifically for multi-agent systems represent a new programming paradigm that has gained popularity over recent years, with some multi-agent programming languages being used in increasingly sophisticated applications, often in critical areas. To support this, we have developed a set of tools to allow the use of model-checking techniques in the verification of systems directly implemented in one particular language called AgentSpeak. The success of model checking as a verification technique for large software systems is dependent partly on its use in combination with various state-space reduction techniques, an important example of which is property-based slicing. This article introduces an algorithm for property-based slicing of AgentSpeak multi-agent systems. The algorithm uses literal dependence graphs, as developed for slicing logic programs, and generates a program slice whose state space is stuttering-equivalent to that of the original program; the slicing criterion is a property in a logic with LTL operators and (shallow) BDI modalities. In addition to showing correctness and characterizing the complexity of the slicing algorithm, we apply it to an AgentSpeak program based on autonomous planetary exploration rovers, and we discuss how slicing reduces the model-checking state space. The experiment results show a significant reduction in the state space required for model checking that agent, thus indicating that this approach can have an important impact on the future practicality of agent verification.

Keywords: Program verification; multi-agent programming languages; property-based slicing; model checking; multi-agent systems



References

  1. Allen Emerson E. Temporal and Modal Logic. In: Handbook of Theoretical Computer Science—van Leeuwen J, ed. (1990) B. Elsevier Science. 997–1072. Ch. 16.
  2. Benerecetti M, Cimatti A. Validation of multiagent systems by symbolic model checking. In: Proceedings of the 3rd International Workshop on Agent-Oriented Software Engineering (AOSE) (2003) Springer. 32–46. Vol. 2585 of Lecture Notes in Computer Science.
  3. Biesiadecki J, Maimone MW, Morrison J. The Athena SDM rover: a testbed for Mars rover mobility. (2001) In Sixth International Symposium on AI, Robotics and Automation in Space (ISAIRAS-01), June, Montreal, Canada.
  4. Bordini RH, Dastani M, Dix J, El Fallah Seghrouchni A, eds. Multi-Agent Programming: Languages, Platforms and Applications (2005) Springer. Number 15 in Multiagent Systems, Artificial Societies, and Simulated Organizations.
  5. Bordini RH, Fisher M, Visser W, Wooldridge M. Model checking rational agents. IEEE Intelligent Systems (2004) 19:46–52.[CrossRef][Web of Science]
  6. Bordini RH, Fisher M, Visser W, Wooldridge M. Verifying multi-agent programs by model checking. Journal of Autonomous Agents and Multi-Agent Systems (2006) 12:239–256.[CrossRef]
  7. Bordini RH, Hübner JF, Wooldridge M. Programming Multi-Agent Systems in AgentSpeak Using Jason. Wiley Series in Agent Technology (2007) JohnWiley & Sons.
  8. Bordini RH, Moreira ÁF. Proving BDI properties of agent-oriented programming languages: the asymmetry thesis principles in AgentSpeak(L). Annals of Mathematics and Artificial Intelligence (2004) 42:197–226. (Special Issue on Computational Logic in Multi-Agent Systems).[CrossRef][Web of Science]
  9. Canfora G, Cimitile A, Lucia ADe. Conditioned program slicing. In: Information and Software Technology, Special Issue on Program Slicing—Harman M, Gallagher K, eds. (1998) Elsevier. 40.
  10. Cheda D, Cavadini S. Conditional slicing for first-order functional logic programs. In. In: 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP-2008), Siena, Italy, 3–4 July (2008).
  11. Clarke EM Jr., Grumberg O, Peled DA. Model Checking (1999) MIT Press.
  12. Cohen PR, Levesque HJ. Intention is choice with commitment. Artificial Intelligence (1990) 42:213–261.[CrossRef][Web of Science]
  13. Corbett JC, Dwyer MB, John H, Robby. Bandera: a source-level interface for model checking Java programs. (2000) ACM Press. 762–765. In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), 4–11 June, Limerick, Ireland.
  14. Dennis LA, Farwer B, Bordini RH, Fisher M, Wooldridge M. A Common Semantic Basis for BDI Languages. In: Proceedings of the Seventh International Workshop on Programming Multiagent Systems (ProMAS), Lecture Notes in Artificial Intelligence (2007) Springer.
  15. Fisher M, Bordini RH, Hirsch B, Torroni P. Computational logics and agents: a road map of current technologies and future trends. Computational Intelligence (2009) 23:61–91.[CrossRef]
  16. Fisher M, Gabbay D, Vila L, eds. Handbook of Temporal Reasoning in Artificial Intelligence (2005) North Holland: Elsevier Publishers. Vol. 1 of Advances in Artificial Intelligence.
  17. Francel MA, Rugaber S. The value of slicing while debugging. Science of Computer Programming (2001) 40:151–169.[CrossRef][Web of Science]
  18. Gallagher KB, Lyle JR. Using program slicing in software maintenance. IEEE Transactions on Software Engineering (1991) 17:751–761.[CrossRef][Web of Science]
  19. Giordano L, Martelli A, Schwind C. Specifying and verifying interaction protocols in a temporal action logic. Journal of Applied Logic (2007) 5:214–234.[CrossRef]
  20. Harel D, Kozen D, Tiuryn J. Dynamic Logic (2000) MIT Press.
  21. Harman M, Danicic S. Using program slicing to simplify testing. Software Testing, Verification and Reliability (1995) 5:143–162.[CrossRef]
  22. Harman M, Danicic S. Amorphous program slicing. In: WPC’97: Proceedings of the 5th International Workshop on Program Comprehension (WPC’97) (1997) IEEE Computer Society. 70–79.
  23. Hatcliff J, Dwyer MB. Using the Bandera Tool Set to model-check properties of concurrent Java software. Larsen KG, Nielsen M, eds. (2001) Springer. 39–58. In Proceedings of the 12th International Conference Concurrency Theory(CONCUR2001), Aalborg, Denmark, 20–25August, Vol. 2154 of Lecture Notes Computer Science.
  24. Holzmann GJ. The SPIN Model Checker: Primer and Reference Manual (2003) Addison-Wesley.
  25. Jennings NR, Wooldridge M, eds. Applications of agent technology. In: Agent Technology: Foundations, Applications, and Markets (1998) Springer.
  26. Java PathFinder. (2009) Available at http://javapathfinder.sourceforge.net.
  27. Krishna Rao M, Kapur D, Shyamasundar R. Proving termination of GHC Programs. Warren DS, ed. (1993) MIT Press. 720–736. In Proceedings of the Tenth International Conference on Logic Programming, 21–24 June, Budapest, Hungary.
  28. Lanubile F, Visaggio G. Extracting reusable functions by flow graph-based program slicing. IEEE Transactions Software Engineering (1997) 23:246–259.[CrossRef]
  29. Ljunberg M, Lucas A. The OASIS air traffic management system. (1992) Korea: Seoul. In Proceedings of the Second Pacific Rim International Conference on AI (PRICAI-92).
  30. Lloyd JW. Foundations of Logic Programming (1987) 2nd edn. Springer.
  31. Lucia AD, Fasolino AR, Munro M. Understanding function behaviors through program slicing. In: 4th International Workshop on Program Comprehension (WPC’96), March 29-31, 1996, Berlin, Germany (1996) IEEE Computer Society. 9–10.
  32. Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification (1992) Springer.
  33. Mayfield J, Labrou Y, Finin T. Evaluation of KQMLas an agent communication language. In: Intelligent Agents II—Proceedings of the Second International Workshop on Agent Theories, Architectures, and Languages (ATAL’95), held as part of IJCAI’95, Montréal, Canada, August 1995—Wooldridge M, Müller JP, Tambe M, eds. (1996) Springer. 347–360. Number 1037 in Lecture Notes in Artificial Intelligence.
  34. Moreno A, Garbay C. Special issue on "Software Agents in Health Care". Artificial Intelligence in Medicine (2003) 27:229–232.[CrossRef][Web of Science][Medline]
  35. Muscettola N, Pandurang Nayak P, Pell B, Williams BC. Remote Agent: to boldly go where no AI system has gone before. Artificial Intelligence (1998) 103:5–47.[CrossRef][Web of Science]
  36. Osman N, Robertson D. Dynamic verification of trust in distributed open systems. (2007) 1440–1445. In IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007.
  37. Plotkin G. A structural approach to operational semantics. In: Technical Report DAIMI FN-19 (1981) Department of Computer Science, Aarhus University.
  38. Raimondi F, Lomuscio A. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic (2007) 5:235–251.[CrossRef]
  39. Rao AS. AgentSpeak(L): BDI agents speak out in a logical computable language. In: Proceedings of the Seventh Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW’96), 22–25 January, Eindhoven, The Netherlands—Van de Velde W, Perram J, eds. (1996) Springer. 42–55. Number 1038 in Lecture Notes in Artificial Intelligence.
  40. Rao AS, Georgeff MP. Decision procedures for BDI logics. Journal of Logic and Computation (1998) 8:293–343.[Abstract/Free Full Text]
  41. Robby M, Dwyer B, Hatcliff J. Bogor: an extensible and highly-modular model checking framework. (2003) ACM Press. 267–276. In Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, Fourth Joint Meeting ESEC/FSE 2003, Helsinki, Finland, 1–5 September.
  42. Schoenig S, Ducassé M. A backward slicing algorithm for Prolog. Cousot R, Schmidt DA, eds. (1996) Springer. 317–331. In Proceedings of the Third International Symposium on Static Analysis (SAS’96), Aachen, Germany, 24–26 September 1996, Vol. 1145 of Lecture Notes in Computer Science.
  43. Szilágyi G, Gyimóthy T, Maluszynski J. Slicing of constraint logic programs. Ducassé M, ed. (2000) In Proceedings of the Fourth International Workshop on Automated Debugging (AADEBUG 2000), 28–30 August, Munich. Computing Research Repository cs.SE/0010035.
  44. Szilágyi G, Gyimóthy T, Maluszynski J. Static and dynamic slicing of constraint logic programs. Journal of Automated Software Engineering (2002) 9:41–65.[CrossRef]
  45. SPIN: on-the-fly LTL model checking. Available at http://spinroot.com/spin.
  46. Tadjouddine EM, Guerin F, Vasconcelos WW. Abstracting and verifying strategyproofness for auction mechanisms. In: Declarative Agent Languages and Technologies VI, 6th International Workshop, DALT 2008, Estoril, Portugal, May 12, 2008, Revised Selected and Invited Papers—Baldoni M, Son TC, van Riemsdijk MB, Winikoff M, eds. (2009) Springer. 197–214. Vol. 5397 of Lecture Notes in Computer Science.
  47. Tip F. Asurvey of program slicing techniques. Journal of Programming Languages (1995) 3:121–189.[Web of Science]
  48. van Riemsdijk MB, de Boer FS, Dastani M, Meyer J-JC. Prototyping 3APL in the Maude term rewriting language. In: Computational Logic in Multi-Agent Systems, 7th International Workshop, CLIMA VII, Hakodate, Japan, May 8-9, 2006, Revised Selected and Invited Papers—Inoue K, Satoh K, Toni F, eds. (2007) Springer. 95–114. Vol. 4371 of Lecture Notes in Computer Science.
  49. Vasconcelos WW, Aragão MAT. Slicing knowledge-based systems: techniques and applications. Knowledge-Based Systems (2000) 13:177–198.
  50. Vieira R, Moreira A, Wooldridge M, Bordini RH. On the formal semantics of speechact based communication in an agent-oriented programming language. Journal of Artificial Intelligence Research (JAIR) (2007) 29:221–267.
  51. Visser W, Havelund K, Brat G, Park S. Model Checking Programs. (2000) IEEE Computer Society. 3–12. In Proceedings of the Fifteenth International Conference on Automated Software Engineering (ASE’00), 11-15 September, Grenoble, France.
  52. Washington R, Golden K, Bresina J, Smith D, Anderson C, Smith T. Autonomous Rovers for Mars Exploration. In. In: Aerospace Conference, 6–13 March, Aspen, CO (1999) 1. IEEE. 237–251.
  53. Wobcke W, Chee M, Ji K. Model checking for prs-like agents. Zhang S, Jarvis R, eds. (2005) Springer. 17–28. In AI 2005: Advances in Artificial Intelligence, 18th Australian Joint Conference on Artificial Intelligence, Sydney, Australia, December 5-9, 2005, Proceedings, Vol. 3809 of Lecture Notes in Computer Science.
  54. Wooldridge M. Reasoning about Rational Agents (2000) The MIT Press.
  55. Xu B, Qian J, Zhang X, Wu Z, Chen L. A brief survey of program slicing. SIGSOFT Software Engineering Notes (2005) 30:1–36.
  56. Zhao J, Cheng J, Ushijima K. Literal dependence net and its use in concurrent logic programming environment. In. In: Proceedings of the Workshop on Parallel Logic Programming, held with FGCS’94, ICOT, Tokyo, 15–16 December (1994) 127–141.
  57. Zhao J, Cheng J, Ushijima K. Slicing concurrent logic programs. In. In: Proceedings of the Second Fuji International Workshop on Functional and Logic Programming, Shonan Village Center, Japan, 1–4 November 1996—Ida T, Ohori A, Takeichi M, eds. (1997) World Scientific. 143–162.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bordini, R. H.
Right arrow Articles by Visser, W.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?