Computationally Grounded Model of BDI-Agents

1 Introduction

There are two main semantic approaches to formalizing agent systems via modal logics, the possible worlds semantics [Hintikka, 1962] and the interpreted system model [Fagin et al., 1995]. The �rst approach includes the well-known theory of intension [Cohen and Levesque, 1990] and the formalism of the belief-desire-intension paradigm [Rao and Georgeff, 1998]. The second approach, offers a natural interpretation, in terms of the states of computer processes, to S5 epistemic logic. The signi�cance of the second approach is that we are able to associate the system with a computer program, and formulas can be understood as properties of program computations. In this sense, the interpreted systemmodel is computationally grounded [Wooldridge, 2000].

There are few computationally grounded models for formalizing general BDI-agents. A number of researchers have attempted to develop executable agent languages such as AgentSpeak(L) [Rao, 1996], but these agent languages have comparatively simple semantics [van der Hoek and Wooldridge, 2003]. The aim of this paper is to present a computationally grounded model of general BDI-agents.

The main idea of our BDI-model is that we characterize an agent's belief, desire and intention as a set of runs (computing paths), which is exactly a system in the interpreted system model. Let Bi, Di and Ii be sets of runs related to the beliefs, desires and intentions of agent i, respectively. Then, runs in Bi are possible computing paths from the viewpoint of the agent; runs in Di are those computing paths that the agent desires; and runs in Ii are those computing paths with the agent's choices of the possible actions. Clearly, it is reasonable to assume that Di ⊆ Bi, that is, every desired computing path is a possible one, but we need not to assume that Ii ⊆ Di or even Ii ⊆ Bi because an agent's intention may fail to achieve its goal and the real computing path may be beyond the agent's belief even though the agent has chosen and completed an intentional series of actions.

The salient point of our work is that we present a general form of BDI agent programs, from which BDI-models can be generated and speci�cations in full BDI logics can be veri�ed by symbolic model checking techniques.

∗This work was supported by the Australian Research Council grant DP0452628, and partially by the NSFC grants 60496327, 10410638 and 60473004.

2 Computationally Grounded BDI Logic

We introduce a multimodal logic of belief, desire and intention, called OBDI logic, where the changes and computation of agents' beliefs, desires, and desires are based on agents' observations (i.e. local states). We assume the reader is familiar with the notion of interpreted system model, and we will follow the terminology of [Fagin et al., 1995].

2.1 Syntax

Given a set Φ of propositional atoms, the language of OBDI logic is de�ned by the following BNF notations:

Informally, Biϕ and Diϕ means that agent i believes and desires ϕ, respectively. While Iiϕ denotes that ϕ holds under the assumption that agent i acts based on his intention.

2.2 The BDI-systemModel

Given a set G of global states and a system K over G, an agent's mental state over system K is a tuple 〈B, D, I〉, where B, D and I are systems (sets of runs over G) such that I ⊆ K and D ⊆ B ⊆ K. A BDI-system is a structure 〈K,M1, · · · ,Mn〉, where K is a system and for every i, Mi is agent i's mental state over K.

Assume that we have a set Φ of primitive propositions. An interpreted BDI-system I consists of a pair (S, π), where S is a BDI-system and π is a valuation function, which gives the set of primitive propositions true at each point in G.

2.3 Semantics

In what follows, we inductively de�ne the satisfaction relation |=OBDI between a formula ϕ and a pair of interpreted BDI-system and a point. Given an interpreted BDI-system I = (S, π), suppose that S = 〈K,M1, · · · ,Mn〉 and for every i, Mi = 〈Bi, Di, Ii〉. Let r be a run in K and u a natural number, then we have that:

• (I, r, u) |=OBDI Biϕ iff (I, r′ , v) |=OBDI ϕ for those (r′ , v) ∈ Bi such that (r, u) ∼i (r′ , v);
• (I, r, u) |=OBDI Diϕ iff (I, r′ , v) |=OBDI ϕ for those (r′ , v) ∈ Di such that (r, u) ∼i (r′ , v);
• (I, r, u) |=OBDI Iiϕ iff (I, r′ , v) |=OBDI ϕ for those (r′ , v) ∈ Ii such that (r, u) ∼i (r′ , v);

Other cases are trivial and omitted here.

Proposition 1 The following formulas are valid:

