BDI logic with probabilistic transition
and fixed-point operator
NIDE, Naoyuki1 , Shiro Takata2 , and Megumi Fujita1
1

Nara Women’s University,
Kita-Uoya Nishimachi, Nara-shi, Nara, 630-8506 Japannide@ics.nara-wu.ac.jp, saboten@ics.nara-wu.ac.jp
2
Kinki University,
Kowakae 3–4–1, Higashi-Osaka-shi, Osaka, 577-8502 Japan
shiro@info.kindai.ac.jp

Abstract. One of the advantages of the BDI (Belief-Desire-Intention) model isthat we can formally discuss and prove properties about the mental states (beliefs,
desires and intentions) and behaviors of rational agents using a modal logic called
BDI logic. However, various extensions, such as probabilistic state transitions inreinforcement learning and cooperative acts in multi-agent environments, havebeen attempted in the BDI model. Since those notions are difficult to treat precisely in traditional BDI logic, the advantage of formalization in BDI logic is diminished. In this paper, we propose an extension of BDI logic, called TOMATO,
which introduces probabilistic state transitions and a fixed-point operator. We
can strictly describe and infer various properties of rational agents with thoseextended notions by using TOMATO.

1Introduction

The BDI (Belief-Desire-Intention) model [1] is a model of rational agents based on
Bratman’s “theory of intention” [2, 3]. There have been many studies and applications
on this model, which have proved its usefulness [4].
In the BDI model, a rational agent has three kinds of mental states, which are belief,
desire and intention, and the agent determines its action to achieve its goal by maintaining and updating these states of mind. One of the features of the BDI model is thatit has a modal logic system called “BDI logic”. BDI logic explicitly describes thosemental states and their temporal changes, so we can formally prove and discuss rational
agents’ mental states and their behaviors. For example, a blind commitment strategy [5],well-known one of the commitment maintenance strategies which is stated as ‘once anagent intends to achieve φ necessarily in the future, then she maintains that intention
until she believes that she has achieved φ’, can be written as INTEND(AF φ) ⊃ A(INTEND(AF φ) U BEL(φ)). As another example, a property of rational agent that “ifan agent intends to achieve p at the next time point, and believes that p and q are mutually excluded forever, then she does not intend to achieve q at that time”, one of theconsistencies of mental states [2], can be shown by proving INTEND(AX p) ∧ BEL(AG(p ⊃ ¬q)) ⊃ ¬ INTEND(AX q). This point is considered to be a major advantage
to designing rational agents, and that’s why the BDI model has been generally accepted.

However, in the advancement of research of rational agents, various extensions to
BDI logic have been proposed. If there are mismatches between notions appearing inthese extensions and the ones in traditional BDI logic, we may have difficulties in formalizing them appropriately. Therefore, one of the advantages of the BDI model that
we can strictly discuss properties about rational agents can be diminished. Examples ofsuch extensions are, as described in Section 2, “probabilistic state transitions” which
are used in the reinforcement learning task and “cooperative actions” which are used in
multi-agent system. In particular, these notions are considered important for realizationof rational agents in the real world. Based on this standpoint, we propose a logic systemcalled TOMATO (Theory about Observations of Multi-Agents with Tense and Odds)
which introduces probabilistic state transitions and a fixed-point operator by extending
traditional BDI logic.
We have constructed sound and complete deduction systems of traditional BDI logic
using sequence calculi [6–8]. Therefore, we also aim to construct one for TOMATO.
In this paper, we show the soundness of the deduction system of TOMATO, and in
addition, the completeness which is restricted to propositional logic. Our future work
includes studying the completeness of TOMATOin predicate logic.
With a deduction system, we can formally discuss properties of rational agents syntactically rather than semantically, and automatic proof checking also becomes possible. We also intend to construct a decision algorithm using the tableau method [9] inthe future, though restricted to propositional logic.
One of the advantages of TOMATO is that, using probabilistic state transition operators, we can describe state transitions in MDPs (Markoff decision processes), which
is a basis of the reinforcement learning task. In addition, using a fixed-point operator,
we can finitely describe notions, such as mutual belief and cooperative intentions, in
multi-agent systems, which cannot be described in LORA [10] without using infinite
conjunctions/disjunctions. Moreover, inferences about these properties using sequentcalculus are possible. These points are discussed in detail in Section 4.
In this paper, we first describe the mismatches between the traditional BDI modeland the above-mentioned new notions in Section 2, and we introduce TOMATOin Section 3. In Section 4, we show examples of descriptions and proofs in TOMATO concerning probabilistic state transitions and cooperative actions. In Section 5, we present
discussions and describe our future work, and conclude in Section 6.

2

Divergence from BDI Model

2.1

Treatment of probabilistic state transition

As described in Section 1, one of the notions that is difficult to treat strictly in traditional
BDI logic is the idea of probabilistic state transitions, which is mandatory to incorporatemachine learning techniques into the BDI model.
We propose the integration of a BDI agent and reinforcement learning, in which anagent combines deliberation and reflexive actions according to the situation [11].
For example, when we are passing a familiar road, we can select the route in response to our surroundings without the need for practical reasoning. As another example, a soccer player instantaneously performs an appropriate action according to theskills acquired by intensive training. Our idea is, similar to these situations, to importreactive action acquired by learning into a BDI agent to enable more human-like behaviors.
We attempted, within the BDI model, to describe state transitions used in MDP [12],which is a basis for the reinforcement learning task [13]. However, MDP is basically
based on probabilistic transitions, and within traditional BDI logic, which does not haveprobabilistic transition operators, we can only describe agent movement as “moves oneof the accessible states”.
For instance, if we try to write a situation “if an agent at state s1 executes an action
e1 , then it transfers to state s2 and receives reward 3 with probability 0.7, or transfers
to state s3 and receives reward 5 with probability 0.3” in traditional BDI logic, we haveto eliminate the probabilities and only write as “transfers to either one”.
PCTL [14] is known as a logical system that extends CTL to treat a probabilistictransition. However, since it describes probability per path (a line of time points) as described in Section 5.2, describing the probability for each action (event) may be difficultin this logic.
2.2

Treatment of cooperative action

