ノイズを伴う基本行為による目標達成能力の形式的な保証
新出尚之† a)

後藤

勇樹††

藤田

恵†††

高田

司郎††††

Certification of ability to accomplish goals using atomic actions involving noises
by formal method
NIDE, Naoyuki†a) , Yuki GOTO†† , Megumi FUJITA††† , and Shiro TAKATA††††

あらまし 実世界において、ロボットが目標達成に向けて振る舞うためには、行為の誤差に対処して基本行為を遂行できる能力と、それを用いて計画 (プラン) を選ぶことのできる能力を要する。それをモデル化し、目標達成の過程について形式化された議論を行うには、双方の能力を 1 つのモデルで一体的に扱える必要がある。特に、実世界でのノイズを伴う行為の効果をモデル化するには、連続的な確率分布を扱えることを要する。本論文
では、我々が提案した拡張 BDI 論理体系 C-TOMATOes を用いて、実世界ロボットが目標を達成する能力を論理モデルのもとで示す試みについて述べる。
キーワード

実世界, 形式化, 論理, BDI モデル

1. は じ め に実世界で、知能ロボットが目標を達成する振る舞いをある方式によって選んだ振る舞いをとることで目標が達成されることを形式的に保証するなどの応用も、可能となると考えられる。

とるためには、実践的推論などによってプランを立てた以前に著者らは [1] について、基本行為の効果を数式にり選択したりする能力と、そのプランで用いる基本行為

よって形式的に記述することでモデル化し、そのモデルを遂行する能力の双方を必要とする。ここで、ロボット

上で、ロボットが目標を達成することを保証する試みをの移動など基本行為の遂行は、実世界ではセンサ入力の行った [5]。しかしこの試みでは、状態 (ロボットが存在す

ノイズやアクチュエータの精度の問題などに起因する誤る位置) の集合が (すなわち実験場が) 特定の形をしてい差（注 1）を伴うので、それに対処できる必要がある。

ることを用いており、その点で一般性を欠いていた。ま我々はこれまでに、基本行為をセンシングと移動の同た、目標の達成を保証する部分の議論は数学的な議論で時並行 (センサ · モータカップリング) として設計するこ

行われており、振る舞いを決めるメカニズムの部分と一とで、基本行為の誤差による衝突など不測の事態に陥る体化した論理モデルを提供していたわけではなかった。

ことを避け、知覚から規則に基づいて行為選択すること
で振る舞いを決める手法 [1], [2] の提案を行った。

本論文では、我々が提案した、連続的な確率分布を扱える拡張 BDI 論理である C-TOMATOes [6] を用いて、実この提案では、目標を達成するための振る舞いを選ぶ

世界での行為による状態遷移先の連続な分布を表現し、部分は Teleo-Reactive Program [3], [4] に基づき、論理

これによって、実世界での誤差を伴う基本行為による目モデルを用いた推論で行われているため、論理モデルに

標達成能力を形式的に記述した上で、意味論的議論に基よる形式化が可能である。しかし、実世界で目標を達成

づいてではあるが、それを保証する試みについて述べる。

するための振る舞い全体を一体として形式化するには、

特に、BDI モデルを用いることによって、ロボットが目誤差を伴う実世界での基本行為の部分もこの形式化で議標達成のための意図を形成する過程と、実際の目標達成論が行える必要がある。また、それができれば、例えば、の保証とを、単一のモデルのもとで議論できることを示す。事例としては同じく [1] を用いるが、特定の実験場の†奈良女子大学研究院 生活環境科学系, 奈良市

形に依存しない、より一般的なモデルを用いる。

Faculty, Division of Human Life and Environmental Sciences,
Nara Women’s University, Kita-uoya Nishimachi, Nara-shi,

2. 実験でのロボットの目標達成過程

630-8506 Japan††神戸大学大学院 システム情報学研究科, 神戸市
Graduate School of System Informatics, Kobe University, 1-1†††

Rokkodai-cho, Nada-ku, Kobe-shi, 657-8501 Japan

Evo (以下 Qbo と呼ぶ) が、以下の 3 つの基本行為 (図 1)

奈良女子大学大学院 人間文化研究科, 奈良市

によって目標地点 (ターゲットの場所) まで到達する実験

Graduate School of Humanities and Sciences, Nara Women’s
University, Kita-uoya Nishimachi, Nara-shi, 630-8506 Japan††††

著者らは [1] で、TheCorpora 社のロボット Q.bo Lite

近畿大学 理工学部, 東大阪市

を行った。

•

