2016 International Conference on Agents

Tracing Werewolf game by using extended BDI model
NIDE, Naoyuki

Shiro Takata

Faculty, Division of Human Life and Environmental Sciences
Nara Women’s University
Kita-Uoya Nishimachi, Nara, Japan
E-mail: nide@ics.nara-wu.ac.jp

Faculty of Science and Engineering
Kindai University
Kowakae 3–4–1, Higashi-Osaka, Japan

Abstract—The werewolf game is a kind of role-playing gamein which players have to guess other players’ roles from theirspeech acts (what they say). In this game, players have toestimate other players’ beliefs and intentions, and try to modify
others’ intentions. The BDI model is a suitable model for thisgame, because it explicitly has notions of mental states, i.e.
beliefs, desires and intentions. On the other hand, in this game,players’ beliefs are not completely known. Consequently, in manycases it is difﬁcult for players to choose a unique strategy; inother words, players frequently have to maintain probabilistic
intentions. However, the conventional BDI model does not havethe notion of probabilistic mental states. In this paper, we propose
an extension of BDI logic that can handle probabilistic mental
states and use it to model some situations in the Werewolf game.
We also show examples of deductions concerning that situations.
We believe that this study will serve as a basis for developing a
Werewolf game agent based on BDI logic.

I.

Osawa et al.[1] devised a BDI logic with probabilistic
mental states, and used it to model the Werewolf game. They
showed reasoning about the players’ beliefs. However, they did
not give formal semantics or a deduction system. Moreover,their example did not use probabilistic mental states.
We proposed another extended BDI logic with probabilistic
mental states, gave its formal semantics and deduction system,and showed several deductions about Werewolf games thatused probabilistic mental states[2, in Japanese]. However, it isimportant to capture the process of state transitions to model
the Werewolf game, since it reﬂects the thinking processes ofplayers. In particular, one agent’s beliefs should be able to be
modiﬁed by another agent’s speech acts, i.e. be affected bywhat the other agent says. Yet, our study mentioned above did
not include any examples of this.

I NTRODUCTION

In this paper, we show examples of deductions in our logic
system, including representations of agents’ speech acts andstate transitions caused by them. Our logic system, called
TOMATOes -P , is an extension of TOMATO[3], which we
previously proposed and is itself an extension of the BDI logic.
We aim to develop agents for playing Werewolf games basedon reasoning, and we believe that this study to be a ﬁrst step
toward this goal.

AIs for match-type games such as shogi and go have
evolved remarkably. These games are complete information
games in that each player ideally knows all the information
about the current phase of the game. In contrast, in somegames, players can only get incomplete information about thegame. Such games are called incomplete information games,
and the Werewolf game (originally also known as Maﬁa) is
one such game.
Some attempts have already been made to develop agentsfor playing Werewolf, and they typically make use of machinelearning. Yet, we consider that the BDI model is more usefulfor developing such agents. In the Werewolf game, due tothe incompleteness of information, players have to estimate
other players’ beliefs and intentions, and try to modify others’ intentions. The BDI model is useful for modeling suchcircumstances, since it explicitly has notions of mental statessuch as beliefs, desires and intentions.

II.

In this section, we introduce our modal logic system

TOMATOes -P (TOMATO extended with Event Selection and
Probabilistic mental states). It is an extension of TOMATO[3](Theoretical Observation of Multi-Agent system with Tense
and Odds) obtained by adding probabilistic mental state operators and event selectability operator.
For simplicity, in regard to mental state consistencies[4],which are considered to be important properties of autonomous
agents modeled in the BDI model, we only consider part ofthem in this paper. To be precise, we do not consider “realism”
or any properties derived from it, such as “asymmetry thesis”;
e.g. “an agent who does not believe a goal to be eventuallyachievable will not intend to eventually achieve that goal”.
We only take into account the introspection axioms; e.g. “anyagent has complete beliefs about its mental states”1 .

However, the conventional BDI model does not have thenotion of probabilistic mental states, especially probabilistic
intentions. In other words, it is considered normal that a BDI
agent would choose single plan for its goal at a time and form
an intention to commit to the plan. Nonetheless, in Werewolf,
due to the incompleteness of information, it is often the casethat a player has to choose from a number of strategies. For
example, when a player has probabilistic multiple beliefs about
the identity of the wolf, then (s)he may have probabilistic
multiple intentions as to voting for someone, and may not
be able to choose one of them until just before they make thedetermination. To handle such a situation, it would convenient
if the BDI model had notions of probabilistic mental states.
978-1-5090-3931-9/16 $31.00 © 2016 IEEE
DOI 10.1109/ICA.2016.28

