skip to main content
10.5555/1402298.1402322acmconferencesArticle/Chapter ViewAbstractPublication PagesaamasConference Proceedingsconference-collections
research-article

Model-checking agent refinement

Published: 12 May 2008 Publication History

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]
F. Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 14(3):329--366, 2004.
[2]
R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Verifying multi-agent programs by model checking. Autonomous Agents and Multi-Agent Systems, 12(2):239--256, 2006.
[3]
T. Bosse, C. M. Jonker, L. van der Meij, A. Sharpanskykh, and J. Treur. Specification and verification of dynamics in cognitive agent models. In IAT, pages 247--254, 2006.
[4]
M. Bratman. Intentions, Plans, and Practical Reason. Harvard University Press, 1987.
[5]
K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley Publishing Company, Inc., Reading, Massachusetts, 1988.
[6]
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. F. Quesada. Maude: Specification and programming in rewriting logic. Theoretical Computer Science, 2001.
[7]
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. L. Talcott. All About Maude - A High-Performance Logical Framework, volume 4350 of Lecture Notes in Computer Science. Springer, 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]
J. Edmund M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999.
[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]
K. V. Hindriks, F. S. de Boer, W. van der Hoek, and J.-J. C. Meyer. Agent programming in 3apl. Autonomous Agents and Multi-Agent Systems, 2(4):357--401, 1999.
[12]
Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York, NY, USA, 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. B. van Riemsdijk, F. S. de Boer, M. Dastani, and J.-J. C. Meyer. Prototyping 3apl in the maude term rewriting language. In AAMAS '06: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, pages 1279--1281, New York, NY, USA, 2006. ACM Press.
[17]
A. Verdejo and N. Martí-Oliet. Two case studies of semantics execution in maude: Ccs and lotos. Form. Methods Syst. Des., 27(1/2):113--172, 2005.

Cited By

View all
  • (2010)Commitment-based protocols with behavioral rules and correctness properties of MASProceedings of the 8th international conference on Declarative agent languages and technologies VIII10.5555/1996758.1996764(60-77)Online publication date: 10-May-2010
  • (2009)On coordination, autonomy and timeProceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 210.5555/1558109.1558292(1357-1358)Online publication date: 10-May-2009
  • (2009)Choice, interoperability, and conformance in interaction protocols and service choreographiesProceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 210.5555/1558109.1558129(843-850)Online publication date: 10-May-2009
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
AAMAS '08: Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 2
May 2008
673 pages
ISBN:9780981738116

Sponsors

In-Cooperation

Publisher

International Foundation for Autonomous Agents and Multiagent Systems

Richland, SC

Publication History

Published: 12 May 2008

Check for updates

Author Tags

  1. BDI
  2. non-determinism
  3. refinement
  4. rewriting
  5. simulation

Qualifiers

  • Research-article

Conference

AAMAS08
Sponsor:

Acceptance Rates

Overall Acceptance Rate 1,155 of 5,036 submissions, 23%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2010)Commitment-based protocols with behavioral rules and correctness properties of MASProceedings of the 8th international conference on Declarative agent languages and technologies VIII10.5555/1996758.1996764(60-77)Online publication date: 10-May-2010
  • (2009)On coordination, autonomy and timeProceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 210.5555/1558109.1558292(1357-1358)Online publication date: 10-May-2009
  • (2009)Choice, interoperability, and conformance in interaction protocols and service choreographiesProceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 210.5555/1558109.1558129(843-850)Online publication date: 10-May-2009
  • (2009)Using rewrite strategies for testing BUpL agentsProceedings of the 19th international conference on Logic-Based Program Synthesis and Transformation10.1007/978-3-642-12592-8_11(143-157)Online publication date: 1-Sep-2009
  • (2009)The refinement of choreographed multi-agent systemsProceedings of the 7th international conference on Declarative Agent Languages and Technologies10.1007/978-3-642-11355-0_2(20-34)Online publication date: 11-May-2009
  • (2009)An Empirical Study of Agent ProgramsProceedings of the 12th International Conference on Principles of Practice in Multi-Agent Systems10.1007/978-3-642-11161-7_14(200-215)Online publication date: 15-Dec-2009

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media