Abstract
We present a framework for the automated verification of time and communication requirements in systems of distributed rule-based reasoning agents which allows us to determine how many rule-firing cycles are required to solve the problem, how many messages must be exchanged, and the trade-offs between the time and communication resources. We extend CTL* with belief and communication modalities to express bounds on the number of messages the agents can exchange. The resulting logic, \(\mathcal{L}_{CRB}\), can be used to express both bounds on time and on communication. We provide an axiomatisation of the logic and prove that it is sound and complete. Using a synthetic but realistic example system of rule-based reasoning agents which allows the size of the problem and the distribution of knowledge among the reasoners to be varied, we show the Mocha model checker [1] can be used to encode and verify properties of systems of distributed rule-based agents. We describe the encoding and report results of model checking experiments which show that even simple systems have rich patterns of trade-offs between time and communication bounds.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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)
Faltings, B., Yokoo, M.: Introduction: Special issue on distributed constraint satisfaction. Artificial Intelligence 161, 1–5 (2005)
Jung, H., Tambe, M.: On communication in solving distributed constraint satisfaction problems. In: Pěchouček, M., Petta, P., Varga, L.Z. (eds.) CEEMAS 2005. LNCS, vol. 3690, pp. 418–429. Springer, Heidelberg (2005)
Provan, G.M.: A model-based diagnosis framework for distributed embedded systems. In: Fensel, D., Giunchiglia, F., McGuinness, D.L., Williams, M.-A. (eds.) Proceedings of the 8th International Conference on Principles and Knowledge Representation and Reasoning (KR 2002), Toulouse, France, April 22-25, 2002, pp. 341–352. Morgan Kaufmann, San Francisco (2002)
Wooldridge, M., Dunne, P.E.: On the computational complexity of coalitional resource games. Artif. Intell. 170, 835–871 (2006)
Adjiman, P., Chatalic, P., Goasdoué, F., Rousset, M.-C., Simon, L.: Distributed reasoning in a peer-to-peer setting. In: de Mántaras, R.L., Saitta, L. (eds.) Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI 2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, August 22-27, 2004, pp. 945–946. IOS Press, Amsterdam (2004)
Amir, E., McIlraith, S.A.: Partition-based logical reasoning for first-order and propositional theories. Artificial Intelligence 162, 49–88 (2005)
Albore, A., Alechina, N., Bertoli, P., Ghidini, C., Logan, B., Serafini, L.: Model-checking memory requirements of resource-bounded reasoners. In: Proceedings of the Twenty-First National Conference on Artificial Intelligence (AAAI 2006), pp. 213–218. AAAI Press, Menlo Park (2006)
Alechina, N., Bertoli, P., Ghidini, C., Jago, M., Logan, B., Serafini, L.: Verifying space and time requirements for resource-bounded age nts. In: Stone, P., Weiss, G. (eds.) Proceedings of the Fifth International Joint Conference on Aut onomous Agents and Multi-Agent Systems (AAMAS 2006), Hakodate, Japan, pp. 217–219. IEEE Computer Society Press, Los Alamitos (2006)
Alechina, N., Bertoli, P., Ghidini, C., Jago, M., Logan, B., Serafini, L.: Verifying space and time requirements for resource-bounded agents. In: Edelkamp, S., Lomuscio, A. (eds.) Proceedings of the Fourth Workshop on Model Checking and Artificial Intelligence (MoChArt 2006), pp. 16–30 (2006)
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)
Alechina, N., Logan, B., Nga, N.H., Rakib, A.: Verifying time, memory and communication bounds in systems of reasoning agents. In: Padgham, Parkes, Muller, Parsons (eds.) Proceedings of the Seventh International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2008), Estoril, Portugal (May 2008)
Ågotnes, T., Alechina, N.: Knowing minimum/maximum n formulae. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P. (eds.) Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006), Riva del Garda, Italy, pp. 317–321. IOS Press, Amsterdam (2006)
Ågotnes, T., Alechina, N.: The dynamics of syntactic knowledge. Journal of Logic and Computation 17, 83–116 (2007)
Reynolds, M.: An axiomatization of full computation tree logic. J. Symb. Log. 66, 1011–1057 (2001)
Lomuscio, A., Raimondi, F.: Mcmas: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alechina, N., Logan, B., Nga, N.H., Rakib, A. (2009). Verifying Time and Communication Costs of Rule-Based Reasoners. In: Peled, D.A., Wooldridge, M.J. (eds) Model Checking and Artificial Intelligence. MoChArt 2008. Lecture Notes in Computer Science(), vol 5348. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00431-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-00431-5_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00430-8
Online ISBN: 978-3-642-00431-5
eBook Packages: Computer ScienceComputer Science (R0)