We present a process-algebraic approach to situated multi-agent systems which incorporates syntax for agent systems as well as for the environments (workspaces) they live in. Agent states are characterized by (1) a belief state, (2) a goal (desire, need) state and (3) a capabilities state. Capabilities are determined by a subspace of the workspace the agent lives in, and they are represented in the agent state as a collection of types of objects (tools, in the agent's workspace) the agent has the expertise (or permission) to use. Action capabilities are then just permissible transformations of workspaces, restricted to the particular capabilities space of the agent. Workspaces (certain kinds of collections of objects, modelled here as simply typed records of labelled attributes) and workspace transformations (record update operations) are structured into a transition system. We use a simple model of objects as records and, therefore, of workspaces and thus we only deal in this report with deterministic environments. Transitions are determined by agent actions (modifications of properties of objects in their capabilities space, modelled as record update operations), thus allowing for a formal account of agent systems living in an ever changing environment. Beliefs and desires are formulae of a many-sorted, first-order multi-modal language of properties of workspaces, where sorts are object types and modalities are indexed by workspace transformations (record updates). The logical language is kept simple, allowing only for first-order beliefs (beliefs about properties of workspaces).We present a language of situated, cooperative, self-interested agent systems, proposing a basic collection of agent behaviors (including ground observation actions, commitments, communication via assertions and requests, recursive behaviors, choice, concurrent behaviors etc), we provide an operational semantics for this language and discuss some examples of useful definable agent behaviors, such as perceiving (performing observations triggered by a statement). We then present and discuss notions of (behavioral) agent preorder and equivalence relations. Using the operational semantics and our notion of behavioral preorder and equivalence we propose an inequational theory for reasoning about agents. We conclude with presenting and discussing a case study for a simple agent system
