research-article

Verifying time, memory and communication bounds in systems of reasoning agents

Authors:

Natasha Alechina,

Nguyen Hoang Nga,

Abdur RakibAuthors Info & Claims

AAMAS '08: Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 2

Pages 736 - 743

Published: 12 May 2008 Publication History

Abstract

We present a framework for verifying systems composed of heterogeneous reasoning agents, in which each agent may have differing knowledge and inferential capabilities, and where the resources each agent is prepared to commit to a goal (time, memory and communication bandwidth) are bounded. The framework allows us to investigate, for example, whether a goal can be achieved if a particular agent, perhaps possessing key information or inferential capabilities, is unable (or unwilling) to contribute more than a given portion of its available computational resources or bandwidth to the problem. We present a novel temporal epistemic logic, BMCL, which allows us to describe a set of reasoning agents with bounds on time, memory and the number of messages they can exchange. The bounds on memory and communication are expressed as axioms in the logic. As an example, we show how to axiomatize a system of agents which reason using resolution and prove that the resulting logic is sound and complete. We then show how to encode a simple system of reasoning agents specified in BMCL in the description language of a model checker, and verify that the agents can achieve a goal only if they are prepared to commit certain time, memory and communication resources.

References

[1]

P. Adjiman, P. Chatalic, F. Goasdoué, M.-C. Rousset, and L. Simon. Distributed reasoning in a peer-to-peer setting. In Proc. of the 16th European Conference on Artificial Intelligence, ECAI'2004, pages 945--946. IOS Press, 2004.

[2]

T. Ågotnes and N. Alechina. Knowing minimum/maximum n formulae. In Proc. of the 17th European Conference on Artificial Intelligence (ECAI 2006), pages 317--321. IOS Press, 2006.

Digital Library

[3]

T. Ågotnes and M. Walicki. Strongly complete axiomatizations of "knowing at most" in standard syntactic assignments. In Pre-proceedings of the 6^th International Workshop on Computational Logic in Multi-agent Systems (CLIMA VI), 2005.

Digital Library

[4]

A. Albore, N. Alechina, P. Bertoli, C. Ghidini, B. Logan, and L. Serafini. Model-checking memory requirements of resource-bounded reasoners. In Proc. of the Twenty-First National Conference on Artificial Intelligence (AAAI 2006), pages 213--218. AAAI Press, 2006.

Digital Library

[5]

N. Alechina, P. Bertoli, C. Ghidini, M. Jago, B. Logan, and L. Serafini. Verifying space and time requirements for resource-bounded age nts. In Proc. of the Fifth International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2006), pages 217--219. IEEE Press, 2006.

Digital Library

[6]

N. Alechina, P. Bertoli, C. Ghidini, M. Jago, B. Logan, and L. Serafini. Verifying space and time requirements for resource-bounded agents. In Proc. of the Fourth Workshop on Model Checking and Artificial Intelligence (MoChArt-2006), pages 16--30, 2006.

Digital Library

[7]

N. Alechina, M. Jago, and B. Logan. Modal logics for communicating rule-based agents. In Proc. of the 17th European Conference on Artificial Intelligence (ECAI 2006), pages 322--326. IOS Press, 2006.

Digital Library

[8]

N. Alechina, B. Logan, and M. Whitsey. A complete and decidable logic for resource-bounded agents. In Proc. of the Third International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2004), pages 606--613. ACM Press, 2004.

Digital Library

[9]

M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson. Space complexity in propositional calculus. SIAM J. of Computing, 31(4):1184--1211, 2002.

Digital Library

[10]

R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Computer Aided Verification, pages 521--525, 1998.

Digital Library

[11]

E. Amir and S. A. McIlraith. Partition-based logical reasoning for first-order and propositional theories. Artificial Intelligence, 162(1--2):49--88, 2005.

Digital Library

[12]

M. Benerecetti, F. Giunchiglia, and L. Serafini. Model checking multiagent systems. J. Log. Comput., 8(3):401--423, 1998.

[13]

R. Bordini, M. Fisher, W. Visser, and M. Wooldridge. State-space reduction techniques in agent verification. In Proc. of the Third International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-2004), pages 896--903. ACM Press, 2004.

Digital Library

[14]

H. Duc. Reasoning about rational, but not logically omniscient, agents. J. Log. Comput., 5:633--648, 1997.

[15]

J. J. Elgot-Drapkin and D. Perlis. Reasoning situated in time I: Basic concepts. J. of Experimental and Theoretical Artificial Intelligence, 2:75--98, 1990.

Digital Library

[16]

J. L. Esteban and J. Torán. Space bounds for resolution. In Proc. STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, pages 551--560. Springer, 1999.

Digital Library

[17]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, Mass., 1995.

Digital Library

[18]

B. Faltings and M. Yokoo. Introduction: Special issue on distributed constraint satisfaction. Artif. Intell., 161(1--2):1--5, 2005.

Digital Library

[19]

M. Fisher and C. Ghidini. Programming Resource-Bounded Deliberative Agents. In Proc. of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99), pages 200--206. Morgan Kaufmann, 1999.

