Model-checking agent refinement

ABSTRACT

We present a proof-technique for reducing the nondeterminism of abstract agent specifications in a BDI framework by means of refinement. We implement the operational semantics of agent specifications in rewrite systems such that we can automatically check if refinement between (fair) executions of agents holds.

REFERENCES

• 1: Farhad Arbab, Reo: a channel-based coordination model for component composition, Mathematical Structures in Computer Science, v.14 n.3, p.329-366, June 2004 [doi>10.1017/S0960129504004153]
• 2: 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]
• 3: Tibor Bosse , Catholijn M. Jonker , Lourens van der Meij , Alexei Sharpanskykh , Jan Treur, Specification and Verification of Dynamics in Cognitive Agent Models, Proceedings of the IEEE/WIC/ACM international conference on Intelligent Agent Technology, p.247-254, December 18-22, 2006 [doi>10.1109/IAT.2006.112]
• 4: M. Bratman. Intentions, Plans, and Practical Reason. Harvard University Press, 1987.
• 5: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 6: M. Clavel , F. Durán , S. Eker , P. Lincoln , N. Martí-Oliet , J. Meseguer , J. F. Quesada, Maude: specification and programming in rewriting logic, Theoretical Computer Science, v.285 n.2, p.187-243, 28 August 2002 [doi>10.1016/S0304-3975(01)00359-0]
• 7: Manuel Clavel , Francisco Durán , Steven Eker , Patrick Lincoln , Narciso Martí-Oliet , José Meseguer , Carolyn Talcott, All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic (Lecture Notes in Computer Science), Springer-Verlag New York, Inc., Secaucus, NJ, 2007
• 8: F. S. de Boer, K. V. Hindriks, W. van der Hoek, and J.-J. C. Meyer. A verification framework for agent programming with declarative goals. J. Applied Logic, 5(2):277--302, 2007.
• 9: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 10: S. Eker, J. Meseguer, and A. Sridharanarayanan. The Maude LTL model checker and its implementation. In Model Checking Software: Proc. 10 th Intl. SPIN Workshop, volume 2648 of LNCS, pages 230--234. Springer, 2003.
• 11: Koen V. Hindriks , Frank S. De Boer , Wiebe Van Der Hoek , John-Jules Ch. Meyer, Agent Programming in 3APL, Autonomous Agents and Multi-Agent Systems, v.2 n.4, p.357-401, November 1999 [doi>10.1023/A:1010084620690]
• 12: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 13: J. Meseguer and G. Rosu. Rewriting logic semantics: From language specifications to formal analysis tools.
• 14: F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. J. Applied Logic, 5(2):235--251, 2007.
• 15: S. Safra. Complexity of automata on infinite objects. PhD thesis, Rehovot, Israel, 1989.
• 16: M. Birna van Riemsdijk , Frank S. de Boer , Mehdi Dastani , John-Jules Ch. Meyer, Prototyping 3APL in the Maude term rewriting language, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan [doi>10.1145/1160633.1160865]
• 17: Alberto Verdejo , Narciso Martí-Oliet, Two case studies of semantics execution in Maude: CCS and LOTOS, Formal Methods in System Design, v.27 n.1/2, p.113-172, September 2005 [doi>10.1007/s10703-005-2254-x]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.5 Model Development

General Terms:
Languages, Theory, Verification

Keywords:
BDI, non-determinism, refinement, rewriting, simulation