Further particulars for the post of:
Research Associate in Computer Science (Formal Methods and Automated Reasoning)

"Proof Methods for Multi-Agent Systems" Project
Department of Computer Science
University of Manchester

The Post

The successful candidate will undertake a three year project to investigate and develop "Proof Methods for Multi-Agent Systems", carrying out, publicising and disseminating high quality research.

Project environment

The work will take place within the Formal Methods Research Group in the Department of Computer Science at the University of Manchester, under the supervision of Dr Renate Schmidt, who is an expert on automated proof methods, resolution decision procedures, solvable first-order fragments, non-classical logics and relation algebras. Co-investigators in this project are Prof. Michael Fisher, who has an international reputation in logic, agent-based systems and programming languages, and Dr Clare Dixon, who has an international reputation in temporal reasoning, automated theorem-proving, and verification; both are from the Centre for Agent Research and Development at the Manchester Metropolitan University.

Person specification

The Project

Background

Agent-Based Systems is widely recognised as an area of rapidly increasing importance [14, 13]. Agents provide a key abstraction within modern development of AI systems and software. Although there exist powerful theoretical models of agency [10, 11, the techniques for solving the reasoning problem within these theories have not been investigated sufficiently and proof systems have not been applied in practical agent systems. This project aims to apply the know-how and tools established and produced in previous work to develop proof methods for the expressive combinations of diverse logics used in agent theories, and apply these to particular examples from agent-based systems.

A multi-agent system is a collection of semi-autonomous processes known as `agents' which live in dynamic and unpredictable environments. Agents continuously interact which each other and the environment and need to reason about their own and other agent's attitudes. A number of theoretical frameworks specifying agent-based systems have been proposed, for example, the BDI model being developed at AAII in Australia [17], 18], the powerful KARO framework being developed at Utrecht University [20], temporal logics of knowledge and belief [4, 5, 6], and also more recent developments in modal description logics [1, 21]. These theories are being used for the specification and formalisation of agent-based systems, yet the much needed techniques to analyse and manipulate such specifications, utilising symbolic information to determine appropriate behaviour, are only slowly beginning to emerge [15]. For example, tableaux for multi-modal belief or knowledge logics [5], tableaux for multi-modal belief or knowledge logics with linear-time temporal logic [23], tableaux for belief-desire-intention logics with either linear or branching-time temporal logics [17], and resolution for knowledge logics with linear-time temporal logics [2].

The key problem in addressing the reasoning problem within multi-agent systems is the inherent complexity of the agent scenarios. The logics introduced in existing specification frameworks usually incorporate combinations of multi-modal logics, temporal logics and first-order logic. The degree to which combinations of these are useful and manageable depends on the kind of interactions existing between the logics. These vary in kind and complexity in different systems. Although the basic properties of some of the individual logics are well-understood, less is known about different interactions, and very little work has been carried out on proof methods for such complex logics.

Aims and objectives

The long term goal of this work is to provide practical proof systems and automated reasoning tools for the development of multi-agent systems. Work in this project will focus on the reasoning problem for complex combinations of expressive modal logics, temporal logics and first-order logic as well as unconventional application-oriented logics which form the basis of common specification frameworks for modelling agent behaviour. Powerful proof techniques are now available and provide viable means for efficient and practical reasoning in a wide range of non-classical logics and first-order classes [3, 7, 8, 9, 10, 11, 12, 13, 16, 19]. The intention is to study to what extent these new methods can be utilised and enhanced for the development of feasible proof systems suitable to meet the reasoning needs of agent-based systems.

The principal objectives for this project are:

  1. The investigation of the computational properties of interactions common in multi-agent systems.
  2. The development, where possible, of terminating, automatic proof procedures.
  3. The identification of general principles correlating particular logics, clausal classes or their combinations, with particular techniques for guiding search during the computation.
  4. The investigation to which extent sound and complete proof procedures of single logics can be combined to form sound and complete proof procedures for the combination of these logics.

References

  1. Baader, F. and Ohlbach, H. J. (1995), A Multi-Dimensional Terminological Knowledge Representation Language. J. Appl. Non-Classical Logics 2 153-197.
  2. Dixon, C. and Fisher, M. and Wooldridge, M. (1998), Resolution for Temporal Logics of Knowledge. J. Logic Computat. 8 (3) 345-372.
  3. Ganzinger, H. and Hustadt, U. and Meyer, C. and Schmidt, R. A. (1999), A Resolution-Based Decision Procedure for Extensions of K4. To appear in Advances in Modal Logic, Vol. 2, CSLI Publ.,
  4. Fagin, R. and Halpern, J. Y. and Moses, Y. and Vardi, M. Y. (1995), Reasoning About Knowledge. MIT Press.
  5. Halpern, J. Y. and Moses, Y. (1992), A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief. Artif. Intell. 54 319-379.
  6. Halpern, J. Y. and Vardi, M. Y. (1989), The Complexity of Reasoning about Knowledge and Time. I Lower Bounds. J. Computer and System Sci. 38 195-237.
  7. Hustadt, U., Dixon, C., Schmidt, R. A. and Fisher, M. (2000), Normal Forms and Proofs in Combined Modal and Temporal Logics. Proc. FroCoS'2000. LNAI, Springer, To appear.
  8. Hustadt, U. and Schmidt, R. A. (1997), On Evaluating Decision Procedures for Modal Logics. Proc. IJCAI'97. 1 Morgan Kaufmann, 202-207.
  9. Hustadt, U. and Schmidt, R. A. (1998), Simplification and Backjumping in Modal Tableau. Proc. TABLEAUX'98. LNCS 1397 Springer, 187-201.
  10. Hustadt, U. and Schmidt, R. A. (1999), An Empirical Analysis of Modal Theorem Provers. J.\ Appl.\ Non-Classical Logics 9 (4) 479-522.
  11. Hustadt, U. and Schmidt, R. A. (1999), On the Relation of Resolution and Tableaux Proof Systems for Description Logics. In Proc. IJCAI'99. Morgan Kaufmann, 110-115.
  12. Hustadt, U. and Schmidt, R. A. (1999), Maslov's Class K Revisited. In Automated Deduction-CADE-16. LNAI 1632, Springer, 172-186.
  13. Hustadt, U. and Schmidt, R. A. (2000), Issues of Decidability for Description Logics in the Framework of Resolution. In Automated Deduction in Classical and Non-Classical Logics. LNAI 1761, Springer, 192-206.
  14. Jennings, N. R. and Wooldridge, M. (1998), Applications of Agent Technology. In Agent Technology: Foundations, Applications, and Markets. Springer.
  15. Ndumu, D. T. and Nwana, H. S. (1997), Research and Development Challenges for Agent-Based Systems. IEE Proc. Softw. Eng. 144 (1).
  16. Ohlbach, H. J. and Schmidt, R. A. (1997), Functional Translation and Second-Order Frame Properties of Modal Logics. J. Logic Computat. 7 (5) 581-603.
  17. Rao, A. S. (1996), Decision Procedures for Propositional Linear-Time Belief-Desire-Intention Logic. In Proc. ATAL'95. LNAI 1037, Springer, 102-118.
  18. Rao, A. S. and Georgeff, M. P. (1991), Modeling Rational Agents within a BDI-Architecture. In Proc. KR'91. Morgan Kaufmann, 473-484,
  19. Schmidt, R. A. (1999), Decidability by Resolution for Propositional Modal Logics. J. Automated Reasoning 22 (4) 379-396.
  20. Van Linder, B. and van der Hoek, W. and Meyer, J.-J. C. (1998), Formalizing Abilities and Opportunities of Agents. Fundameta Informaticae 34 (1, 2) 53-101.
  21. Wolter, F. and Zakharyaschev, M. (1998), Satisfiability Problem in Decsription Logics with Modal Operators. In Proc. KR-98. Morgan Kaufmann, 512-513.
  22. Wooldridge, M. (1998), Agent-Based Computing. Interoperable Comm. Networks 1 (1) 71-97.
  23. Wooldridge, M. and Dixon, C. and Fisher, M. (1998), A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief. J. Appl. Non-Classical Logics 8 (3) 225-258.

Advert | Further details | General Information for applicants

Renate A. Schmidt
Home | Publications | Tools | FM Group | Dept Computer Science | Man Univ

Last modified: 11 Feb 2000
Copyright © 2000 Renate A. Schmidt, Dept Computer Science, Man Univ, schmidt@cs.man.ac.uk