Abstract
We describe a framework for the automated verification of multi-agent systems which do distributed problem solving, e.g. query answering. Each reasoner uses facts, messages and Horn clause rules to derive new information. We show how to verify correctness of distributed problem solving under resource constraints, such as the time required to answer queries and the number of messages exchanged by the agents. The framework allows the use of abstract specifications consisting of Linear Time Temporal Logic (LTL) formulas to specify some of the agents in the system. We illustrate the use of the framework on a simple example.
This work was supported by the UK Engineering and Physical Sciences Research Council [grant EP/E031226/1].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bordini, R.H., Hübner, J.F., Vieira, R.: Jason and the Golden Fleece of agent-oriented programming. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.) Multi-Agent Programming: Languages, Platforms and Applications. Springer, Heidelberg (2005)
Bordini, R., Fisher, M., Visser, W., Wooldridge, M.: State-space reduction techniques in agent verification. In: Jennings, N.R., Sierra, C., Sonenberg, L., Tambe, M. (eds.) Proceedings of the Third International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2004), pp. 896–903. ACM Press, New York (2004)
Adjiman, P., Chatalic, P., Goasdoué, F., Rousset, M.C., Simon, L.: Distributed reasoning in a peer-to-peer setting. In: López de Mántaras, R., Saitta, L. (eds.) Proceedings of the Sixteenth European Conference on Artificial Intelligence (ECAI 2004), Valencia, Spain, pp. 945–946. IOS Press, Amsterdam (2004)
Claßen, J., Eyerich, P., Lakemeyer, G., Nebel, B.: Towards an integration of Golog and planning. In: Proceedings of the 20th International Joint Conference on Artifical Intelligence (IJCAI 2007), pp. 1846–1851. Morgan Kaufmann Publishers Inc., San Francisco (2007)
Alechina, N., Jago, M., Logan, B.: Modal logics for communicating rule-based agents. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P. (eds.) Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006), pp. 322–326. IOS Press, Amsterdam (2006)
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Hirtle, D., Boley, H., Grosof, B., Kifer, M., Sintek, M., Tabet, S., Wagner, G.: Schema Specification of RuleML 0.91 (2006), http://ruleml.org/0.91/
Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of maude. Electr. Notes Theor. Comput. Sci. 4 (1996)
Alechina, N., Logan, B., Nga, N.H., Rakib, A.: Verifying time and communication costs of rule-based reasoners. In: Peled, D., Wooldridge, M. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 1–14. Springer, Heidelberg (2009)
Holzmann, G.J.: On-the-fly model checking. ACM Computing Surveys 28(4) (1996)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Proceedings of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 342–354 (1992)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)
Culbert., C.: CLIPS reference manual. NASA (2007)
Friedman-Hill., E.J.: Jess, The Rule Engine for the Java Platform. Sandia National Laboratories (2008)
Tzafestas, S., Ata-Doss, S., Papakonstantinou, G.: Knowledge-Base System Diagnosis, Supervision and Control. Plenum Press, New York (1989)
Chen, J.R., Cheng, A.M.K.: Predicting the response time of OPS5-style production systems. In: Proceedings of the 11th Conference on Artificial Intelligence for Applications, p. 203. IEEE Computer Society, Los Alamitos (1995)
Cheng, A.M.K., yen Tsai, H.: A graph-based approach for timing analysis and refinement of OPS5 knowledge-based systems. IEEE Transactions on Knowledge and Data Engineering 16(2), 271–288 (2004)
Brodsky, A., Sagiv, Y.: On termination of Datalog programs. In: International Conference on Deductive and Object-Oriented Databases (DOOD), pp. 47–64 (1989)
Alpuente, M., Feliu, M.A., Joubert, C., Villanueva, A.: Defining datalog in rewriting logic. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 188–204. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alechina, N., Logan, B., Nguyen, H.N., Rakib, A. (2011). Automated Verification of Resource Requirements in Multi-Agent Systems Using Abstraction. In: van der Meyden, R., Smaus, JG. (eds) Model Checking and Artificial Intelligence. MoChArt 2010. Lecture Notes in Computer Science(), vol 6572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20674-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-20674-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20673-3
Online ISBN: 978-3-642-20674-0
eBook Packages: Computer ScienceComputer Science (R0)