Another example is the difficulty in the treatment of cooperative actions in multi-agent
environments. Even though this is an important issue, the original BDI logic can treat
only a single agent’s mental state.
There is a logical system LORA [10], which is extended to describe the mental states of multiple agents in multi-agent environments. It treats various concepts required for handling agents’ cooperative actions, such as mutual belief, recognition of
the potential for cooperative action, and generation and execution of joint intension.
However, LORA is a complicated logical system with various components, including action expressions corresponding to dynamic logic and operators such as Agt for
judging whether an agent can execute an action. Nevertheless, it is still necessary to
introduce new operators, by using infinite conjunctions/disjunctions of formulas, to describe cooperative actions,
If a logical system is complicated, it will be intractable and difficult to construct its
deduction system. Then the advantage of formalization in the logic is diminished. In
fact, the deduction system of LORA has not been given.
As an example, for an agent group g, to form a joint intention for achieving a mutual
goal (φ) of lifting a 1-ton object, it is necessary that agents in g can achieve this only
cooperatively, and they mutually believe this fact. To describe this situation in LORA,
we introduce the formula (J-Can0 g φ) using pre-existing operators, which states thatg can first achieve φ in a single step, as an abbreviation of a formula signifying that “gcan execute some action α and φ is achieved by this action. Also, g mutually believes
this fact”. Next, a formula (J-Can g φ) which states that an agent group g can achieve
the goal φ, is introduced as an abbreviation of the infinite disjunction (J-Can0 g φ) ∨(J-Can0 g (J-Can0 g φ))∨(J-Can0 g (J-Can0 g (J-Can0 g φ)))∨· · · . Subsequently,
the process of forming a joint intention of achieving φ is described using J-Can.
However, to be accurate, we have to introduce J-Can as a new operator rather thanas an abbreviation, because the infinite disjunctive cannot be originally written as aproper formula1 . Moreover, because infinite conjunctions are used in the definition ofmutual belief2 , this part of J-Can cannot be written in LORA either.
Consequently, we consider treating infinite conjunctions and disjunctions uniformly
by introducing a fixed-point operator to reduce complication of the syntax.

3

Extension of BDI logic

In this section, based on the discussions so far, we propose a modal logic system

TOMATO for easily handling the notions described in Section 2. TOMATO is abranching-time temporal logic with a fixed-point operator and mental state operatorsfor each agent in multi-agent environments.
3.1

FormulasSyntax We give the definition of formulas in TOMATO here. Hereinafter, the word‘formula’ means that of TOMATO unless expressly stated otherwise. Symbols like x
and y are used as usual variable symbols in first-order predicate logic, and symbols suchas X and Y are variable symbols, each of which expresses a formula. We call the latter‘formula variables’3 . Typically, they are used with fixed-point operators.
Suppose that we fix a first-order language L, a set of formula variables V, a set of
event constant symbols E, and a set of agent constant symbols A, where E and A are
finite and V is infinite. Hereafter, we write {p | p ∈ R, 0 ≤ p ≤ 1} as [0, 1]. Then,– Any atomic formula in L is a formula (in TOMATO).
– If φ, ψ are formulas, then φ ∨ ψ and ¬φ are also formulas.
– If φ is a formula and x is a variable symbol, then ∀xφ is also a formula.
– If e ∈ E, n is a positive integer, and for i = 1, 2, · · · , n, φi is a formula, pi ∈ [0, 1]
and ri ∈ {≥, >}, then Xe (r1 p1 φ1 | · · · | rn pn φn ) is a formula. In particular, whenn = 1, we write Xer1 p1 φ1 instead of Xe (r1 p1 φ1 ).
– If φ is a formula and a ∈ A, then BELa φ, DESIREa φ, INTENDa φ are formulas.
– If X ∈ V, then X is a formula.
– If φ is a formula, X ∈ V, and X does not occur negatively (i.e. does not occur in
odd number of nesting of ‘¬’) in φ, then µX.φ is a formula. However, X may occur
only inside the scope of any modal operator (Xe , BELa , DESIREa , INTENDa ); forexample, µX.p ∧ X is not a formula.
We introduce ∧, ⊃, ⇔, ∃ as abbreviations in the usual manner. In addition, νX.φ is anabbreviation of ¬µX.¬φ[X := ¬X]. Here µ is the so-called least fixed-point operator[15], and ν is the greatest fixed-point operator. We also introduce notations Xe<p φ,
In other words, no finite formula in LORA can be semantically equivalent to (J-Can g φ),without introducing a new operator.
2
See [10] for the need of infiniteness.
3
The name ‘formula variables’ may be slightly irrelevant, because they don’t range over formulas. However, their main use is to form fixed-points, which can be regarded as new formulas.
In this sense, we call them ‘formula variables’.
1next time φ1

next time.2 φ φcurrent
1 2time e e .1
φ2
e
φ ’ holds
e .4
φ does not hold .3 φ 1
φcurrent
time e .3
e .5
φ ’ holds e .2
φ holds2

φ = X (≥.3 φ1 | ≥.5 φ2 ), φ
e

0

e .4

Z1

φ1
φ2

ψ1ψ2

e .6
Z2
e .6
e .4

ψ2ψ3
ψ1

Z3

ψ3
e .6
e .4

ψ3ψ1
ψ2

= Xe≥.3 φ1 ∧ Xe≥.5 φ2Fig. 1. Intuitive explanation of Xe operator