Digital Library

[20]

J. Grant, S. Kraus, and D. Perlis. A logic for characterizing multiple bounded agents. Autonomous Agents and Multi-Agent Systems, 3(4):351--387, 2000.

Digital Library

[21]

J. Y. Halpern, Y. Moses, and M. Y. Vardi. Algorithmic knowledge. In Proc. of the 5th Conference on Theoretical Aspects of Reasoning about Knowledge, pages 255--266. Morgan Kaufmann, 1994.

Digital Library

[22]

M. Jago. Logics for Resource-Bounded Agents. PhD thesis, University of Nottingham, 2006.

[23]

H. Jung and M. Tambe. On communication in solving distributed constraint satisfaction problems. In Multi-Agent Systems and Applications IV, Proc. 4th International Central and Eastern European Conference on Multi-Agent Systems, CEEMAS 2005, pages 418--429. Springer, 2005.

Digital Library

[24]

K. Konolige. A Deduction Model of Belief. Morgan Kaufmann, San Francisco, Calif., 1986.

Digital Library

[25]

G. M. Provan. A model-based diagnosis framework for distributed embedded systems. In Proc. of the Eighth International Conference on Principles and Knowledge Representation and Reasoning (KR-02), pages 341--352. Morgan Kaufmann, 2002.

Digital Library

[26]

R. Pucella. Deductive algorithmic knowledge. In AI&M 1-2004, Eighth International Symposium on Artificial Intelligence and Mathematics, 2004.

[27]

M. Reynolds. An axiomatization of PCTL*. Inf. Comput., 201(1):72--119, 2005.

Digital Library

[28]

M. Wooldridge and P. E. Dunne. On the computational complexity of coalitional resource games. Artif. Intell., 170(10):835--871, 2006.

Digital Library

[29]

A. C.-C. Yao. Some complexity questions related to distributive computing (preliminary report). In Conference Record of the Eleventh Annual ACM Symposium on Theory of Computing, pages 209--213. ACM, 1979.

Digital Library

Cited By

Bulling NFarwer B(2009)Expressing properties of resource-bounded systemsProceedings of the 10th international conference on Computational logic in multi-agent systems10.5555/1927368.1927370(22-45)Online publication date: 9-Sep-2009
https://dl.acm.org/doi/10.5555/1927368.1927370
Alechina NLogan BNga NRakib A(2009)A logic for coalitions with bounded resourcesProceedings of the 21st International Joint Conference on Artificial Intelligence10.5555/1661445.1661550(659-664)Online publication date: 11-Jul-2009
https://dl.acm.org/doi/10.5555/1661445.1661550

Index Terms

Verifying time, memory and communication bounds in systems of reasoning agents
1. Computing methodologies
  1. Artificial intelligence
    1. Philosophical/theoretical foundations of artificial intelligence
2. Theory of computation
  1. Logic
  2. Semantics and reasoning

Recommendations

Ascribing beliefs to resource bounded agents
AAMAS '02: Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2

Logical approaches to reasoning about agents often rely on idealisations about belief ascription and logical omniscience which make it difficult to apply the results obtained to real agents. In this paper, we show how to ascribe beliefs and an ability ...
Reasoning about time-dependent multi-agents: foundations of theorem proving and model checking
Transactions on Compuational Collective Intelligence VI

Firstly, an extension of linear-time temporal logic (LTL), called an agents-indexed linear-time temporal logic (ALTL), is introduced as a Gentzen-type sequent calculus. ALTL is intended to appropriately express reasoning about time-dependent multi-...
Reasoning about agent execution strategies
AAMAS '08: Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 3

We present a logic for reasoning about properties of agent programs under different agent execution strategies. Using the agent programming language SimpleAPL as an example, we show how safety and liveness properties can be expressed by translating ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

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

ACM: Association for Computing Machinery
AAAI: Association for the Advancement of Artifical Intelligence

In-Cooperation

SIGAI: ACM Special Interest Group on Artificial Intelligence

Publisher

International Foundation for Autonomous Agents and Multiagent Systems

Richland, SC

Publication History

Published: 12 May 2008

Check for updates

Author Tag

formalisms and logics

Qualifiers

Research-article

Conference

AAMAS08

Sponsor:

ACM
AAAI

AAMAS08: 7th International Conference on Autonomous Agents and Multi Agent Systems

May 12 - 16, 2008

Estoril, Portugal

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
125
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bulling NFarwer B(2009)Expressing properties of resource-bounded systemsProceedings of the 10th international conference on Computational logic in multi-agent systems10.5555/1927368.1927370(22-45)Online publication date: 9-Sep-2009
https://dl.acm.org/doi/10.5555/1927368.1927370
Alechina NLogan BNga NRakib A(2009)A logic for coalitions with bounded resourcesProceedings of the 21st International Joint Conference on Artificial Intelligence10.5555/1661445.1661550(659-664)Online publication date: 11-Jul-2009
https://dl.acm.org/doi/10.5555/1661445.1661550

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents