Abstract
To make verification a manageable part of the system development process, comprehensibility and reusability of properties and proofs is essential. The work reported in this paper contributes formally founded methods that support proof structuring and reuse. Often occurring patterns in agent behaviour can be exploited to establish a library containing properties and proofs. This is illustrated here by verifying the class of single agents acting in dynamic environments. First, a notion of abstraction for properties and proofs is introduced that provides means to structure and clarify verification. Also, the paper contributes to establishing the library by proposing a reusable system of generic co-ordination properties for applications of agents acting in dynamic environments.
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
Brazier, F.M.T., Cornelissen, F., Gustavsson, R., Jonker, C. M., Lindeberg, O., Polak, B., and Treur, J., Compositional Design and Verification of a Multi-Agent System for One-to-Many Negotiation, in: Proceedings of the Third International Conference on Multi-Agent Systems, ICMAS’98, IEEE Computer Society Press, 1998, pp. 49–56.
Depke, R., Heckel, R., and Küster, J. M., Requirement Specification and Design of Agent-Based Systems with Graph Transformation, Roles and UML, in: this volume.
Engelfriet, J., Jonker, C.M., and Treur, J., Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic, in: Pre-proceedings of the Fifth International Workshop on Agent Theories, Architectures and Languages, ATAL’98 (J. P. Mueller, M. P. Singh, and A. S. Rao, eds.), 1998, pp. 91–106. To appear in:Intelligent Agents V (J.P. Mueller, M. P. Singh and A. S. Rao eds.), Lecture Notes in AI, Springer Verlag, in press,1999.
Ferber, J., Gutknecht, O., Jonker, C. M., Müller, J. P., and Treur, J., Organization Models and Behavioural Requirements Specification for Multi-Agent Systems, in: Proceedings of the Fourth International Conference on Multi-Agent Systems, ICMAS 2000, IEEE Computer Society Press, in press. Extended version in: Proceedings of the ECAI 2000 Workshop on Modelling Artificial Societies and Hybrid Organizations, in press, 2000.
Hodges, W., Model theory, Cambridge University Press, 1993.
Jonker, C.M., and Treur, J., Compositional Verification of Multi-Agent Systems: a Formal Analysis of Pro-activeness and Reactiveness, in: Proceedings of the International Workshop on Compositionality, COMPOS’97 (W.P. de Roever, H. Langmaack, A. Pnueli eds.), Lecture Notes in Computer Science, vol. 1536, Springer Verlag, 1998, pp. 350–380.
Jonker, C.M., Treur, J., and Vries, W. de, Compositional Verification of Agents in Dynamic Environments: a Case Study, in: Proceedings of the KR98 Workshop on Verification and Validation of KBS (F. van Harmelen ed.), 1998.
Kendall, E. A., Agent Software Engineering with Role Modelling, in: this volume.
McCarthy, J., and Hayes, P. J., Some Philosophical Problems from the Standpoint of Artificial Intelligence, Machine Intelligence, vol. 4, 1969, pp. 463–502.
Odell, J., Van Dyke Parunak, H., and Bauer, B., Representing Agent Interaction Protocols in UML, in: this volume.
Reiter, R., The Frame Problem in the Situation Calculus: a Simple Solution (Sometimes) and a Completeness Result for Goal Regression, in: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy (V. Lifschitz ed.), Academic Press, 1991, pp. 359–380.
Reiter, R., Proving Properties of States in the Situation Calculus, Artificial Intelligence, vol. 64, 1993, pp. 337–351.
Sandewall, E., Features and Fluents. The Representation of Knowledge about Dynamical Systems, Volume I, Oxford University Press, 1994.
Wood, M., and DeLoach, S. A., An Overview of the Multiagent Systems Engineering Methodology, in: this volume.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jonker, C.M., Treur, J., de Vries, W. (2001). Reuse and Abstraction in Verification: Agents Acting in Dynamic Environments. In: Ciancarini, P., Wooldridge, M.J. (eds) Agent-Oriented Software Engineering. AOSE 2000. Lecture Notes in Computer Science, vol 1957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44564-1_17
Download citation
DOI: https://doi.org/10.1007/3-540-44564-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41594-7
Online ISBN: 978-3-540-44564-7
eBook Packages: Springer Book Archive