E XTENDED BDI LOGIC

1 TOMATO considers neither realism nor introspection axioms. While ourprevious work TOMATOes [5] considers both of them, it does not consider
probabilistic desires or intentions.

7φ. Accordingly, AX φ denotes “for any possible event between
the current time and the next time point, φ holds at the latter”,
and this corresponds to the AX operator of CTL. Because it has
the AX operator and a ﬁxed-point operator μ, TOMATOes -P
is more expressive than CTL* as a temporal logic. Hereafter,
we will assume that all operators of CTL have already been
introduced as abbreviations (e.g. AG φ is an abbreviation of¬μX.(¬φ ∨ ¬ AX ¬X)).

A. Syntax
Here, we deﬁne the formulas in TOMATOes -P . Hereinafter, the word “formula” means one of TOMATOes -P
unless expressly stated otherwise. Symbols like x and y areused as the usual variable symbols in ﬁrst-order predicate
logic, while symbols such as X and Y are variable symbols
that express formulas. We call the latter “formula variable
symbols”. They are mainly used with ﬁxed-point operators.
We choose and ﬁx a ﬁrst-order language L, an inﬁnite setof formula variable symbols V, a ﬁnite set of event constantsymbols E and a ﬁnite set of agent constant symbols A.
Hereafter, we write {p | 0  p  1} as [0, 1].

B. Semantics
1) BDI structure: First we choose and ﬁx the following:

We deﬁne formulas as follows.
•

Any atomic formula in L is a formula (in TOMATOes P ).

•If φ, ψ are formulas and x is a variable symbol in L,then φ ∨ ψ, ¬φ and ∀xφ are formulas.

•

If e ∈ E, then pos(e) is a formula.

•

If Op is one of Xe (where e ∈ E), BELa , DESIREa
and INTENDa (where a ∈ A), and n is a positive
integer, and for i = 1, 2, · · · , n, φi is a formula, pi ∈[0, 1], ri ∈ {, >}, then Op(r1 p1 φ1 |· · ·| rn pn φn ) is aformula. In particular, if n = 1, we omit the outermost
parentheses. We call the pi in this item probability
parameters.

•

If X ∈ V, then X is a formula.

•

If φ is a formula, X ∈ V, and X does not occur
negatively in φ, then μX.φ is a formula. Here, “occur
negatively” means that there are odd numbers of ¬’s
in the path from the root of the tree structure of φto the occurrence of that X. μ is the least ﬁxed-point
operator.

•

A set of possible worlds W (= ∅)•For each w ∈ W , a set of states St w (= ∅)•For each w ∈ W and each t ∈ St w , an interpretation iw,t of L. We assume that the domain and theinterpretation of terms are the same for all w and t.

•

For each w ∈ W and each t ∈ St w , an non-empty
subset pos w,t of E•e
For each w ∈ W andeach e ∈ E, a function Rw:
e
St 2w → [0, 1] where t ∈St w Rw
(t, t ) = 1 for anyt ∈ St w

For each a ∈ A and each t ∈ w∈W St w , (hereafter,
we write {w | t ∈ St w } as Wt ) functions Bat , Dat ,Iat : Wt2 → [0, 1] which satisfy:t for each w ∈ Wt ,w ∈Wt Ba (w, w ) = 1,
and similar for Dat , Iat for each w, w ∈ Wt which satisfy Bat (w,w ) > 0 and each w ∈ Wt , Bat (w, w ) =Bat (w , w ), Dat (w, w ) = Dat (w , w ) andIat (w, w ) = Iat (w , w )•We call a tuple of the above-mentioned components a BDI
structure. Intuitively, a state corresponds to a time point in
temporal logic, and a possible world is a time tree of states
whose edges are {(t, t ) | there is some e ∈ pos w,t whereeRw(t, t ) > 0}. pos w,t is a set of events which can be currentlyeexecuted, and Rw(t, t ) = p means that if an event e is
executed at state t, the next time is t with probability p.
Bat , Dat , and Iat are accessibility relations (with possibilities)
between possible worlds, which represent the belief, desire andintention of agent a with possibilities at time t. Bat (w, w ) > 0
roughly corresponds to the existence of the accessibility relation w Bat w in the usual Kripke semantics.