Xe≤p φ, Xe=p φ as abbreviations of ¬ Xe≥p φ, ¬ Xe>p φ, (Xe≥p φ)∧(¬ Xe>p φ), respectively.
When needed, we eliminate ambiguities using parenthesis. Without parenthesis, operators associate in the following order: unary operators (including fixed-point operators), ∧, ∨, ⊃, ⇔. Moreover, ⊃ is right-associative, while other binary operators areleft-associative.
Informal explanation of operators Xe is an extension of the next-time operator AX
in CTL with an event e and transition probabilities. For example, Xe (≥.3 φ1 | ≥.5 φ2 )intuitively means that if an event e occurs, then at the next time point, φ1 holds withprobability of at least 0.3, and aside from that case, φ2 holds with probability of atleast 0.5. Note the difference between that formula and Xe≥.3 φ1 ∧ Xe≥.5 φ2 ; the former
ensures that the case in which φ1 holds and the one in which φ2 holds does not overlap,
but the latter does not (the left half of Fig. 1, where at each state φ1 and φ2 may or may
not hold unless expressly stated).
BELa φ, DESIREa φ and INTENDa φ mean that an agent a has a belief, desire or
intention φ, respectively. For simplicity, we currently do not introduce probabilities into
these mental state operators. However, it is thought to be possible to do so in the same
way as for Xe operator. It can be useful for modeling agents, which have functions ofsome sort of statistical estimations such as pattern recognition.
Expressiveness compared to traditional BDI logics It is known that branching-time
temporal logics with AX and the fixed-point operators have strictly stronger expressive
power than CTL* [16, 17].
Since
∧ TOMATO has an individual next-time operator for each event, we have towrite e∈E AXe φ (where, and hereafter, AXe φ is an abbreviation of Xe≥1 φ) to express
what is equivalent to AX φ in CTL. Formulas using other CTL or CTL* operators canalso be written in TOMATO in a similar manner. Moreover, with event-wise next-time
operators, we can write formulas such as µX.(ψ ∨ φ ∧ AXe X), which means that “ifan event e continuously occurs, then φ holds until ψ holds” and cannot be handled by
CTL*.
Using the fixed-point operator, we can also handle notions which correspond to theaction expressions in LORA [10]. In LORA, concatenations, choices, and repetitionsof actions, such as in dynamic logic, can be written as action expressions. For example,

B at

B at
t

t

e1
0.6
e1

e1
0.5
e1

t

e1
1.0
e2

0.5

0.4

e3

e2

0.6

1.0

0.4

e2

w’

1.0

w

w’’
=world=stateFig. 2. Overview of BDI structure

a formula of LORA (Nec α φ) means “just after executing an action α, φ holds”.
Supposing that α = ((α1 ; α2 )∗; α3 ), it means “if an action α3 is executed soon after
executing an action sequence α1 , α2 for arbitrary times, then φ holds”. In TOMATO,
the equivalent of this can be written as νX.(AXe3 φ ∧ AXe1 AXe2 X), where e1 , e2 , e3
are events corresponding to α1 , α2 , α3 , respectively.
Mutual mental states∧[8, 10] can also be handled by the fixed-point operator. Wheng ⊂ A, we abbreviate a∈g BELa φ as E-BELg φ. Then, we abbreviate E-BELg νX.
(φ ∧ E-BELg X) as M-BELg φ, which means that “a group of agents g has a mutual
belief φ”. Mutual desires and intentions can be written in the same manner.
3.2

Semantics

BDI structure First we fix the following:– a set of possible worlds W (6= ∅)– for each w ∈ W , a set of states St w (6= ∅) (may be different in different worlds)– for each w ∈ W and each t ∈ St w , an interpretation (including variable assignment)
iw,t of L. In other words, a domain U and an interpretation of each constant, predicate, function, and variable symbol of L. All components except the interpretationof predicate symbols must be the∪ same for all states.
– for each a ∈ A and each t ∈ w∈W St w , a serial, transitive and Euclidean binary
relation Bat on the set {w | t ∈ St w }, and serial binary relations Dat , Iat on the sameset.
e
– for each w ∈ W and each∑e ∈ E, a serial binary relation Rw
on St w , and a functione0eePw : Rw → [0, 1] where t0 ∈{t0 |tRw
e t0 } Pw (t, t ) = 1 for any t ∈ St w .
We call a tuple of the above-mentioned components a BDI-structure. Intuitively, a statecorresponds to a time point in temporal logics, and a possible world is a time tree ofestates. t Rw
t0 and Pwe (t, t0 ) = p mean that if an event e occurs at state t, then the0
next time is t with probability p. Bat , Dat , and Iat are accessibility relations on possible
worlds at time t, which represent the belief, desire and intention of agent a, respectively(an overview is shown in Fig. 2).
e
Since each Rw
is defined to be serial, any event can occur at any state. However,in fact, usually only specific events can occur at a specific state. This property can be
expressed by establishing a so-called dead-state d, at which a specific atomic formuladead holds, and creating state transitions from any state t to d with any non-executable
event at t (in particular, state transition from d by any event goes to d itself). For example, a property that “if an event e can occur, then φ holds after e occurs” can be written
as ¬ AXe dead ⊃ AXe φ.
In this paper, for simplicity, we do not consider the mental state consistencies of the
BDI model [7, 18]. Thus there are no special relationships among Bat , Dat and Iat . A
brief discussion on this issue appears in Section 5.1.
Interpretation of formulas We write {(w, t) | w ∈ W, t ∈ St w } as Swt hereafter.
Given a BDI structure M and a function fV : V → 2Swt , we define the interpretation[ φ]]hM,fV i of a formula φ as follows (note that [ φ]]hM,fV i ⊂ Swt).
– If φ is an atomic formula, [ φ]]hM,fV i = {(w, t) | φ is true w.r.t. iw,t }– [ φ ∨ ψ]]hM,fV i = [ φ]]hM,fV i ∪ [ ψ]]hM,fV i– [ ¬φ]]hM,fV i = Swt∩ \ [ φ]]hM,fV i– [ ∀xφ]]hM,fV i = u∈U [ φ]]hM u ,fV i where M u is a BDI structure obtained by replacing the interpretation of x in M with u.
– [ Xe (r1 p1 φ1 | · · · | rn pn φn )]]hM,fV i = {(w, t) | there are some mutually disjointet0 } s.t. Ti ⊂ {t0 | (w, t0 ) ∈ [ φi ] hM,fV i } andsubsets T1 , · · · , Tn of {t0 | t Rw∑0e
t0 ∈Ti Pw (t, t ) ri pi for i = 1, · · · , n} (note that each r1 , · · · , rn is ≥ or >)– [ BELa φ]]hM,fV i = {(w, t) | for any w0 s.t. w Bat w0 , (w0 , t) ∈ [ φ]]hM,fV i }– Similar for [ DESIREa φ]]hM,fV i and [ INTENDa φ]]hM,fV i– [ X]]hM,fV i = fV (X) for X ∈ V
Then, a formula φ, with (or without) free occurrences of a formula variable X, can be
regarded as a function fφ : Swt → Swt, which receives an interpretation of X as anargument and returns an interpretation of φ. Therefore, we define that– [ µX.φ]]hM,fV i is the least fixed-point of fφ .
Here, the least fixed-point is known to exist since fφ in this case is monotonic by definition [19].
We say that φ holds at a state t of a world w when [ φ]]hM,fV i 3 (w, t). If[ φ]]hM,fV i = Swt for any M and fV , we say that φ is valid.
3.3