• X(ϕ⇒ψ) ⇒ (Xϕ⇒Xψ) Xϕ ⇒ Y Xϕ ¬Xϕ ⇒ Y ¬Xϕ where X and Y stand for Bi, Di or Ii (for the same i).
• Relationship between belief and desire Biϕ ⇒ Diϕ
• Temporal operators ©(ϕ ⇒ ψ) ⇒ (©ϕ ⇒ ©ψ) ©(¬ϕ) ⇒ ¬ © ϕ φUψ ⇔ ψ ∨ (ϕ ∧ ©(ϕUψ))

2.4 Axiomatization

We give a proof system, called OBDI proof system, for those BDI-agents with perfect recall and a global clock, which contains the axioms of propositional calculus plus those formulas in Propositions 1. The proof system is closed under the propositional inference rules plus: ⊢ϕ ⊢Diϕ and ⊢ϕ ⊢Iiϕ for every agent i.

Theorem 2 The OBDI proof system is sound and complete with respect to interpreted BDI-systems with satisfaction relation |=OBDI .

3 Model Checking BDI-Agents

In order to make our model checking algorithm practically useful, we must consider where our model, an interpreted BDI-system comes from. To make the things simpler, we may consider some abstract programs such as �nite-state programs, which are expressive enough from the standpoint of theoretical computer science. Moreover, to make our model checking system practically ef�cient, we use symbolic model checking techniques. Thus, a �nite-state program in our approach is represented in a symbolic way.

3.1 Symbolic representation of interpreted BDI-agents

We formally de�ne a (symbolic) �nite-state program with n agents as a tuple P = (x, θ(x), τ (x, x′ ), O1, · · · , On), where x is a set of system variables; θ is a boolean formula over x, called the initial condition; τ is a boolean formula over x ∪ x′ , called the transition relation; and for each i, Oi ⊆ x, containing agent i's local variables, or observable variables. Given a state s, we de�ne agent i's local state at state s to be s ∩ Oi. We may associate with P an interpreted system IP = (R, π) called the generated interpreted system of P.

For convenience, we may use P(θ, τ) to denote a �nitestate program with n agents (x, θ(x), τ (x, x′ ), O1, · · · , On), if x and O1, · · · ,On are clear from the context. Given a �nite-state program P(θ, τ) with n agents, we de�ne an agent's internal program (over P(θ, τ) as a tuple 〈P(θ1, τ1),P(θ2, τ2),P(θ3, τ3)〉, where (θj ⇒ θ) ∧ τj ⇒ τ ,for j = 1, 2, 3, and (θ2 ⇒ θ1) ∧ τ2 ⇒ τ1 are valid. Clearly, an agent's internal program is exactly related with an agent's mental state. Thus, we de�ne a (symbolic ) BDI-program with n agents as a tuple PA = (PK, P1, · · · , Pn), where PK

is a �nite-state program with n agents and for each agent i, Pi is agent i's internal program over P. We use IPA to denote the corresponding interpreted BDI-system.

3.2 Model checking OBDI logic

Theorem 3 Given a BDI-program with n agents PA = (PK, P1, · · · , Pn), suppose that PK = (x, θ(x), τ(x, x′ ),O1, · · · ,On), and for every i, Pi = 〈P(θi1 , τ i1 ),P(θi2 , τ i2 ),P(θi3 , τ i3 )〉. Then, for every LTL formula ϕ and agent i, the following are valid in IPA ,

1. Biϕ⇔ ∀(x-Oi)(G(P(θi1 , τ i1 )) ⇒Γ(ϕ, θi1 , τ i1 ))
2. Diϕ ⇔ ∀(x - Oi)(G(P(θi2 , τ i2 )) ⇒ Γ(ϕ, θi2 , τ i2 ))
3. Iiϕ⇔ ∀(x-Oi)(G(P(θi3 , τ i3 )) ⇒Γ(ϕ, θi3 , τ i3 ))

where Γ(ϕ, θ, τ) is a boolean formula built from ϕ, θ, τ by using quanti�cations and �xed-point operations lft and gft.

Remark that Theorem 3 provides a reduction of OBDI to LTL, while Proposition 9 in [Su, 2004] gives an OBDDbased method of model checking LTL formulas. The complexity of our reduction of logic OBDI to LTL is PSPACEcomplete. However, because quanti�cations of boolean functions and �xed-point operators can be dealt with in any OBDD package, the reduction can be based on OBDDs. In fact, we implemented a prototype of the OBDI model checker using CUDD, a very in�uential OBDD package developed by Fabio Somenzi, and achieved some preliminary experimental results.

4 Concluding Remarks

In this work, we have explored computationally grounded modal logics that characterize the internal attitudes of an agent�its beliefs, desires, etc, beyond S5 axioms and carried out a methodology on symbolic model checking for general BDI-agents.