In addition, we introduce operators such as ∧, ⊃, ⇔ and ∃as abbreviations in the usual manner, and set standard priority
order among operators (e.g. unary operators combine ﬁrst, ∧combines before ∨, ⊃ is right associative, and parentheseschanges priorities).
For example, BELa (0.3 φ1 | 0.5 φ2 ) is a formula. Intuitively, this formula means “agent a believes φ1 with probability of at least 0.3, and as another possibility, believes φ2with probability of at least 0.5”. DESIREa and INTENDa
are similarly interpreted. Xe is an extension of the next-time
operator AX in CTL (computation tree logic) with an event
e and transition probabilities; for example, Xe.3 φ1 intuitively
means that if an event e occurs, then at the next time point,
φ1 holds with probability of at least 0.3. In addition, pos(e)intuitively means “event e can be executed now”.

2) Interpretation of formulas: Hereafter, we write {(w, t) |w ∈ W, t ∈ St w } as Swt. Given a BDI structure M and afunction fV : V → 2Swt , we deﬁne the interpretation [ φ]]M,fV 
of a formula φ as follows (note that [ φ]]M,fV   Swt). We saythat φ holds at a state t of a world w when [ φ]]M,fV  (w,t). If [ φ]]M,fV  = Swt for any M and fV , we say that φ isvalid.

BELa<p φ, BELa=p φ etc. are treated as abbreviations of
BELa1−p ¬φ and BELap φ ∧ ¬ BELa>p φ, etc. The same goesfor Xe , etc.
Additionally, we abbreviate BELa1 φ as BELa φ, which
denotes a usual (i.e. without probability) belief of agent aa(the same goes for DESIREa and INTEND ). Moreover, weabbreviate Xe1 φ as AXe φ, and e∈E (pos(e) ⊃ AXe φ) as AX
8•

If φ is an atomic formula, [ φ]]M,fV  = {(w, t) | φ istrue w.r.t. iw,t }•[ φ ∨ ψ]]M,fV  = [ φ]]M,fV  ∪ [ ψ]]M,fV •[ ¬φ]]M,fV  = Swt \ [ φ]]M,fV 

•

•
•


rule, n  2, and for i = 1, · · · , n, ψi is Xi ∧ 1jn,i=j ¬Xjwhere X1 , · · · , Xn are formula variable symbols that do notfreely occur in the conclusion of the rule. This rule is provided
so that we can decompose formulas in the form of Op(· · ·|· · · )into those in the form of Op r1 p1 φ, by inversely applying it.

[ ∀xφ]]M,fV  = u∈U [ φ]]M [x:=u],fV  where M [x :=u] is a BDI structure obtained by replacing the interpretation of x in M with u[ pos(e)]]M,fV  = {(w, t) | pos w,te}e[ X (r1 p1 φ1 | · · · | rn pn φn )]]M,fV  = {(w, t) | for i =1, · · · , n, there are mutually disjoint sets T1 , · · · , Tn
that satisfy the following} Ti  {t | (w, t ) ∈ [ φi ] M,fV  }e ( t ∈Ti Rw (t, t )) ri pi (note that each r1 ,· · · , rn is  or >)•[ BELa (r1 p1 φ1 | · · · | rn pn φn )]]M,fV  = {(w, t) | fori = 1, · · · , n, there are mutually disjoint sets W1 , · · · ,Wn that satisfy the following} Wi  {w | (w , t) ∈ [ φi ] M,fV  } ( w ∈Wi Bat (w, w )) ri pi•

The same goes for DESIREa and INTENDa•

If X ∈ V, [ X]]M,fV  = fV (X)2) Additional inference rules: Here we set Op to be one ofXe , BELa , DESIREa or INTENDa . Let Γ = {Op r1 p1 ψ1 , · · · ,Op rn pn ψn }, where each r1 , · · · , rn is  or >, and Q = {ψ1 ,· · · , ψn }.
We say that a set Z = {Q1 , · · · , Qm } (where each Qi is
a subset of Q) is a satisfaction request set (SRS) of Γ iff thefollowing m-variable linear simultaneous inequation has any
solution.
⎧ ⎨
1jm xj = 1(for 1  j  m)
x
j >0
⎩ (
x
)
r
p
(for 1  i  n)jii
1jm,ψi ∈Qj
Then, Γ is satisﬁable iff there is an SRS Z of Γ where each1ψ1 ,element of Z are satisﬁable. For example, if Γ = {Xe0.3
e1
e1
X0.4 ψ2 , X0.6 ψ3 } and Z = {{ψ1 , ψ2 }, {ψ3 }}, Z is an SRSof Γ. If {ψ1 , ψ2 } and ψ3 are both satisﬁable, so is Γ.

