Abstract
When designing multi-agent systems, it is often hard to guarantee that the specification of a system that has been designed 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 will have 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, it is a recent trend in the literature on verification in general to study the use of compositionality and abstraction to structure the process of verification; for example, see [Abadi and Lamport, 1993], [Hooman, 1994], [Dams et al., 1996].
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.
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.
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.), 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, 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. Principles of compositional multi-agent system design. In Proceedngs of the 15th IFIP World Computer Congress, WCC 98, subconference IT & KNOWS, J. Cuena (ed.), 1998. IOS Press, 1999.
F.M.T. Brazier, J. Treur, N.J.E. Wijngaards and M. Willems. Temporal semantics of compositional task models nd problem solving methods. Data and Knowledge Engineering,29(1), 17–42,1999.
F. Comelissen, C.M. Jonker and J. Treur. Compositional verification of knowledge-based systems: a case study in diagnostic reasoning. In: E.Plaza, R. Benjamins (eds.), Knowledge Acquisition, Modelling and Management, Proc. of the 10th EKAW,Lecture Notes in AI,1319,Springer Verlag, 65–80, 1997. See also this volume.
D. Dams, R. Gerth and P. Kelb. Practical Symbolic Model Checking of the full p-calculus using Compositional Abstractions. Report, Eindhoven University of Technology, Department of Mathematics and Computer Science.
J. Engelfriet, C.M. Jonker and J. Treur. Compositional Verification of Multiagent Systems in Temporal Epistemic Logic. Journal of Logic, Language and Information,to appear, 2001.
D. Fensel. Assumptions and limitations of a problem solving method: a case study. In: B.R. Gaines, M.A. Musen (eds.), Proceedings of the 9th Banff Knowledge Acquisition for Knowledge-based Systems workshop, KAW’95, Calgary: SRDG Publications, Department of Computer Science, University of Calgary, 1995.
D. Fensel and R. Benjamins. Assumptions in model-based diagnosis. In: B.R. Gaines, 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, 5/1–5/18, 1996.
Fensel et al.,1996] D. Fensel, A. Schonegge, R. Groenboom and B. Wielinga. Specification and verification of knowledge-based systems. In: B.R. Gaines, 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.
F. van Harmelen and D. Fensel. Formal Methods in Knowledge Engineering. Knowledge Engineering Review, 10 (4), 1995.
J. Hooman. Compositional Verification of a Distributed Real-Time Arbitration Protocol. Real-Time Systems, 6, 173–206, 1994.
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, 1994.
I.A. van Langevelde, A. Philipsen and J. Treur. Formal Specification of Compositional Architectures. In B. Neumann (ed.), Proceedings of the 10th European Conference on Al, ECAI’92,Wiley and Sons, 272–276, 1992.
[Leemans et al.,1993] P.Leemans, J. Treur and M. Willems. On the verification of knowledge-based reasoning modules, Report IR-346, Department of Mathematics & Computer Science, AI Group, Vrije Universiteit Amsterdam, 1993.
A.S. Rao and M.P. Georgeff. Modeling rational agents within a BDI architecture. In: R. Fikes and E. Sandewall (eds.), Proceedings of the Second Conference on Knowledge Representation and Reasoning, Morgan Kaufman, 473–484, 1991.
J. Treur and M. Willems. A logical foundation for verification. In: Proceedings of the 11th European Conference on AI, ECA’94, A. Cohn (ed.), John Wiley & Sons, Ltd., 745–749, 1994.
M. Wooldridge and N.R. Jennings (eds.). Intelligent Agents. Proceedings of the First International Workshop on Agent Theories, Architectures and Languages. Lecture Notes in AI, 890, Springer Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Jonker, C.M., Treur, J. (2001). A Formal Analysis of Pro-Activeness and Reactiveness in Cooperative Information Gathering. In: Meyer, JJ.C., Treur, J. (eds) Dynamics and Management of Reasoning Processes. Handbook of Defeasible Reasoning and Uncertainty Management Systems, vol 6. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1743-4_15
Download citation
DOI: https://doi.org/10.1007/978-94-017-1743-4_15
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5903-1
Online ISBN: 978-94-017-1743-4
eBook Packages: Springer Book Archive