looking Qbo · · · ターゲットの方向を探し、見つFaculty of Science and Engineering, Kinki University, HigashiOsaka-shi, 577-8502 Japana) E-mail: nide@ics.nara-wu.ac.jp（注 1）：表題の「ノイズ」はこの誤差のことを指す。

1

JAWS2015 予稿集

かったか否かの情報と、見つかった場合にはターゲットの実験では行為の誤差ではなく環境の変化 (障害物の設の方向を得る。ロボットは移動しない

置) に基本行為レベルで対応しているが、行為の誤差によ•forward Qbo · · · looking Qbo によってターゲットが見つかっているならばその方向へ、さもなければあらかじめ定められているデフォルトの方向 (これはほぼター
ゲットの方向に初期設定してある) へ、一定の距離進む•

search Qbo · · · forward Qbo と同じ方向を初期方向として、その角度にできるだけ近い、目前に障害物のる壁など障害物との遭遇にも同様に基本行為レベルで対応している。

3. C-TOMATOes
ここでは C-TOMATOes について、最小限の説明を行う。

C-TOMATOes は、一階述語論理に加え、BDI モデルの心的状態 (信念 · 願望 · 意図) を表す様相オペレータ、未来ない方向を見つけ、その方向へ一定の距離進む方向に分岐する時相を表すオペレータを加えて拡張した
search_Qbo

forward_Qbo(ターゲットが見える場合)

様相論理体系で、特に、イベント (C-TOMATOes ではイベントが基本行為にあたる) に伴う状態遷移 (= 1 時刻後への遷移) には、遷移先の確率分布として連続な分布を記ターゲットの方向へ進む

forward_Qbo(ターゲットが見えない場合)
デフォルトの方向へ進む

述できる。主な論理オペレータないし論理式として以下
障害物の
ない方を
見つけて進む

図 1 ロボットの基本行為
Fig. 1 Atomic actions of robot

Qbo は、目標地点に到達するために、looking Qbo と、
forward Qbo か search Qbo のいずれかの行為を交互に行う。forward Qbo は動き出す時点で目前に障害物がなかった場合の行為、search Qbo はあった場合の行為である。
但し forward Qbo と search Qbo は、移動と障害物の知覚を同時並行で行っており、移動開始後に障害物が新たに置かれた、あるいは知覚が誤っていたなどにより、進行途中に障害物に遭遇した場合は、その時点でその行為を中止 (図 2) して次の行為に移る。これにより、基本行為を遂行し続けて衝突などの事態に陥ることを防いでいる。
forward_Qbo

新たに
置かれた

(途中で障害物を置く場合)
中止ターゲットの方向へ進むのようなものがある。下記の中には、C-TOMATOes では
略記として導入されているものもある。

•⊃, ∨, ∧, ¬, ∀x, ∃x · · · ならば · または · かつ · でな

い · 全ての x について · ある x について (結合優先順位は
右 3 つが最高、左ほど低い。なお、BELa など上記以外の単項演算子も結合優先順位は上記の右 3 つと同じ)•

pos(e) · · · その時刻でイベント e が実行可能•

BELa φ, DESIREa φ, INTENDa φ · · · エージェン

ト a は φ を信じる · 願望する · 意図する。特に、イベント

e に対する DESIREa pos(e) や INTENDa pos(e) は「そのイベントを行う未来へ進むことが可能であることを a が願望ないし意図する」ということになり、すなわち「そのイベントの実行を願望する、あるいは意図する」を表す•

Xe@τ φ · · · イベント e による状態遷移先 (i.e. 次時刻) が確率密度関数 τ で分布する。例えば N (x) =√2e−x /2 / 2π (平 均 0、分 散 1 の 正 規 分 布) と す る と 、
Xe@N (x) at(x) は「イベント e による遷移をした直後は、
at(x) を満たす x の値は平均 0、分散 1 の正規分布をす
る」を表す

•

AXe φ · · · イベント e による遷移で行けるどの未

来でも、次の時刻で φ が成り立つ
元の位置

図 2 障害物に遭遇した場合の行為
Fig. 2 Action when encountering obstacle•

AG φ, AF φ, AX φ, A(φ U ψ) · · · どの未来でも、

φ が永久に成り立つ · いつか成り立つ · 次の時刻で成り立つ · ψ が成り立つときまで成り立つ。この他、CTL*の状
態論理式を全て (略記として) 表現可能

Qbo の動作は、以下のようなプログラム (疑似 Prolog
コードで示す) で実現されている (ただし、実際には引数の受け渡しや、カットを用いた最適化などを行っている)。
この手法は、Kowalski らの Logic-based teleo-reactive