Accordingly, a formula φ, with (or without) free occurrencesof a formula variable symbol X, can be regarded as a function
fφ : Swt → Swt, which receives an interpretation of X as
an argument and returns an interpretation of φ. Therefore, wedeﬁne that•If, for Z, Z  ⊂ 2Q , some Q ∈ Z and Z  ⊂ 2Q exist andZ = (Z ∪ Z  ) \ {Q} holds, we write Z  Z  . We call Z an
essential SRS (eSRS) of Γ if Z is an SRS of Γ and there is no
SRS Z  of Γ which satisﬁes Z  Z  . It is easy to show that Γ
is satisﬁable iff there is an eSRS Z of Γ and each element of
Z is satisﬁable. In other words, Γ is unsatisﬁable iff for any
eSRS Z of Γ, there is an unsatisﬁable element of Z.
[ μX.φ]]M,fV  is the least ﬁxed-point of fφ .

Here, the least ﬁxed-point exists since fφ in this case ismonotonic by deﬁnition[6].

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
TOMATOes -P , provided that Op is one of Xe , DESIREa or
INTENDa .

From the properties of Bat , Dat and Iat , the introspection axioms hold; i.e. if Op is one of BELa , DESIREa or INTENDa, then Op(r1 p1 φ1 | · · · | rn pn φn ) ⇔ BELa Op(r1 p1 φ1 | · · · | rn pn
φn ) is valid.
C. Deduction system

Q1,j1 → · · · Qk,jk →XDI-KDΓ→In this section we describe the deduction system of
TOMATOes -P using sequent calculus.
We identify α-equivalent formulas. We regard the left sideof “→” of a sequent as a (ﬁnite) multi-set of formulas, andlikewise for the right side (thus we do not have the exchangerule). Hereafter, we sometimes enclose a whole sequent in [ ]to clarify the range of the sequent in the text.

If Op is BELa , the following is an inference rule. Here Σ isa multi-set of formulas whose top-level operator is DESIREa
or INTENDa (with the same agent a). Γ and Σ remain in theassumption so as to make the introspection axioms provable.
Γ, Q1,j1 , Σ →We will use capital Greek letters (Σ, Δ etc.; including
letters with a hash such as Σ , and Δ ) to denote multi-sets of
0 or more formulas.

· · · Γ, Qk,jk , Σ →BEL-KD45-DI
Γ, Σ →

If we want to consider the realism property, we have tomodify these rules. It will be our future work.

1) Inference rules: Now let us enumerate the inference
rules. Note that there are two more rules described in Sec.
II-C2.

3) Provability: A sequent S is said to be derivable froma set L of sequents if S ∈ L, or there is an inference ruleS1 , · · · , Sn(n  0) and all of S1 , · · · , Sn are derivable fromS
L.

In the ∀L rule, t is an arbitrary term. In the ∀R rule, y isa variable symbol that does not occur freely in the conclusionof the rule. In the evAll rule, {e1 , · · · , en } is equivalent to E.
In the Opexcl , Op R and Op> R rules, Op may be one ofXe , BELa , DESIREa or INTENDa (and must be same for one
application of this rule). Opexcl rule means that any subformulaof the form shown in the assumption anywhere in the sequentcan be replaced by the formula shown in the conclusion. In thisWe say that a sequent S is provable if one of the following
conditions is satisﬁed. Here φn (X) is deﬁned as φ0 (X) = X
and φn (X) = φ[X := φn−1 (X)].
1)

9

S is derivable from ∅.

Σ, φ, φ → Δ
Σ→Δ
Weak
CL
Σ, Σ → Δ, Δ
Σ, φ → Δ

Σ → Δ, φ, φ
Σ → Δ, φ
Σ, φ → Δ
Σ, φ → Δ Σ, ψ → Δ
CR
¬L
¬R
∨L
Σ → Δ, φΣ, ¬φ → Δ
Σ → Δ, ¬φ
Σ, φ ∨ ψ → Δ
Γ, Op 1−p ¬φ → Δ
Γ, Op >1−p ¬φ → Δ
Γ, φ[X := μX.φ] → Δ
Γ → Δ, φ[X := μX.φ]
Σ → Δ, φ, ψ
Op R
Op> R
μL
μR
∨R
Σ → Δ, φ ∨ ψΓ, μX.φ → Δ
Γ → Δ, μX.φ
Γ → Δ, Op p φ
Γ → Δ, Op >p φ

φ→φInitialΣ, φ[x := t] → Δ∀LΣ, ∀xφ → Δ
Fig. 1.

2)

