Online research in philosophy

We here describe research into the formal specification and implementation of resource-bounded agents. In particular, we provide an overview of our work on incorporating resource limitations into executable agent specifications. In addition, we outline future directions, highlighting both their promise and their problems.

Syntactic logics do not suffer from the problems of logical omniscience but are often thought to lack interesting properties relating to epistemic notions. By focusing on the case of rule-based agents, I develop a framework for modelling resource-bounded agents and show that the resulting models have a number of interesting properties.

We propose a framework for modelling situated resource-bounded agents. The framework is based on an objective ascription of intentional modalities and can be easily tailored to the system we want to model and the properties we wish to specify. As an elaboration of the framework, we introduce a logic, OBA, for describing the observations, beliefs, goals and actions of simple agents, and show that OBA is complete, decidable and has an efficient model checking procedure, allowing properties of agents specified in OBA to be verified using standard theorem proving or model checking techniques.

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as "Alternating-time Temporal Logic" (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by "cooperation modalities", of the form $\langle \langle \Gamma \rangle \rangle $ , where Γ is a set of agents. The intended interpretation of an ATL formula $\langle \langle \Gamma \rangle \rangle \varphi $ is that the agents Γ can cooperate to ensure that φ holds (equivalently, that Γ have a winning strategy for φ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as "group Γ can cooperate to bring about φ iff it is common knowledge in Γ that ψ". The resulting logic -- Alternating-time Temporal Epistemic Logic (ATEL) -- shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems.

If we express our knowledge in sentences, we will find that these sentences are linked in complex patterns governed by our observations and our inferences from these observations. These inferences are to a large extent driven by logical rules. We ask whether the structure logic imposes on our knowledge restricts what we forget and what we remember. The model is a two period S5 logic. In this logic, we propose a memory loss operator: the agent forgets a sentence pif and only if he knows pat time 1 and he does not know pat time 2. Equipped with the operator, we prove theorems on the relation between knowledge and memory loss. The main results point to classes of formulas that an agent cannot forget, and classes of formulas he must forget. A desirable feature is that most results hold in the S4 logic. The results illustrate bounds to memory loss, and thus to bounded rationality. We apply the model to single-agent conventions: conventions made between an agent and himself.

We characterize the collapse of Buss' bounded arithmetic in terms of the provable collapse of the polynomial time hierarchy. We include also some general model-theoretical investigations on fragments of bounded arithmetic.

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems.

We present a framework for verifying systems composed of heterogeneous reasoning agents, in which each agent may have differing knowledge and inferential capabilities, and where the resources each agent is prepared to commit to a goal (time, memory and communication bandwidth) are bounded. The framework allows us to investigate, for example, whether a goal can be achieved if a particular agent, perhaps possessing key information or inferential capabilities, is unable (or unwilling) to contribute more than a given portion of its available computational resources or bandwidth to the problem. We present a novel temporal epistemic logic, BMCL-CTL , which allows us to describe a set of reasoning agents with bounds on time, memory and the number of messages they can exchange. The bounds on memory and communication are expressed as axioms in the logic. As an example, we show how to axiomatise a system of agents which reason using resolution and prove that the resulting logic is sound and complete. We then show how to encode a simple system of reasoning agents specified in BMCL-CTL in the description language of the Mocha model checker (Alur et al., Proceedings of the tenth international conference on computer-aided verification (CAV) , 1998), and verify that the agents can achieve a goal only if they are prepared to commit certain time, memory and communication resources.

There exists a considerable body of work on epistemic logics for resource-bounded reasoners. In this paper, we concentrate on a less studied aspect of resource-bounded reasoning, namely, on the ascription of beliefs and inference rules by the agents to each other. We present a formal model of a system of bounded reasoners which reason about each other’s beliefs, and investigate the problem of belief ascription in a resource-bounded setting. We show that for agents whose computational resources and memory are bounded, correct ascription of beliefs cannot be guaranteed, even in the limit. We propose a solution to the problem of correct belief ascription for feasible agents which involves ascribing reasoning strategies , or preferences on formulas, to other agents, and show that if a resource-bounded agent knows the reasoning strategy of another agent, then its ascription of beliefs to the other agent is correct in the limit.

Alternating-time temporal logic (ATL) is a branching time temporal logic in which statements about what coalitions of agents can achieve by strategic cooperation can be expressed. Alternating-time temporal epistemic logic (ATEL) extends ATL by adding knowledge modalities, with the usual possible worlds interpretation. This paper investigates how properties of agents’ actions can be expressed in ATL in general, and how properties of the interaction between action and knowledge can be expressed in ATEL in particular. One commonly discussed property is that an agent should know about all available actions, i.e., that the same actions should be available in indiscernible states. Van der Hoek and Wooldridge suggest a syntactic expression of this semantic property. This paper shows that this correspondence in fact does not hold. Furthermore, it is shown that the semantic property is not expressible in ATEL at all. In order to be able to express common and interesting properties of action in general and of the interaction between action and knowledge in particular, a generalization of the coalition modalities of ATL is proposed. The resulting logics, ATL-A and ATEL-A, have increased expressiveness without loosing ATL’s and ATEL’s tractability of model checking.