program [4] とほぼ同様である。
goal :- looking Qbo, goal’.
goal’ :- found Obstacle, search Qbo, goal.
goal’ :- not found Obstacle, forward Qbo, goal.
その上で、goal を実行して Qbo をターゲットに向かわせ、途中で Qbo の進路上に一旦障害物を置いてターゲッ
トを見失わせる実験を行った。図 3 にその様子を示す。こ2

4. 目標達成可能性の議論に関する準備
ここでは、2. 節の実験での目標達成可能性について C-

TOMATOes で議論するための数学的な準備を行う。
4. 1 行為による目標地点への接近と到達の表現
まず、2. 節の事例に依存せず一般的な目標達成過程について議論できるような表現を整備する。

S を状態集合、D を S 上の確率分布の集合とする。特に、S 中の 1 点 t のみに分布する確率分布 (これは Dirac’s

Delta を用いて表現できる) を δt (∈ D) と書く。
f を D から D への関数とする。直感的には、f はあるノイズを伴う基本行為による目標達成能力の形式的な保証(1) 初期状態(2) 発見したターゲット方向へ進行(3) 障害物が置かれた(4) ターゲットが見えない(5) 障害物を回避(6) ターゲット再発見(7) ターゲット方向へ進行(8) ターゲットに到達

図 3 Qbo の目標達成過程
Fig. 3 Proces that Qbo attains goal

実験は平面で行われたと想定して、4. 1 節での S をユー

行為による状態 (の確率分布) の遷移を表す。
また、d を D から R = {r | r ∈ R, r >= 0} への関数とする。d は直感的には、確率分布 D を与え、D が、到+クリッド平面の有界な部分集合 {x | x ∈ R2 , |x| <= R} とし (R は実験場を表現するのに十分大きな定数、|x| は原達を目的とするある状態 (以下「目標状態」と呼ぶ) にど

点 O と x の間の距離)、また、ロボットの目標状態 (これの程度近いかを返す関数である (d(D) が 0 に近いほど、はある地点であるので、以降「目標地点」と呼ぶ) を原点

D は目標状態に近いところに分布し、また、目標状態 s

O とする。有界性は実世界を考えれば妥当な仮定と言えの 1 点にだけ分布する確率分布 δs に対しては d(δs ) = 0

よう。また、目標地点を O と特定することも、R が十分となるよう d を選ぶものとする)。

大きければ一般性の喪失にはつながらないであろう。

いま、定数 k >= 0 があって、f が次の性質を満たすと行為 forward Qbo, search Qbo による遷移は、いずれもする。
任意の k 0 > k に対しある ε > 0 があって、d(D) >k 0 なる任意の D に対し d(D) − d(f (D)) >=ε

S 上の確率分布全体の集合を D とする。2. 節の各基本(1)

D から D への関数として差し支えないと考えられる。なお、looking Qbo はロボットを移動させないので、本節の議論では考慮しない。

R

これは、「目標状態よりある程度遠い確率分布 D からは、確率分布 D ∈ D に対する d(D) としては、 x∈S |x|2

必ずそれより一定以上目標状態に近い確率分布へ、f をD(x) dx を選ぶ。すると、原点 1 点だけの分布 δO に対用いて遷移できる」を表す。すなわち、f は目標状態へ接しては d(δO ) = 0、また、直感的に O から遠い分布ほど近する行為を表す関数であり、このような f を「接近関d(D) は大きくなって、d は、D の目標地点 O への近さ数」と呼ぶこととする。

を表す関数となる。

このとき、以下は容易である。
［補題 1］ f が接近関数ならば、任意の D と任意の ε >n0 に対し、ある n >= 0 があって d(f (D)) <= k + ε。 

すなわち、いかなる確率分布から出発しても、f による遷移の繰り返しにより、目標状態へ “十分近づく” こと

以下、R2 上の確率分布 p (6∈ D) に対し、p の S への幅
寄せ pS とは、S 上の以下のような確率分布 (∈ D) を指す

ものとする。これは、直感的には p のうち S からはみ出る部分を S の “端に寄せた” 分布と捉えられる。ただし δは Dirac’s Delta である。

ができる。



p(x)

ここで k が 0 でない場合、d(f n (D)) は必ずしも 0 には近づかないが、実世界においては、d(f n (D)) を限りな

pS (x) =く 0 に近づけることにはそれほど意味はなく、k を実際δ(0) ·Z ∞R

