Mike
Wooldridge
Department of Computer Science, University of Liverpool (UK)
Formal methods have a mixed reputation in mainstream computer science. On the one hand, the development of formal specification and verification methods has led to an improved understanding of the underlying theory of computing and programming, and has fed into the development of some programming languages and tools. On the other hand, attempts to promote formal methods as part of thew software development process have largely failed, and (it could be argued), have tended to widen the gulf of imcomprehension between those that do computing science and those that do computing. Against this background, this talk focusses on the role that formal methods, broadly construed, have played to date in the short history of multiagent systems. In particular, I discuss the potential roles of the various logics of agency that have been developed over the years. I review the way in which such logics might be used in the specification, implementation, and verification of agent systems, and highlight some problems associated with the current ``state of the art''. I conclude with pointing to some developments that I believe are promising, in particular the increasingly large body of work on logics of game-like encounters, and the focus on model checking as a paradigm for automatic verification.