Deduction system

In this section we give a deduction system of TOMATOusing sequent calculus.
We identify α-equivalent formulas. We regard the left-hand side of ‘→’ of a sequent
as a (finite) multi-set of formulas, and likewise for the right-hand side (thus we do nothave the exchange rule). Hereafter, we sometimes enclose a whole sequent into [ ] toclarify the range of the sequent in the text.
We use a capital Greek letter (Σ, ∆ etc.; including a letter with a hash such as Σ 0 ,and ∆0 ) to denote a multi-set of 0 or more formulas. As an exception, Θ contains only
one or no formula.
∧∨ The interpretation∧of a sequent [Σ ∨→ ∆] is defined as that of the formula Σ ⊃∆. We define that ∅ = true and ∅ = false, where true is an abbreviation of asuitable tautology and false is an abbreviation of ¬true.

Σ, φ, φ → ∆Σ → ∆, φ, φ
Σ→∆
Weak
CL
CR
Initialφ→φΣ, Σ 0 → ∆, ∆0
Σ, φ → ∆Σ → ∆, φΣ → ∆, φ
Σ, φ → ∆Σ, φ → ∆ Σ, ψ → ∆Σ → ∆, φ, ψ
¬L
¬R
∨L
∨R
Σ, ¬φ → ∆
Σ → ∆, ¬φ
Σ, φ ∨ ψ → ∆Σ → ∆, φ ∨ ψΣ, φ[x := t] → ∆Σ → ∆, φ[x := y]∀L∀RΣ, ∀xφ → ∆Σ → ∆, ∀xφΓ, Xe>1−p ¬φ → ∆X≥ R
Γ → ∆, Xe≥p φ

Γ, φ[X := µX.φ] → ∆Γ → ∆, φ[X := µX.φ]µLµR
Γ, µX.φ → ∆Γ → ∆, µX.φ

Γ, Xe≥1−p ¬φ → ∆X> R
Γ → ∆, Xe>p φ

Γ, BELa Γ → BELa ∆, Θ, BELa ΘΓ →Θ
DESIRE-KD
BEL-KD45
BELa Γ → BELa ∆, BELa Θ
DESIREa Γ → DESIREa Θ· · · Xer1 p1 (φ1 ∧ ψ1 ) ∧ · · · ∧ Xern pn (φn ∧ ψn ) · · ·
Γ →Θ
Xexcl
INTEND-KD
INTENDa Γ → INTENDa Θ· · · Xe (r1 p1 φ1 | · · · | rn pn φn ) · · ·Fig. 3. Inference rules of TOMATO(excluding a rule described in Section 3.4)

Inference rules We enumerate the inference rules of TOMATO in Fig. 3. However,note that there is an additional rule which is concerned with the Xe operator in theleft-hand side of ‘→’ of a sequent. It is not shown in Fig. 3 but described in Section 3.4.
For a multi-set of formulas Γ and a unaly operator K, K(Γ ) stands for a multi-setof formulas obtained by applying K for each element of Γ .
In the ∀L rule, t is an arbitrary term. In the ∀R rule, y is a variable symbol which
does not occur freely in the conclusion of the rule.
The Xexcl rule means that any subformula of the form shown in the assumption
anywhere in the sequent can be replaced by the formula shown in the conclusion. In
this rule, n ≥ 2, and for i = 1, · · · , n, ψi is ¬X1 ∧ · · · ∧ ¬Xi−1 ∧ Xi ∧ ¬Xi+1 ∧· · · ∧ ¬Xn , where X1 , · · · , Xn are formula variables that does not occur freely in the
conclusion of the rule. This rule is provided so that we can decompose formulas in theform of Xe (· · · ) into those in the form of Xer1 p1 φ1 , by reversely applying it.
The BEL-KD45 rule, same as in [6, 20], is constructed so that the axiom schemas
KD45 for the BEL operator are ensured to be held. The µL and µR rules are provided
to enable proofs by loop (see Section 6 for example), such as in [6, 20, 21].
3.4

Additional inference rule for Xe

In this section, we describe an additional inference rule for the Xe operator, which is
not included in Fig. 3.
Let Γ = {Xer1 p1 ψ1 , · · · , Xern pn ψn }, where each r1 , · · · , r∑n is ≥ or >, and Q =
Q
{ψ
,
·
·
·
,
ψ
}.
If
a
function
v
:
2
→
[0,
1]
satisfies
thatnQ⊂Q v(Q) = 1, and∑1( Q∈{T |T ⊂Q,ψi ∈T } v(Q)) ri pi holds for each i = 1, · · · , n, then we call v a probability distribution function (PrDF) of Γ . Intuitively, a PrDF determines probabilitiesof transitions from a state to next-time states, at each of which a subset Q of Q holds,
so that for each ψi , the probability that ψi holds satisfies ri pi .
For a PrDF v of Γ , we call {Q ⊂ Q | v(Q) > 0} a satisfaction request set (SRS) of
Γ on v, and write it as reqv (Γ ). Let Z be an SRS of Γ (on some PrDF v). If all elementsof Z are satisfiable, we say that Z is satisfiable. In general, Γ is satisfiable iff there is aψ1 , ψ2 → ψ2 , ψ3 → ψ3 , ψ1 →Xe≥.3 ψ1 , Xe≥.4 ψ2 , Xe≥.6 ψ3 →ψ2 →Xe≥.3 ψ1 , Xe≥.4 ψ2 , Xe≥.6 ψ3 →ψ1 →Xe≥.3 ψ1 , Xe≥.4 ψ2 , Xe≥.6 ψ3 →ψ3 →Xe≥.3 ψ1 , Xe≥.4 ψ2 , Xe≥.6 ψ3 →Fig. 4. Example of inference rules about Xe operators