r r 
px dr
RR

if |x| < R
if |x| = Rの問題に応じて十分小さくとっておいてそれに近づけば「目標状態に “到達” した」と考えてよいであろう。

4. 2. 1 障害物を置かない場合

また、接近関数でない関数による遷移が有限回混じっ

まず、S 内に一切の障害物がない場合を考える。その場ても結論は同じ、すなわち目標状態へ “到達” できること

合、行為としては forward Qbo が繰り返される。以降、も容易にわかる。

紛れがない限り forward Qbo による遷移の関数を単に f

4. 2 我々の実験のモデル化
ここでは、4. 1 節で導入した表現法を用い、2. 節の事
例での基本行為の形式化を行う。

と書く。

f によりロボットは、基本的には元の位置 µ から O の方向へあらかじめ定められた長さ l だけ離れた点 µ0 (=3

JAWS2015 予稿集lµ − |µ|µ) へ動くが（注 2）、行為の誤差により実際の到達地点は若干ずれる。

め、d(f (δµ )) は d(Dµ0 ,σ2 ) = (|µ| − l)2 + 2σ 2 よりわず
かに小さい値、すなわち (|µ| − l)2 + 2σ 2 − κ と書ける (κここでの「誤差」には、ロボットのアクチュエータの精は正の値、但し S が十分広ければほとんど 0 と見なすべ

度による誤差の他、センサの誤認識 (例えば looking Qbo

き値であろう。従って、これを 0 と見なしても悪影響をの認識が少ない確率でターゲットの存在する方向を若干及ぼさないように今後の議論を展開する)。一方 d(δµ ) =ずらして報告し、その結果ロボットがターゲットと若干違う方向に向かう) なども考えるものとする。そして、そ|µ|2 であり、これらから常に dsub(µ) >= 0 であること、>>
特に |µ| = r ならば dsub(µ) = 2r(|µ| − r) であることをれらの和が正規分布 (あるいはそれで抑えられる分布) を得る。
さて、k = r 2 とし、k 0 > k なる定数 k 0 をとり、d(D) >とるものとしよう。
そこで、実際の到達地点の分布が、正規分布 N (x | µ0 ,022σ I) (i.e. 平均 µ 、共分散がスカラ行列 σ I の 2 次元正規分布。ただし I は 2 次単位行列、以降でも同じ) の S
への幅寄せ N (x | µ0 , σ 2 I)S として表せるとする (図 4、
ただし青線は確率分布の値を表す。ロボットの移動はあくまでも平面上であることに注意)。ここで、パラメータl と σ 2 は以下のように決まるものとしよう。r2 /2 >=sを満たす正定数 r, s があってl = r, σ 2 = s

if |µ| >=rl = |µ|, σ 2 = s|µ|2 /r2otherwise(2)2に近づく)、σ もある大きさに抑えられた定数 (移動の精度はそれなりにある) だが、O に近い範囲では移動の距離も減り、分布のばらつきも減る。目標地点に近ければ移動が短くなること、短い距離ではばらつきが減ること、

.
µ

O
.