Σ → Δ, φ[x := y]evAll∀RΣ → Δ, ∀xφ→ pos(e1 ), · · · , pos(en )· · · Opr1 p1 (φ1 ∧ ψ1 ) ∧ · · · ∧ Oprn pn (φn ∧ ψn ) · · ·Opexcl· · · Op(r1 p1 φ1 | · · · | rn pn φn ) · · ·Inference rules of TOMATOes -P

S = [Σ, μX.φ → Δ] where X does not occur freelyin Σ, Δ, and there is a positive integer n s.t. [Σ,φn (X) → Δ] is derivable from {[Σ, X → Δ]}.

φ→φ ψ→ψ
classicφ ⊃ ψ, ¬ψ, ¬¬φ →BEL-KD45-DI+ WeakBELa.9 (φ ⊃ ψ), BELa ¬ψ, BELa>.1 ¬¬φ →
Op R
a
a
a
BEL.9 (φ ⊃ ψ), BEL ¬ψ → BEL.9 ¬φclassic→ BELa.9 (φ ⊃ ψ) ∧ BELa ¬ψ ⊃ BELa.9 ¬φ

The soundness of TOMATOes -P can be proved just likein [3] and is relatively easy. We also expect that we can show
the completeness of TOMATOes -P . We guess that the proof
is similar to the sketch we gave in our previous study[5].

Fig. 2.

III.

Proof of formula (4)M ODELING W EREWOLF

In this section, as an example of actual Werewolf play, we
select a story written in [7] and show some descriptions andproofs, though rather simple, about the game process near theend of the story. The story is a description of a Werewolf match
between AIs, and the AI Werewolf Project submitted this story
to the 3rd Hoshi-Shin’ichi award of Nikkei Inc. as “a novel thatan AI was involved in writing”. However, to make the story
in the style of SF, the terminology of the Werewolf game was
replaced with other words; e.g. “werewolf” was changed into
“AI”, “seer” into “analyst”, etc. In the following, we turn thosewords back into the original ones. Note that the spoiler of thestory is included hereafter.

Formula (3) represents that if player2 is a lunatic, then(since the werewolf is very likely to know it) unless (s)heis executed, tomorrow the werewolf will collude with him/her
and the villagers’ side will likely lose. 0.8 in that formula may
not be accurately 0.8, but will be some relatively large value.
B. Inferences using mental state operators with probability
At this time, player6 says that “if player2 were a werewolf,a lunatic would very likely support a werewolf in some way,
but actually no such action has been observed”. Viewing thisspeech as a decisive factor, many players vote for player4, andas a result, player4 is executed. Here we write “player x has
acted by supporting a werewolf in some way” as support(x).
Accordingly, “since no support action by a lunatic has been
observed, maybe player2 is not a werewolf” is represented asfollows.

A. Representing some situation
Near the ﬁnal stage of the game, ﬁve players (out of ten)are still alive; player1 (medium), player2 (confessed2 to being
a seer, but is actually a lunatic3 ), player4 (villager), player6(werewolf) and player9 (villager). As the game progresses, theplayers come to believe that there is only one werewolf alive.
Though this belief is actually uncertain, for simplicity, we willassume that the players are certain in this belief.

BELa.9 (wolf (player2 ) ⊃ ∃x support(x)) ∧BELa ¬∃x support(x)⊃ BELa.9 ¬wolf (player2 )This formula can be proved as in Fig. 2. Here, for sake ofreadability, we have replaced some subformulas with φ, ψ etc.
and displayed some applications of rules in a bundled manner(the same goes for the proofs hereafter). The application of
BEL-KD45-DI depends on the fact that the only eSRS of{BELa.9 (φ ⊃ ψ), BELa1 ¬ψ, BELa>.1 ¬¬φ} is {{φ ⊃ ψ, ¬ψ,¬¬φ}}.

One day, player2 says that (s)he has divined player4 andthat player4 is a werewolf. However, in the past, player5 (whohas confessed to being a seer, and was already executed) said
that player4 is a human.
So the village has to make a decision whether to believe
player2 as a seer and execute player4 or to doubt player2 as awerewolf and execute him/her. We can describe this situation
as follows. AX operator denotes the next day, and executed
denotes “executed yesterday”.
BELa (seer (player2 ) ⊃AX(executed (player4 ) ⊃ village win))
BELa (wolf (player2 ) ⊃AX(executed (player2 ) ⊃ village win))
BELa0.8 (lunatic(player2 ) ⊃AX(¬executed (player2 ) ⊃ village lose))(4)

