Abstract
When designing multi-agent systems, it is often difficult to guarantee that the specification of a system actually fulfils the needs, i.e., whether it satisfies the design requirements. Especially for critical applications, for example in real-time domains, there is a need to prove that the designed system has certain properties under certain conditions (assumptions). While developing a proof of such properties, the assumptions that define the bounds within which the system will function properly, are generated. For nontrivial examples, verification can be a very complex process, both in the conceptual and computational sense. For these reasons, a recent trend in the literature on verification is to exploit compositionality and abstraction to structure the process of verification; cf. [Abadi and Lamport, 1993], [Hooman, 1997], [Jonker and Treur, 1998].
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.
Bibliography
M. Abadi and L. Lamport. Composing Specifications. ACM Transactions on Programming Languages and Systems, 15(1), 73–132, 1993.
H. Akkermans, F. Ygge and R. Gustaysson. HOMEBOTS: Intelligent Decentralized Services for Energy Management. In: Proceedings of the Fourth International Symposium on the Management of Industrial and Corporate Knowledge, ISMICK’96, 1996.
R. Benjamins, D. Fensel and R. Straatman. Assumptions of problem-solving methods and their role in knowledge engineering. In: W. Wahlster (ed.), Proceedings of the 12th European Conference on AI, ECAI’96, John Wiley and Sons, 408–412, 1996.
Brazier et al.,1998] F.M.T. Brazier, F. Cornelissen, R. Gustaysson, C.M. Jonker, O. Lindeberg, B. Polak and J. Treur. Agents Negotiating for Load Balancing of Electricity Use. In: M.P. Papazoglou, M. Takizawa, B. Krämer and S. Chanson (eds.), Proceedings of the 18th International Conference on Distributed Computing Systems, ICDCS’98,IEEE Computer Society Press, 622–629, 1998.
F.M.T. Brazier, B. Dunin-Keplicz, N.R. Jennings and J. Treur. Formal specification of Multi-Agent Systems: a real-world case. In: V. Lesser (ed.), Proc tasks. In: B.R. Gaines and M.A. Musen (eds.), Proceedings of the First International Conference on Multi-Agent Systems, ICMAS’95, MIT Press, Cambridge, MA, 25–32, 1995. Extended version in: International Journal of Cooperative Information Systems, M. Huhns and M. Singh, (eds.), special issue on Formal Methods in Cooperative Information Systems: Multi-Agent Systems, 6, 67–94, 1997.
F.M.T. Brazier, J. Treur, N.J.E. Wijngaards and M. Willems. Temporal semantics of compositional task models and problem solving methods. Data and Knowledge Engineering, 29 (1), 17–42, 1999.
J. Engelfriet, C.M. Jonker and J. Treur. Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic. In: J.P. Mueller, M.P. Singh and A.S. Rao (eds.), Proceedings of the Fifth International Workshop on Agent Theories, Architectures and Languages, ATAL’98, pp. 177–194. Lecture Notes in AI, Vol. 1555, Springer Verlag, 1999.
D. Fensel, A. Schonegge, R. Groenboom and B. Wielinga. Specification and verification of knowledge-based systems. In: B.R. Gaines and M.A. Musen (eds.), Proceedings of the 10th Banff Knowledge Acquisition for Knowledge-based Systems workshop, KAW’96, Calgary: SRDG Publications, Department of Computer Science, University of Calgary, 4/1–4/20, 1996.
M. Fisher and M. Wooldridge. On the Formal Specification and Verification of Multi-Agent Systems. International Journal of Cooperative Information Systems, M. Huhns, M. Singh, (eds.), special issue on Formal Methods in Cooperative Information Systems: Multi-Agent Systems, 6, 67–94, 1997.
R. Gustaysson. Requirements on Information Systems as Business Enablers. Invited paper. In Proceedings of DA/DSM Europe DistribuTECH’97, PennWell, 1997.
J. Hooman. Compositional Verification of a Distributed Real-Time Arbitration Protocol. Real-Time Systems, 6, 173–206, 1997.
C.M. Jonker and J. Treur. Compositional Verification of Multi-Agent Systems: a Formal Analysis of Pro-activeness and Reactiveness. In: W.P. de Roever, H. Langmaack and A. Pnueli (eds.), Proceedings of the International Workshop on Compositionality, COMPOS’97. Lecture Notes in Computer Science, 1536, Springer Verlag, 350–380, 1998.
Kinny et al.,1996] D. Kinny, M.P. Georgeff and A.S. Rao. A Methodology and Technique for Systems of BDI Agents. In: W. van der Velde, J.W. Perram (eds.), Agents Breaking Away, Proceedings 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World, MAAMAW’96,Lecture Notes in AI,1038 Springer Verlag, 56–71, 1996.
J.S. Rosenschein and G. Zlotkin. Rules of Encounter: Designing Conventions for Automated Negotiation among Computers, MIT Press, 1994.
J.S. Rosenschein and G. Zlotkin. Designing Conventions for Automated Negotiation. In: AI Magazine, 15(3), 29–46, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Brazier, F.M.T. et al. (2002). Compositional Verification of a Multi-Agent System for One-to-Many Negotiation. In: Meyer, JJ.C., Treur, J. (eds) Agent-Based Defeasible Control in Dynamic Environments. Handbook of Defeasible Reasoning and Uncertainty Management Systems, vol 7. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1741-0_18
Download citation
DOI: https://doi.org/10.1007/978-94-017-1741-0_18
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6109-6
Online ISBN: 978-94-017-1741-0
eBook Packages: Springer Book Archive