|µ| =a02
D(µ) dµ >)。
= (k − k)/(2R
R
R
d(D) − d(f (D)) = µ∈S dsub(µ)D(µ) dµ >= |µ|2 >=aR√
dsub(µ)D(µ) dµ >2r(a−r)D(µ)dµより、
2= |µ| >
√ =a0
2
d(D) − d(f (D)) >= r( a − r)(k − k)/R となる。この右辺は正で、しかも D に依存しない。以上より f は接近関数である。



返すことで、O に “到達” できることが保証される。ここでの k の選択 k = r2 は、目標地点から距離 r 以内 (ロボットが forward Qbo の 1 回で目標地点に到達できる範囲内) の地点付近の分布を「目標地点に十分近い」と見なしたことになる。これは、この問題では十分に小さい値と言えるであろう。

ともに妥当な仮定と言ってよいであろう。

µ′=

k0 より大、および右辺の第 1 項が a より小さいことかR
0ら、第 2 項 >2>
= (k − k)/2、よって S の有界性より

これと補題 1 より、任意の D から出発して f を繰りすなわち、基本的には l は定数 (一定の距離だけ目標地点

N (x | µ′ , σ 2 I)S

k0 なる任意の D を選んだとする。a = (k0 + k)/2 とおく。
RR
d(D) = |µ|2 <a |µ|2 D(µ) dµ + |µ|2 >a |µ|2 D(µ) dµ がまた、4. 1 節で一般的な表現法を用意してから個別の例の議論を行ったことの利点として、f の具体的な形や、あるいは状態集合 S がここでの例と異なるものだった場
合にも、(うまい d をとって) f が接近関数であることをl示せれば、同様の議論ができる。

|µ| ≥ r の場合

4. 2. 2 障害物が出現しうる場合(l = r, σ2 = s)

こちらはラフな議論のみ行う。

.
N (x | µ′ , σ 2 I)S[1] では、障害物を置かない場合の実験の他に、実世界
環境の予期せぬ変化を考慮した実験として、目標地点に
向かって進行中のロボットと目標地点との間に障害物をµ

置き、ロボットが目標物を一旦見失う実験を行った。
′

µ =O

l

|µ| < r の場合(l = |µ|, σ2 = s|µ|2 /r 2 ).

この実験では、障害物を置くのはあらかじめ決められた回数であり、また、障害物の形状は凸であるため、障
害物の凹部分にロボットが迷い込んで脱出できなくなる

図 4 forward Qbo による遷移
Fig. 4 Transition by forward Qbo

ことはない。さらに、障害物の大きさは有限であり、しかもロボットの 1 回あたりの移動距離との比は極端な値ではないことから、障害物に遮られてから有限回の移動

このとき、以下を示そう。
［補題 2］ f は接近関数である。
［証明］ 以後、µ ∈ S に対し d(δµ ) − d(f (δµ )) を dsub(µ)と、また分布 N (x | µ, σ 2 I) を Dµ,σ2 と書く。

R

まず、 x∈R2 |x|2 Dµ,σ2 (x) dx = |µ|2 + 2σ 2 であることに注意しよう。すると、f (δµ ) = (Dµ0 ,σ2 )S であるた
（注 2）：5. 節で用いる C-TOMATOes の不動点オペレータ µ との区別のため、本論文では変数としての µ や µ には直立体を用いる。

4

で、ロボットは目標物の見える地点まで到達できる。
従ってこの場合、forward Qbo で目標物に近づく移動を行う以外の行為 (search Qbo 、または障害物に遮られて止まる forward Qbo) が起こる回数は、有限回であると考えることができる。よって、4. 1 節の議論より、やはりロボットは O に “到達” することができる。
この他、S 内に壁が障害物とは別に (あるいは障害物のノイズを伴う基本行為による目標達成能力の形式的な保証

他に) ある場合も、forward Qbo で目標物に近づく移動

準備として、ある基本行為 e による状態遷移が接近関を行う以外の行為が有限回であることが (壁の形状などか数であるという性質は、式 (1) での定義 (と 4. 2 節での dら) 示せれば、同じ議論ができる。図 4 のように、実験場の定義) を用いてを挟んで十分な幅で平行に壁があるような場合 (実際にはドア部分の凹部があるので、そこにロボットが引っかからないことが保証できれば) がその例である。

4. 3 モデルの意義と限界
ここまでに述べたモデル化では、行為に伴う誤差の種類を必ずしも明確化しなかった。しかし、ロボットの行∀x(at(x) ⊃ Xe@P (x,y) at(y)) ∧R
f = λD.(λy. x∈S D(x)P (x, y) dx) ∧R
d = λD.( x∈S |x|2 D(x) dx) ⊃∀k0 > k ∃ε > 0 ∀D(d(D) > k0 ⊃ d(D) − d(f (D)) >
= ε)

(3)

為の正確さに影響を与える全ての要因に伴う誤差の集積と書ける。ここで、数学記号 (λ を含む) については、通が、4. 2. 1 節で導入したもので表せる (あるいは抑えられ常の数学での解釈を解釈として持つ関数記号や述語記号

る) ならば、ロボットの実際の動作をこのモデルで表現でとして扱うものとする。式 (3) を appr(e) と略記する。

5. 1. 1 障害物を置かない場合

き、その目標達成性を保証することができる。
一方、現実の実験の状況によっては、ここまでに述べたモデルによって十分表現できない場合もある。例えば、

4. 2. 1 節で述べたように、forward Qbo の遷移結果の正規分布には、looking Qbo の認識誤りによりロボットがまず、障害物がない実験の場合は、forward Qbo による遷移は∀x(at(x) ∧ dest(x, µ0 , σ 2 ) ⊃ XfwQ
at(y))@N (y|µ0 ,σ 2 I)

ターゲットと若干違う方向に向かうことの考慮も含めてと書ける。この式を distN(fwQ) とする。なお、ここであるのではあるが、しかし、実際の looking Qbo の認識

dest(x, µ0 , σ 2 ) は、移動元 x から、移動先の平均 µ0 と共率があまり良くなく、全く違う方向にターゲットが存在す

分散 σ 2 を求める述語で、x を用いて式 (2) により定義でると報告する確率が無視できないならば、forward Qbo

きるが、ここでは定義は略する。

の遷移結果も目標地点に近づく正規分布をするとは言えなくなり、モデルでの結果に反し、目標地点への到達可

すると、forward Qbo による遷移が接近関数であることは AG(distN(fwQ) ⊃ appr(fwQ)) と書ける。

能性を保証できないことになる。モデルと実際のロボッ

また、looking Qbo ではロボットは移動しないことは、

トの動作の双方について、互いに近づける努力が今後の

at(x) ⊃ AXlkQ at(x) と表せる。この性質を immov(lkQ)

課題の 1 つである。

と略記する。
さらに、「x が十分に目標地点 O に近い」を near O(x)5. C-TOMATOes による記述で表す (これの定義は省く)。すると、「現在位置が十分

本節では以上の議論をもとに、[1] での実験によるロボッに目標地点 O に近い」は ∀x(at(x) ⊃ near O(x)) で表せ

トの振る舞いを C-TOMATOes で記述する例を与える。なお、記述力を示すため、本節では looking Qbo による遷初めに以下の略記を導入する。一部に C-TOMATOes の
不動点オペレータ µ を用いている。
0

0

def

AXφ?e:e ψ ≡ (φ ⊃ AXe ψ) ∧ (¬φ ⊃ AXe ψ)

これは、「φ なら e を、さもなければ e0 を実行すると、次の時刻には ψ が成り立つ」を表す

•

0

0

def

AFe;e φ ≡ µX.(φ ∨ AXe AXe X)

これは、
「イベ

ント e と e0 の交互実行を繰り返すといつか φ が成り立
def

A(φ, φ0 U ψ) ≡ µX.(ψ ∨ φ ∧ AX(φ0 ∧ AX X))

成性は次のように記述できる。

AG distN(fwQ) ∧ AG(distN(fwQ) ⊃ appr(fwQ)) ∧AG immov(lkQ)⊃ AFlkQ;fwQ at near O
5. 1. 2 障害物が出現しうる場合
この場合、4. 2. 2 節の議論より、search Qbo は有限回し
か実行されず、また、有限回を除いて forward Qbo は障つ」を表す。上の略記と併用することもある•

以上を用いると、障害物がない場合 (looking Qbo とforward Qbo が交互に実行されることになる) の目標達移も無視しない。

•

る。これを at near O と略記する。

こ

害物に遭遇しない。これらのことは、AF AG ¬pos(search

れは、「ψ が成り立つまで φ と φ0 が繰り返し交互に成り

Qbo) および AF AG distN(fwQ) で書ける。従って、障害立つ) を表す

物を伴う実験の場合に成り立つ条件は

5. 1 基本行為による目標達成過程
以 降 、条 件 found Obstacle, 基 本 行 為 looking Qbo,

forward Qbo, search Qbo のそれぞれを論理式中では
fOb, lkQ, fwQ, srQ と表記する (前 1 者は原始論理式、

AF AG distN(fwQ) ∧ AG(distN(fwQ) ⊃ appr(fwQ))∧ AF AG ¬pos(srQ) ∧ AG immov(lkQ)(4)と書ける。この式を ζ とおく。

後 3 者はイベントである)。また、at(x) で「位置 x にいすると、looking Qbo と、found Obstacle が成り立つ

る」を表す (なお、ここからは位置を表す変数にも細字をか否かによって forward Qbo または search Qbo のいず

用いる)。

れかとを交互に実行することでいつかは目標を達することは、次のように記述できる。
5

JAWS2015 予稿集

ζ ⊃ AFlkQ;(fOb?srQ:fwQ) at near O(5)

η の成立のもとで、実際に意図 INTENDa AF at near Oが発生すると、a は 3 種類の基本行為を交替で意図し、これらの式は数学記号を多数使っているため、推論規則を設けてこれらの式を導くことは困難と考えられる。
しかし、意味論的議論を用いてなら、これらの成立を示従ってそれらを実際に実行する。これにより、いつかはat near O を達成することになる。この過程は以下のように書ける。

すことは 4. 節での数学的議論と同じ筋道で行え、この意η ∧ INTENDa AF at near O ⊃ AF at near O

味で、目標達成性を形式的な記述のもとで論じることができている。

また、at near O を達成したときに a がそれを信じること

5. 2 ロボットの意図と目標達成過程の実行
ここまでの議論は「ロボットがこのような一連の行為を実行したら目標を達成する」という性質にとどまり、ロボットが目標達成や行為実行を意図する部分の記述はな
かった。ここでは、ロボットが目標達成を意図し、それを実行する過程の記述を示す。
本行為については意図した時点で実行する (それ以外のイ
ベントは実行不可) というもので、合理的エージェントに要請される性質である。E は全てのイベントの集合 (ここでは {lkQ, fwQ, srQ}) を表す。
e∈E (INTENDVaが成り立つなら、目標地点到達時には、式 (8) 式により基本行為を交替で意図することは止まり、さらに、式 (7)式によりくまの人形を掴む動作に実際に移る。
以上のように、BDI モデルでの心的状態と、結果の連続な分布を伴う遷移の双方を扱うことによって、エージェ

まず、次の式が満たされることを仮定する。これは、基Vができれば、すなわち AG(at near O ⊃ BELa at near O)

ント (ロボット) が目標を達成するための意図を形成し、誤差を伴う基本行為を用いてそれを実行する過程、およ
びそれによる目標の達成可能性を、(その目標をサブゴールとして含むさらに大きな目標の達成過程も含めて) 単一のモデル内で論じることができた。また、特に at near Oの達成の部分は、言い換えれば、誤差を伴うロボットの行

pos(e) ⊃0(6)

為に対し形式的な意味を与えたとも考えることができる。

さて、いま、ロボット (a とする) はくまの人形を入手ては、例えば何らかの知識を用いた振る舞いの選択 (例とpos(e) ∧e0 ∈E,e=e/ 0 ¬pos(e ))双方が単一のモデル内で扱えることにより、発展とし(get bear) したいと願望しているとする。そのために「くして、ターゲットからの帰り道には、行きに得た障害物

まの人形のある場所 (5. 1. 1 節の O) に到達し、それを手に関する知識を使うなど) を表現するなどの応用も可能とで掴む」というプラン (pick bear) があり (今回は簡単のなろう。ここではラフなアイデアを述べるにとどめるが、ためこれしかプランがないものとする)、それを意図とし

fOb ∧ percept obstacle at(x) ⊃ AG BELa obstacle at(x)て選ぶ。この過程は DESIREa AF get bear ⊃ INTENDa

で「障害物に遭遇すればその位置を覚えておく」、帰りpick bear と書け、またプラン pick bear の内容は道にINTENDa pick bear ⊃BELa ∃x obstacle at(x) ⊃INTEND AF at near O ∧achoose obstacle free pos(p) ∧AG(BELa at near O ⊃a

AX INTEND pos(hold bear))

INTENDa AF(at near(p) ∧(7)

AF at near(original position))と表せる (「くまの人形を掴む」はここでは基本行為とで「障害物に当たらない適切な経由地を選択して帰る」な

し、hold bear で表す)。これにより、まず目標地点 O へどが表現できる。

の到達 (at near O) を意図し、その達成を信じればくまの人形を掴む動作に移る。

6. 議

論

目標地点到達を意図したら、その達成を信じるまで、[6] で我々は、連続な確率分布を扱う他の論理体系とlooking Qbo と、found Obstacle が成り立つか否かによっ

C-TOMATOes との比較を行った。それらとは別に、本論て forward Qbo または search Qbo のいずれかとを交互

文と同様に、動作が確率的に記述される過程について、に意図することを実際に行うものとする。これは、2. 節

その性質を論理的に扱おうとする研究としては、例えの擬似 Prolog コードで表された動作である。この部分はば Gupta ら [7] や Cardelli, Mardare ら [8], [9] のものなどがある。前者は、プロセスを一般化セミマルコフ過程

INTENDa AF at near O ⊃A(INTENDa pos(lkQ), ξ U BELa at near O)
ここで

(8)

ξ ≡ (fOb ⊃ INTENDa pos(fwQ)) ∧(¬fOb ⊃ INTEND pos(srQ))aと書ける (交互実行のため、通常の until オペレータでは書けない)。
式 (4)、式 (5)、式 (6) 、および式 (8) の ∧ を η と書く。
6

(GSMP) として扱い、その間に距離を入れることで、プロセス間に双模倣 (bisimulation) に近い関係を入れ、プロセスに関する近似推論を行おうというものである。連続時間を扱えるという、C-TOMATOes にない利点を持つが、逆に GSMP では状態の集合は有限であるため、C-

TOMATOes と異なり状態上の連続的な確率分布は扱えない。後者は、連続マルコフ過程に関する性質を扱う論理ノイズを伴う基本行為による目標達成能力の形式的な保証

体系 CML (Continuous Markovian Logic) を提案していvol.7360, pp.12–32, Lecture Notes in Computer Science,
2012.

る。プロセス間の (確率的な) 双模倣によってプロセスの性質を捉えようとする点は、前者と共通している。健全[5]で完全な公理系を示している点は C-TOMATOes より強いが、ベースは一階述語論理ではなく命題論理であり、ま[6]た、状態空間としては解析空間一般を扱えるものの、C-

TOMATOes のように任意の確率分布を書ける構文はやは[7]

り持たない。

後藤勇樹，藤田 恵，新出尚之，“不確実性に対処可能な Teleoreactive program の意味論とその応用，” 情報処理学会研究報告，no.2，pp.1–6，2014-ICS-173，2014．
新出尚之，高田司郎，藤田 恵，“連続した状態空間での合理的エージェントの行為を扱う論理モデルの試み，” 電子情報通信学会論文誌，vol.J96-D，no.12，pp.2939–2950，2013．
V. Gupta, R. Jagadeesan, and P. Panangaden, “Approximate reasoning for real-time probabilistic processes,”
Logical Methods in Computer Science, vol.2, issue 1,

この他、Clark ら [10] は確率的なプロセス代数を用いて、分散システムに関する性能測定の問題を様相論理で記述し、(確率的な) 検証を行う手法を示している。こち

2006.
[8]

markovian logic — from complete axiomatization to the

らも任意の確率分布を記述する構文はないが、逆に本論

metric space of formulas,” Proc. of CSL11, LIPIcs 12,
pp.144–158, 2011.

文では、目標の達成可能性は論じているものの、[10] と異なり性能についての議論は取り上げていない。例えば、[9]fied metatheory,” Logical Methods in Computer Science,

保証することも重要であろう。C-TOMATOes 自体には、過去には仮想世界でのより簡単な例ではあるが「所定のR. Mardare, L. Cardelli, and K.G. Larsen, “Continuous markovian logics — axiomatization and quanti-

現実的な時間内に十分な確率で目標を達成できることを確率的な状態遷移を扱えるためそうした記述能力はあり、

L. Cardelli, K.G. Larsen, and R. Mardare, “Continuous

vol.8, no.4, 2012.
[10]

G. Clark, S. Gilmore, J. Hillston, and M. Ribaudo, “Exploiting modal logic to express performance measures,”Proc. of 11th International Conference on Computer Per-

回数以内の行為で特定の地点に到達できる確率が低くな

formance Evaluation: Modelling Techniques and Tools,

れば、目標達成を断念する」といった例を示している [6]。

pp.247–261, 2000.

今回は扱っていないが、実世界でのこうした性質を C-

TOMATOes で扱うことは今後の課題の 1 つである。
ただ、ここで比較した研究はいずれも、確率的な動作をするプロセス (群) を単独で対象としての議論であり、エージェントが意思を決定する過程までを含めて単一モデルで議論できるものは見られない。C-TOMATOes は、

BDI モデルと一体化し、単一モデルによって、連続的分
布も含めた確率的なプロセスの動作と、エージェントの意思決定過程とをまとめて扱える点が、これらと比べて特徴的な利点である。

7. ま と め
我々が提案した拡張 BDI 論理体系 C-TOMATOes を用
いて、実世界での誤差を伴う行為による目標達成能力に関する形式化が行えることを、実験を用いた事例により示した。今後は、4. 3 節で示したように、モデルと実験とのマッチングを精密化していく過程を進めることと、そこでの C-TOMATOes の優位性を検証することなどが課
題である。
文
[1]

献

M. Fujita, Y. Goto, N. Nide, K. Satoh, and H. Hosobe,“An architecture for autonomously controlling robot
with embodiment in real world,” Proc. of Knowledge
Representation and Reasoning in Robotics (workshop at
ICLP 2013), pp.59–71, 2013.

[2]

M. Fujita, Y. Goto, N. Nide, K. Satoh, and H. Hosobe,“Logic-based and robust decision making for robots inreal world,” Proc. of AAMAS ’14, pp.1685–1686, 2014.

[3]

N.J. Nilsson, “Teleo-reactive programs for agent control,” Journal of Artificial Intelligence Research, vol.1,
pp.139–158, 1994.

[4]

R.A. Kowalski and F. Sadri, “Teleo-reactive abductive
logic programs,” Logic Programs, Norms and Action,

7