satisfiable SRS Z of Γ .
If, for Z, Z 0 ⊂ 2Q , some Q ∈ Z and Z 00 ⊂ 2Q exist and Z 0 = (Z ∪ Z 00 ) \ {Q}holds, we write Z  Z 0 . Let  be a non-reflective transitive closure of . Note that if
Z  Z 0 and Z is satisfiable, then Z 0 is also satisfiable. If Z is an SRS of Γ , and there
is no SRS Z 0 of Γ which satisfies Z  Z 0 , we say that Z is an essential SRS (eSRS).
Since Q is finite, there is no infinite sequence Z1 , Z2 , · · · s.t. Z1  Z2  · · · . As aresult, there exists a satisfiable SRS of Γ iff there exists a satisfiable eSRS of Γ .
Let Z1 = {Q1,1 , · · · , Q1,m1 }, · · · , Zk = {Qk,1 , · · · , Qk,mk } be the enumeration of
all eSRSs of Γ . Then for any sequence of positive integers j1 , · · · , jk , where 1 ≤ j1 ≤m1 , · · · , 1 ≤ jk ≤ mk , the following is an inference rule of TOMATO.
Q1,j1 → · · · Qk,jk →X-KDΓ →For example, Let Γ = {Xe≥0.3 ψ1 , Xe≥0.4 ψ2 , Xe≥0.6 ψ3 } and Q = {ψ1 , ψ2 , ψ3 }.
Then a function v : 2Q → [0, 1], where v({ψ1 , ψ2 }) = 0.4, v({ψ3 }) = 0.6, andv(Q) = 0 for all other Q ⊂ Q is a PrDF of Γ , and reqv (Γ ) = {{ψ1 , ψ2 }, {ψ3 }} =Z1 is an SRS of Γ . Z1 is also an eSRS. A function v 0 , where v 0 ({ψ1 , ψ2 }) = 0.3,v 0 ({ψ2 }) = 0.1, v 0 ({ψ2 , ψ3 }) = 0.6, and v 0 (Q) = 0 for all other Q ⊂ Q is also a
PrDF of Γ , but reqv0 (Γ ) = Z10 is not an eSRS since Z10  Z1 .
In this example, Z1 and Z2 = {{ψ2 , ψ3 }, {ψ1 }} and Z3 = {{ψ3 , ψ1 }, {ψ2 }} (seethe right half of Fig. 1) are all eSRSs. In the tableau method, to show that [Γ →] isprovable, we have to show that Γ is unsatisfiable. It is equivalent to show that there isno satisfiable eSRS of Γ , and also equivalent to show that any eSRS of Γ has at least
one unsatisfiable element. The X-KD rule is constructed in this way.
Therefore, in this example, we have 8 (= |Z1 | · |Z2 | · |Z3 |) rules, and one of themis the following.
ψ 1 , ψ2 → ψ 2 , ψ 3 → ψ 2 →Xe≥.3 ψ1 , Xe≥.4 ψ2 , Xe≥.6 ψ3 →However, the leftmost two sequents of the assumption of this rule are redundant. Afterremoving similar redundancies from other rules, we need only 4 rules, as shown in Fig.
4, and the rest 4 can be omitted since the assumption of each of those includes anotherrule. (In addition, rules in Fig. 4 except the upper-left-most one can be aggregated intoa single ruleφ→

, where 0 < p ≤ 1.)

Xe≥p φ →Definition of provability A sequent S is said to be derivable from a set L of sequents
if one of the following conditions holds.

1. S ∈ L
S , · · · , Sn
2. There is an inference rule 1(n ≥ 0) and all of S1 , · · · , Sn are derivable
S
from LWe say that a sequent S is provable if one of the following conditions is satisfied.
Here φn (X) is defined as φ0 (X) = X and φn (X) = φ[X := φn−1 (X)].
1. S is derivable from ∅.
2. S = [Σ, µX.φ → ∆] where X does not occur freely in Σ, ∆, and there is a positive
integer n s.t. [Σ, φn (X) → ∆] is derivable from {[Σ, X → ∆]}.
A formula φ is defined to be provable if [→ φ] is provable.
Soundness and completeness In this section, we first show the soundness of

TOMATO, and then we show a proof sketch to show the completeness of TOMATO
restricted to propositional logic. A study of the completeness of TOMATOon predicate
logic is for future work.
To show the soundness, it is enough to show that every inference rule preserves thevalidity of sequents, and that S in the item 2. of the provability definition is valid. The
former is easy; therefore, we show the latter. For any ordinal α and the function fφ inSection 3.2, we define a function fφα : Swt → Swt as follows.
fφ0 (x) = x
fφα+1 (x) = fφ (fφα (x))∪{fφα (x)} when λ is a limit ordinalfφλ (x) =α<λThen, if [Σ, φn (X) → ∆] is derivable from {[Σ, X → ∆]}, for any BDI structure andany infinite ordinal α, [Σ → ∆] holds at any state in fφα (∅). Also, an infinite ordinal αexists s.t. fφα (∅) = [ µX.φ]]. Thus [Σ, µX.φ → ∆] is valid.
Next we show the proof sketch of the completeness restricted to propositional logic.
Without loss of generality, we can assume that any subformulas of the form Xe (r1 p1 φ1 |· · · | rn pn φn ), where n ≥ 2 do not occur anywhere in sequents, since we can omit themby reversely applying the Xexcl rule (as described in Section 3.3).
Let Nps be a set of non-provable sequents that have only atomic formulas (i.e.
atomic propositions) and formulas in the form of µX.φ, Xerp φ, BELa φ, DESIREa
φ, and INTENDa φ in the both sides of ‘→’, but do not have formulas in the form of
Xerp φ to the right of ‘→’. For S ∈ Nps, we define dec-µ(S) as a non-provable sequentobtained from S by reversely applying µL/R, ∨L/R, ¬L/R, X≥ R, and X> R rules as
many times as possible. If there are more than one such sequents, choose an arbitrary
one as dec-µ(S). Note that we cannot apply µL/R infinite times because in a formulaµX.φ we do not have any X outside the scope of modal operators.
Regarding Nps as a set of states, we construct a ‘flat’ version of BDI structure (i.e.
we do not take the set of worlds W into consideration, and all accessibility relations
are binary relations on Nps) by the following procedure, which is based on Wang’salgorithm [20, 22] for propositional modal logics.
First, we define binary relations Ba , Da , and Ia on Nps for each a ∈ A as follows.

