A logic for specifying and reasoning about cooperative environments

Abstract

In this paper we describe the current progress of an attempt to develop a logic which will allow us to specify required properties of systems which typically consist of a single interactive program being used, probably simultaneously, by several agents, usually people. The logic is a development of ideas from modal logic and their more recent developments to describe computation. Since modal logic (and its extensions) are still relatively new to most people we give introductions to these logics in this paper, assuming only a familiarity with classical first-order logic and some proof theory. We also give an account of some of the sorts of situations that we want to specify. Finally, we consider what work will be needed in the future, building on what we present here, in order to achieve our goal of providing a language in which to specify and reason about systems intended to support co-operative working.