Reuse and Abstraction in Verification: Agents Acting in Dynamic Environments
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.
Unable to display preview. Download preview PDF.
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Hodges, W., Model theory, Cambridge University Press, 1993.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Kendall, E. A., Agent Software Engineering with Role Modelling, in: this volume.Google Scholar
- McCarthy, J., and Hayes, P. J., Some Philosophical Problems from the Standpoint of Artificial Intelligence, Machine Intelligence, vol. 4, 1969, pp. 463–502.Google Scholar
- Odell, J., Van Dyke Parunak, H., and Bauer, B., Representing Agent Interaction Protocols in UML, in: this volume.Google Scholar
- 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.Google Scholar
- Sandewall, E., Features and Fluents. The Representation of Knowledge about Dynamical Systems, Volume I, Oxford University Press, 1994.Google Scholar
- Wood, M., and DeLoach, S. A., An Overview of the Multiagent Systems Engineering Methodology, in: this volume.Google Scholar