– S Da S 0 iff we can obtain S 0 from dec-µ(S) by applying the following procedure:
1. First, reversely apply Weak to dec-µ(S) to leave only all formulas in the formof DESIREa φ to the left of ‘→’, and only one (iff there is any) of them in thatform to the right of ‘→’.
2. Then, reversely apply DESIRE-KD once to remove outermost DESIREa .
3. Last, reversely apply rules ∨L/R, ¬L/R, X≥ R, X> R as many times as possible.
– Similar for Ia .
– To define Ba , we first define Ba0 in a similar manner to that for Da and Ia . Let
BELa+ (S) be the set of formulas of the form BELa φ to the left of ‘→’ of sequent dec-µ(S), and BELa− (S) be a similar one for the right of ‘→’. Assume that
S = S0 Ba0 S1 Ba0 S2 Ba0 · · · . Then BELa+ (S0 ), BELa+ (S1 ), · · · , and BELa−(S0 ), BELa− (S1 ), · · · are both monotonically nondecreasing. Therefore, due to thefiniteness of formulas and sequents, there is some Sk that satisfies that if Sk Ba0∗S 0 (here Ba0∗ is the transitive closure of Ba0 ), then BELa+ (Sk ) = BELa+ (S 0 ) andBELa− (Sk ) = BELa− (S 0 ). We define that S Ba S 0 , S 0 Ba S 00 iff Sk Ba0∗ S 0 and
Sk Ba0∗ S 00 .
Next we define binary relations Re on Nps and a function P e : Re → [0, 1] for eache ∈ E as follows. Let a sequent S be given.
1. First, we reversely apply Weak to dec-µ(S) to leave only all formulas in the formof Xerp φ in the both sides of ‘→’.
2. Then, reversely apply X≥ R and X> R as many times as possible to move all formulas in the form of Xerp φ in the right-hand side of ‘→’ toward the left of ‘→’. At thismoment the sequent is in the form of [Γ →], where Γ is {Xer1 p1 ψ1 , · · · , Xern pn ψn }.
3. Since [Γ →] is not provable, by the construction of X-KD rule, there is a PrDF
v of Γ and an eSRS {Q1 , · · · , Qm } of Γ on v, where none of sequents [Q1 →], · · · , [Qm →] are provable.
4. Now, we put S Re S 0 and P e (S, S 0 ) = v(Qj ) iff S 0 can be obtained from some
[Qj →] above, by reversely applying rules ∨L/R, ¬L/R, X≥ R, and X> R as manytimes as possible.
Subsequently, for each state t in Nps, we choose an interpretation it of atomic propositions s.t. it (p) is true iff p occurs to the left of ‘→’ of the sequent dec-µ(t). In addition,
we also choose a function fV : V → 2Swt s.t. fV (X) 3 t iff X occurs to the left of ‘→’of the sequent dec-µ(t).
Now we have a ‘flat’ BDI structure. In addition, Ba satisfies KD45, and all otheraccessibility relations satisfy KD. We can easily convert it into a normal BDI structure
M.
Then we show that for each state t in M , formulas to the left of ‘→’ of the sequentt are true at t, and ones to the right are false at t. We do so only for the formulas of theform µX.φ at both sides of ‘→’.
Let F be a set of states (sequents) in M , which has µX.φ to the right of ‘→’. By
the construction method of M , for any ordinal α, we can show that (fφα (∅))c ⊃ F (here
Ac denotes a complement set of A). Therefore, µX.φ is false at any state in F .
Let S be a state (sequent) in M , which has µX.φ to the left of ‘→’, and S(n) be astate obtained from S by replacing µX.φ with φn (X). By the construction method ofM and the finiteness of formulas and sequents, there is a positive∪integer n s.t. for eachsequence of states S0 A S1 A · · · , where S0 = S(n) and A = a,t (Bat ∪ Dat ∪ Iat ) ∪∪e
4e,w Rw , one of the followings holds .
i. X does not occur in some Sk .
ii. There are some k, ` s.t. Sk = S` and X occurs in Sk .
If all such sequences satisfy ii., then S is provable using the item 2. of the provability
definition, and contradicts the assumption. Therefore, there is a sequence that satisfies i.
above. By the construction of M , there is also a sequence S00 A S10 A · · · , where S00 =S and which satisfies i., and again by the construction of M , µX.φ is true at S.
A decision algorithm for propositional TOMATO can be directly derived from thisproof of the completeness (if an algorithm to calculate eSRS is provided). We plan tomention this in the future.

4

Examples of description and proof

4.1

Modeling probabilistic state transitions