In this game, most players commonly have the belief thateither player2 or player5, each of which has confessed to being
a seer, is highly likely to be a werewolf. As a result, at thistime most players apparently think that player2 is either a seeror a werewolf. Given this belief, together with the result fromformula (4), one can conclude that player2 is likely to be aseer. This process can be represented as follows and is provedin Fig. 3.

(1)
(2)

BELa.8 (wolf (player2 ) ∨ seer (player2 )) ∧BELa.9 ¬wolf (player2 )⊃ BELa.7 seer (player2 )(3)

2 This action is also called “coming out”.
3 Also called “possessed”.

10

(5)

φ→φ ψ→ψ
classicφ ∨ ψ, ¬φ, ¬ψ →BEL-KD45-DI+ WeakBELa.8 (φ ∨ ψ), BELa.9 ¬φ, BELa>.3 ¬ψ →
Op R
a
a
a
BEL.8 (φ ∨ ψ), BEL.9 ¬φ → BEL.7 ψclassic→ BELa.8 (φ ∨ ψ) ∧ BELa.9 ¬φ ⊃ BELa.7 ψ
Fig. 3.

Σ, ξ, AX AG ξ → Δ
classic
Σ → Δ, ¬ξ ∨ ¬ AX AG ξμR
Σ → Δ, μX.(¬ξ ∨ ¬ AX ¬X)classic
Σ, AG ξ → Δ

ξ1 , ξ 2 → ζξ1 , ξ2 → ζ¬L¬Lξ1 , ξ2 , ¬ζ →
ξ1 , ξ2 , ¬ζ →
XDI-KD
XDI-KD
e1
en
e1
e1
en
en
AX ξ1 , AX ξ2 , X>0 ¬ζ →· · · AX ξ1 , AX ξ2 , X>0 ¬ζ →
Op R
etc.
AX ξ1 , AX ξ2 → AX ζ

Proof of formula (5)Fig. 4.

In addition, we can write some of the strategies for voteof the players on the villagers’ side (if determining which
player to execute is directly linked to winning or losing thenext day, vote for that player) asfollows. Here pos only(e)is the abbreviation for pos(e) ∧ e =e ¬pos(e ) and denotes“choose e as the action”. In this case, we can prove (in asimilar way to the proofs described above, though the proof
is somewhat long) that if BELa.7 seer (player2 ) and formulas(1), (6) hold, then INTENDa.7 pos only(vote for player4 )holds. In addition, if BELa.05 wolf (player2 ) also holds, then
INTENDa.05 pos only(vote for player2 ) is inferred. In thisway, we can express the situation that if someone cannot get acertain belief then (s)he can hardly decide on a single intention.
In the original BDI model, such situation cannot be expressed(an agent always chooses a single intention for one goal at atime).

Parts of proof of formula (8) ∧ (9) ⊃ (3)explain the behavior of player6 in the actual play. Formula(10) represents this behavior.
DESIREplayer6∀x(human(x) ⊃ BELx ¬wolf (player2 ))(10)

D. State transitionHere we abbreviate μX.( a∈A BELa (φ ∧ X)) as M-BELφ(φ is a mutual belief among all agents) and μX.(φ∧ψ∨¬ψ∧AXX) as A(φ N ψ) (φ holds the next time ψ holds; N is regarded
as the “atnext” operator).
Thus far, we have used the AX operator to denote “the nextday”. However, to capture the process of modifying beliefs byagents’ speech acts, a state transition caused by each speech
act has to be described. So, from here on, we will use theAX operator to denote the progress of one step in the game,e.g. one speech act of an agent, vote for execution, start of a
new day, etc. In this case, “φ will hold the next day” can be
written as A(φ N daystart) where daystart is “a new day has
just started”.

BELap AX(executed (playerN ) ⊃ village win) ⊃(6)
INTENDap pos only(vote for playerN )BELap AX(¬executed (playerN ) ⊃ village lose) ⊃(7)
INTENDap pos only(vote for playerN )In this game, as player2 is actually a lunatic, the villagers’side loses in the course of formula (3). If there was a player
who emphasized the possibility that player2 was a lunatic andhad a belief like BELa<.5 (wolf (player2 ) ∨ seer (player2 )),then through a process like formula (3), the chances that
player2 is a seer would be low for him/her, and (s)he would
have chosen a different way of voting.