We can write the situation in the example of Section 2.1 as at(s1 ) ⊃ Xe1 (≥.7 at(s2 ) ∧reward(3) | ≥.3 at(s3 ) ∧ reward(5)) using the probabilistic transition operator of
TOMATO.
Let φ be this formula. We can confirm that if we are at s1 , then after executing e1 ,we can surely receive reward 3 or more by proving φ ∧ at(s1 ) ⊃ AXe1 ∃x(reward(x) ∧x ≥ 3), provided that we can prove 3 ≥ 3 and 5 ≥ 3. The proof is shown in Fig.
5, where we abbreviate at(s2 ), reward(3), at(s3 ), reward(5), and reward(x) ∧ x ≥ 3
as p1 , q1 , p2 , q2 , and ψ, respectively. An X-KD rule applied between the 3rd column
from the bottom and a column right above it is derived from the fact that all eSRSs of
111
ξ3 } are {{ξ1 , ξ2 }, {ξ3 }}, {{ξ2 , ξ3 }, {ξ1 }}, and {{ξ3 , ξ1 }, {ξ2 }}{Xe≥.7
ξ1 , Xe≥.3
ξ2 , Xe>0(where ξ1 , ξ2 , ξ3 are arbitrary formulas).
Machine learning cannot be performed only by describing in logic, and requires
external tools to do so. However, after learning, we can describe the result as a propertyof an agent like the one above. Also, there is a possibility to implement a learning
system within a frame of logic. In this sense, treating such properties in logic has apositive significance.
4.2

Modeling coordinated actions

J-Can described in Section 2.2 is necessary to describe coordinated actions. However,in LORA, it can only be written using infinite disjunctions and conjunctions. It is
expressible in TOMATOusing the fixed-point operator.
To describe the first half of the description of (J-Can0 g φ) in Section 2.2 (i.e. “g4In other words, the process of reversely applying rules continuously will eventually stop byentering a loop. That is why our system can have a decision algorithm, despite the lack ofsubformula property.

..
..
..
.
.
.
p1 ∧ q1 ∧ X1 ∧ ¬X2 , p2 ∧ q2 ∧ ¬X1 ∧ X2 →
→5≥3
→3≥3
6
..
..
.
.
p2 ∧ q2 ∧ ¬X1 ∧ X2 , ¬∃xψ → ¬∃xψ, p1 ∧ q1 ∧ X1 ∧ ¬X2 →1
1
1(p2 ∧ q2 ∧ ¬X1 ∧ X2 ), Xe>0¬∃xψ →
Xe≥.7(p1 ∧ q1 ∧ X1 ∧ ¬X2 ), Xe≥.3..
.
→ φ ∧ at(s1 ) ⊃ AXe1 ∃xψ
Fig. 5. Example of proof (1)can execute some action α and φ is achieved by this action”), we introduce a predicate
Agt s.t. Agt(e, a) holds iff an agent a can execute an event e. We use a list structure in
first-order language to represent a group of agents, and introduce the ‘member’ predicate using its general definition in Prolog, i.e. a non-logical axiom ∀x(member(x, cons
(x, nil)) ∧ ∀y∀z(member(x, z) ⊃ member(x,cons(y, z))))5 . Then, we can represent∨
the above-mentioned part as µX.(φ ∨ e∈E,a∈A (Agt(e, a) ∧ member(a, g) ∧ AXe X)).
(Note: LORA introduces equivalents for Agt and ‘member’ as primordial components
of formulas, and enables the applying of ∀ for agents and actions. These reduce thelength of formulas, but complicates syntax and semantics.)∧
Let ψ be this formula, and abbreviate νX.(ξ ∧ a∈A (member(a, g) ⊃ BELa X))
as E-Knowg ξ, which states that “ξ holds and an agent group g mutually believes it”.
Then E-Knowg ψ is equivalent to (J-Can0 g φ). Further, we can represent (J-Can g φ)by µX.((J-Can0 g φ) ∨ (J-Can0 g X)). By proceeding in this way, we can construct
further descriptions about coordinations of agents like in LORA.
To prove various properties of coordinations is also possible. Fig. 6 is a proof of aproperty (J-Can0 g φ) ⊃ E-Knowg (J-Can0 g φ), whose equivalent is represented in
LORA (we assume A in Section 3.1 be {a1 , · · · , an }). Using the above-mentioned ψ,gthis formula can be rewritten as E-Knowg ψ ⊃ E-Know
E-Knowg ψ, so we give the∧proof of this formula. In that figure, we abbreviate a∈A (member(a, g) ⊃ BELa ξ)
as Bg ξ. Hence, E-Knowg ξ is an abbreviation of ¬µX.(¬ξ ∨ ¬ Bg ¬X). Furthermore
we abbreviate µX.(¬ξ ∨ ¬ Bg ¬X) as nEkg ξ. As a result, E-Knowg ξ is syntacticallyequivalent to ¬ nEkg ξ. In Fig. 6, the topmost column of the rightward proof figure isderived from the leftward proof figure using the item 2. of the provability definition.

5

Discussions

We have given an extended BDI logic to handle notions required for formalizing realistic rational agents. However, there are more issues to consider, though we do not treat
them in this paper. In this section we discuss some of them.
5.1

Treatment of mental state consistencies

As we described in Section 3.2, we have omitted discussions about mental state consistencies for simplicity. However, mental state consistencies are significant in Bratman’s
5

In fact, the proof in Fig. 6 does not depend on this definition.

X → nEkg ψ..
.

X → nEkg ψ
..
.
a1

BEL

¬ nEkg ψ → ¬X
¬ nEkg ψ → ¬X
g
a1
a
n
..
¬ nEk ψ → BEL ¬X
BEL ¬ nEkg ψ → BELan ¬X
.
..
..
.
· · · (n branches in total) · · ·.

..
.
¬ E-Know ψ → nEkg ψg

Bg ¬ nEkg ψ → Bg ¬X..
.

nEkg E-Knowg ψ → nEkg ψ..
.

¬ Bg ¬X → ¬ψ ∨ ¬ Bg ¬ nEkg ψg¬ Bg ¬X → nEk ψg¬ E-Know ψ ∨ ¬ Bg ¬X → nEkg ψ→ E-Knowg ψ ⊃ E-Knowg E-Knowg ψFig. 6. Example of proof (2)intention principle and need to be handled to describe rational agents. For example, theproperty that “an agent will not form an intention if she cannot believe the possibilityof achieving it” is said to be one of the required properties of rational agents. In traditional BDI logic, as in [7, 18], this is written as INTEND(EX φ) ⊃ BEL(EX φ), andit presents the semantics that make it valid and the deduction system that can prove it.
Currently TOMATOcannot treat such a property. This is for future work.
When considering this, it is also interesting to consider consistency between probabilistic mental state operators mentioned in Section 3.1. For example, when the possibility of achievement of φ is believed with a probability 0.9, can we intend φ?
5.2

Treatment of probabilistic transitions

The temporal operator in TOMATO is an extension of the next-time operator in CTL
with a probability. This is because we introduced this operator so that we can constructa proof system base on the tableau method. However, a disadvantage of this is that thedescription with the probability is restricted to the transition between current time andthe next time.
In PCTL [14], we can describe the probability on the time sequence (path). In
other words, the probability is given on path formulas. For example, a property “wecan achieve φ not less than the probability of 0.9 in the future” can be written as[true U φ]≥0.9 . Currently TOMATOcannot describe such a property.
However, as described in Section 2.1, it is difficult to describe event-wise probabilities in PCTL, unlike in TOMATO. Moreover, it is believed to be difficult for PCTL
to create the proof system using the tableau method due to an excessive flexibility ofprobability descriptions in PCTL. Even for qualitative PCTL, in which probabilistic
descriptions are restricted to 0 and 1, no deduction system is yet known [23]. To takethe balance of construction of the proof system and flexibility of representation is an
important issue.
5.3

Treatment of stability of mental states

We believe that there are more issues to be considered on BDI logic though we did nottreat them in this paper. For example, mental states, such as belief, should generally bekept by default. However, there is no such concept in BDI logic in nature. The mental
states in BDI logic are merely modal operators, and represented by accessibility relations on possible worlds, which vary at different times. Thus, there is no logical relation
between the current belief and the one in the next time. If we want to keep the belief
to some extent, we must explicitly introduce a non-logical axiom such as ψ ⊃ A(BEL(φ) U ξ) (believes φ until ξ holds).
In the standard implementation of BDI agents, mental states, such as belief, arerestricted to first-order formulas, and an agent adds or deletes its mental states in its
database by an event such as add-belief and del-belief. The addition and deletionof her mental states occurs procedurally, so the consistency between it and the logic is
not guaranteed. There are some trials, such as AgentSpeak(L) [24], for bridging thisgap by offering a proof theory about the properties of such procedures. However, they
do not dissolve the un-naturalness of the logic that the mental states are not maintainedby default, nor eliminate the fact that mental states are restricted to first-order formulasin the implementations.
Mental states are not always expected to be kept; for example, if there is a belief
BEL(AX φ) (believes that “φ in next time”), it would be natural that we have BEL(φ)
the next time. [25] is one of such studies, though it is based on non-branching temporal
logic and lack of descriptive power is anticipated. It will be interesting to consider how
we treat such things in modal logics.
Some studies treat the updating of mental states as an update of the model itself
instead of time transition. Though such a method is difficult to apply to MDP because
time path is restricted to be unique, it may be also a possibility to handle stability ofmental states naturally.

6

Conclusion

In this paper, we proposed TOMATO, an extended BDI logic with probabilistic transitions and a fixed-point operator, to enable formal descriptions and discussions on rational agents with notions such as probabilistic state transitions in reinforcement learningand cooperative actions in multi-agent environments. We also showed some examples
of descriptions and proofs associated with these notions. Our future work includes a
study of the completeness of TOMATO on predicate logic, construction of a proof algorithm in propositional logic and to introduce some of the notions described in Section
5, especially the consistency of mental states.
We expect TOMATO to be a productive tool for modeling, designing and implementing rational agents.

References
1. Rao, A.S., Georgeff, M.P.: Modeling Rational Agents within a BDI-Architecture. In: Proc. ofInternational Conference on Principles of Knowlegde Representation and Reasoning. (1991)
473–484
2. Bratman, M.E.: Intention, Plans, and Practical Reason. Harvard University Press (1987)

3. Bratman, M.E., Israel, D.J., Pollack, M.E.: Plans and resource-bounded practical reasoning.
Computational Intelligence 4 (1988) 349–355
4. Wooldridge, M., Rao, A., eds.: Foundations of Rational Agency. Volume 14 of Applied
Logic Series. Kluwer Academic Publishers (1999)
5. Rao, A.S., Georgeff, M.P.: Modeling Rational Agents within a BDI-Architecture. In Huhns,
M.N., Singh, M.P., eds.: Reading in Agents. Morgan Kaufmann, San Francisco (1997) 317–
328
6. Nide, N., Takata, S., Araragi, T.: Deduction Systems for BDI Logics Using Sequent Calculus.
Computer Software 20(1) (2003) 66–83 (In Japanese).
7. Nide, N., Takata, S., Araragi, T.: Reasoning About Mental State Compatibilities of Rational
Agents and Its Applications. Transactions of the Institute of Electronics, Information andCommunication Engineers J86-D-I(8) (2003) 514–523 (In Japanese).
8. Nide, N., Takata, S., Araragi, T.: A Deduction System of Extended BDI Logic to Handle
Mutual Belief. Transactions of Information Processing Society of Japan 46(SIG2 (TOM11))(2005) 85–99 (In Japanese).
9. Wolper, P.: The tabuleau method for temporal logic: an overview. Logique et Anal. 28 (1985)
119–136
10. Wooldridge, M.: Reasoning about Rational Agents. The MIT Press (2000)
11. Takata, S., Nide, N., Yamakawa, H., Miyazaki, K., Ohta, M.: An achievement method of
bdi agent who practically reasons about the skill acquired isung reinforcement learning. In:
Proc. of JAWS2004. (2004) 517–524 (In Japanese).
12. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming.
John Wiley & Sons (1994)
13. Nide, N., Takata, S., Yamakawa, H., Miyazaki, K., Ohta, M.: Correspondence between BDI
model and world model in reinforcement learning. In: Proc. of JAWS2004. (2004) 378–385
14. Hansson, H., Jonsson, B.: A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6(5) (1994) 512–535
15. Kozen, D.: Results on the propositional µ-calculus. Theoretical Computer Science 27 (1983)
333–354
16. Dam, M.: Translating CTL into the modal µ-calculus. Technical Report ECS-LFCS-90123, Laboratory for Foundations of Computer Science, Department of Computer Science,
University of Edinburgh (1990)
17. Manolios, P.: Mu-calculus model-checking. In: Computer-Aided reasoning: ACL2 casestudies. Kluwer Academic Publishers (2000) 93–111
18. Rao, A.S., Georgeff, M.P.: Decision Procedures for BDI Logics. Journal of Logic andComputation 8(3) (1998) 292–343
19. Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pacific Journal of
Mathematics 5 (1955) 285–309
20. Nide, N., Takata, S.: Deduction Systems for BDI Logics Using Sequent Calculus. In: Proc.
of International Joint Conference on Autonomous Agents & Multiagent Systems (AAMAS
2002). (2002) 928–935
21. Stirling, C.: Modal and Temporal Properties of Processes. Springer Verlag (2001)
22. Wang, H.: Towards mechanical mathematics. IBM Journal of Research and Development 4(1960) 224–268
23. Brázdil, T., Forejt, V., Křetı́nský, J., Kučera, A.: The satisfiability problem for probabilistic
ctl. In: Proc. of 23rd Annual IEEE Symposium on Logic in Computer Science. (2008) 391–
402
24. Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: Proc.
of MAAMAW-96. Volume 1038 of LNAI., Springer-Verlag (1996) 42–55
25. Su, K., Sattar, A., Wang, K., Luo, X., Governatori, G., Padmanabhan, V.: Observation-based
Model for BDI-Agents. In: Proc. of AAAI 2005. (2005) 190–195