We treat speech acts as events. However, syntactically, theset of events has to be ﬁnite (Sec. II-A). For this reason (andfor simplicity), we choose some sufﬁciently large ﬁnite set SAof formulas, and limit the set of the contents of the speech acts
to SA.
Again for simplicity, we will consider only the “inform”
type of speech acts deﬁned in FIPA[8]. We write “agent a saysφ (∈ SA) to the set of agents A” as inform(a, A, φ) and treat
this as an event. (From the aspect of the implementation, alogic programming language such as Prolog often does sucha thing, i.e. treats a formula as data.) If A = A (the set of
all agents), we simply write inform(a, φ) (this is a common
case in the Werewolf game). We assume that each agent works
so as to satisfy the following formula (where done(e) denotes“event e has just occurred”):
inform(a,φ)∈E (pos(inform(a, φ)) ⊃AXinform(a,φ) M-BELdone(inform(a, φ)))(11)

C. Nested mental state operators
A belief of an agent that “if player2 is a lunatic, then the
werewolf is very likely to know it”, which was previously
referred to, can be represented as formula (8) by using nested
mental state operators. Here σ is ∀x(wolf (x) ⊃ BELx lunatic(player2 )). In addition, a belief that “the next day, if σ holds,
then villagers’ side will lose unless player2 is executed” canbe represented as formula (9). We can prove that (3) can beinferred from formula (8) and (9). We will omit the details of
the proof, but some small fragments of the proof is shown in
Fig. 4 (where E = {e1 , · · · , en }).

i.e. when someone says something, the fact that (s)he says so
becomes a common belief. We also assume that the following
formula holds; when an agent a intends to do the action e, thene is actually executed. This is regarded as a basic property of
BDI agents.
a(12)e∈E (INTEND pos only(e) ⊃ pos only(e))

BELa.8 (lunatic(player2 ) ⊃ AG σ)(8)
BELa AX(σ ∧ ¬executed (player2 ) ⊃ village lose) (9)It is also possible to handle an agent’s desires and intentions about other agents’ mental states. Here, if the werewolf
actually knows that player2 is a lunatic, (s)he can lead thegame into a win for the werewolves by making other players
not vote for player2. In the situation described above, to doso, one can state that player2 is not a werewolf. This can

When an agent hears someone say something, (s)he decides
whether to modify his/her belief in his/her own way. Here11

Va∈A BELa(done() ∧ M-BELdone()) → BELa done()be realized, by outputting its thought processes and decision
making during the game, we can enjoy looking back on
episodes in the game after it has ﬁnished.

μL
M-BELdone() → BELa done()XDI-KD etc.
aAX M-BELdone() → AX BEL done()classic
etc.
pos only(), pos() ⊃ AX M-BELdone() → AX BELa done()Fig. 5.

Apart from the application to the Werewolf game, there
have been studies on extended BDI model with probabilistic
mental states. For instance, Ma et al.[10] propose a frameworkfor probabilistic plan selection under beliefs with uncertainty.
Coelho et al.[11] proposes an integration of symbolic and probabilistic approaches for agent programming on Jason[12], aninterpreter and development environment for AgentSpeak(L).
However, unlike these studies, our approach is logic-based
and thinking processes including probabilities are directly
expressed as deductions. This feature is considered to besuitable for applications that require logical thought.

Part of proof of formula appeared in Sec. III-D

we assume that when player6 says (φ ⊃ ψ) ∧ ¬ψ (whereφ ≡ wolf (player2 ) and ψ ≡ ∃x support(x)), some player a
accepts φ ⊃ ψ with certainty level  0.9 and ¬ψ with certainty
1. That is, a runs so as to satisfy formula (13) described below,
where  is an event inform(player6 , (φ ⊃ ψ) ∧ ¬ψ).
BELa done() ⊃ BELa.9 (φ ⊃ ψ) ∧ BELa ¬ψ(13)∀x∀t(BELarp wolf (x) ∧ mod bel ∧ time(t) ⊃A(BELarp wolf (x) U ρ))(14)where ρ ≡ (mod bel ∧ ∃t (time(t ) ∧ t < t ))V.

Using an extended BDI logic with probabilistic mental
states, we attempted to describe the processes of decision
making with probabilistic intentions, and prove certain properties of players in the Werewolf game. Our future work will
include developing an algorithm to generate goal candidates
to be inferred and to infer those goals in a realistic amount oftime, as described in Sec. IV, with the ultimate goal being
the realization of a logic-based Werewolf agent. From the
aspect of logic systems, we should also take into account the“realism” property (→ Sec. II) and prove the completeness of
TOMATOes -P .

Additionally, we assume that a runs so as to satisfy
also formula (14) described above, where time is a system
predicate to get the current time, and that when a wants tomodify his/her belief about the werewolf because (s)he has
gotten a new information, (s)he makes mod bel hold. Here r is
an arbitrary comparison operator and p is an arbitrary elementof [0, 1]. In other words, an estimate about the werewolf isretained over time until a attempts to modify it by making
mod bel hold.
Suppose that a is neutral about the success or failure of φ,i.e. BELa=.5 φ. If player6 satisﬁes θ and θ ⊃ INTENDplayer6
pos only() where θ is formula (10) and  is an event
described above, then the event  occurs. Accordingly, BELa.1
φ holds the next time (by formula (4)), and if a makes mod bel
hold at the same time, this belief is retained until anotherestimation is obtained. Regarding these beliefs as states, we
can express the process of state transitions caused by anotheragent’s speech act in this way.

R EFERENCES[1] H. Osawa, F. Toriumi, M. Inaba, D. Katagami, K. Kajiwara, andK. Shinoda, “Agent’s reasoning model for achieving aiwolf,” in Proc. of
19th Game Programming Workshop, 2014, pp. 157–161, (In Japanese).
[2] N. Nide and S. Takata, “Stochastic strategy of agents with uncertain
beliefs and BDI model,” in Proc. of 30th Annual Conference of JSAI,
2016, (In Japanese).
[3] N. NIDE, S. Takata, and M. Fujita, “BDI logic with probabilistictransition and ﬁxed-point operator,” in Proc. of CLIMA ’09, 2009, pp.
71–86.
[4] A. S. Rao and M. P. Georgeff, “Modeling rational agents within a BDIarchitecture,” in Readings in Agents, M. N. Huhns and M. P. Singh,
Eds. Morgan Kaufmann, San Francisco, 1997, pp. 317–328.
[5] N. Nide, S. Takata, and M. Fujita, “Modeling cooperative actions using
an extended BDI logic TOMATOes ,” Transactions of the JapaneseSociety for Artiﬁcial Intelligence, vol. 26, no. 1, pp. 13–24, 2011, (InJapanese).
[6] A. Tarski, “A lattice-theoretical ﬁxpoint theorem and its application,”
Paciﬁc Journal of Mathematics, vol. 5, pp. 285–309, 1955.
[7] AI Werewolf Project, “Are you an AI? TYPE-S,” http://aiwolf.
org/control-panel/wp-content/uploads/2016/03/YASAI2015
0930_Short.pdf, 2016, (In Japanese).
[8] IEEE Foundation for Intelligent Physical Agents, “FIPA communicative act library speciﬁcation,” http://www.fipa.org/specs/
fipa00037/SC00037J.html, 2002.
[9] K. Kajiwara, F. Toriumi, M. Inaba, H. Osawa, D. Katagami, K. Shinoda,
H. Matsubara, and Y. Kano, “Development of AI wolf agent using SVM
to detect werewolves,” in Proc. of 30th Annual Conference of JSAI,
2016, (In Japanese).
[10] J. Ma, W. Liu, J. Hong, L. Godo, and C. Sierra, “Plan selection forprobabilistic BDI agents,” in Proc. of ICTAI 2014, 2014, pp. 83–90.
[11] F. Coelho and V. Nogueira, “Probabilistic selection in AgentSpeak(L),”Computer Research Repository, vol. abs/1409.3717, 2014.
[12] R. H. Bordini, J. F. Hübner, and M. Wooldridge, Programming MultiAgent Systems in AgentSpeak using Jason. John Wiley & Sons, 2007.

We can prove θ ∧ (θ ⊃ INTENDplayer6 pos only()) ∧formula (12) ∧ (11) ∧ AG (13) ⊃ AX BELa.1 φ. The proof ofthis formula is again omitted, but we show a small fragmentof the proof in Fig. 5. We can also prove AX BELa.1 φ ∧ AG
(formula (14)) ⊃ AX ∀t(mod bel ∧ time(t) ⊃ A(BELa.1 φ U
ρ)).
IV.

C ONCLUSIOND ISCUSSION

In this paper, we only showed that an inference rule canbe used to prove some properties. In general, the existenceof a deduction system does not mean the existence of analgorithm which infers goals efﬁciently. To create a logic-based
practical AI Werewolf engine, we need to devise an algorithm
to generate goal candidates to be inferred and infer those goals
in a realistic amount of time. It might be desirable to have an
ability to exclude goals which are not likely to hold from thecandidates, instead of ensuring completeness.
There have already been a number of attempts to realizean AI Werewolf; some of them use machine learning. For
example, [9] uses SVM to estimate werewolves. However, one
can imagine that the best part of the Werewolf game is enjoying
the process of logical thinking rather than being concerned
about winning or losing. Given such a stance, one can expectthat if a logic-based AI Werewolf engine with enough skill can
12