ＡＵＶ心智邏輯

摘 要：為了表示和處理AUV（Autonomous Underwater Vehicle，自治水下機(jī)器人）的心智狀態(tài)及心智活動(dòng)，對Rao和Georgeff的BDI邏輯進(jìn)行了拓展，定義了一種含模態(tài)詞（信念、目標(biāo)、能力、意圖、上一次、下一次、曾經(jīng)、將會(huì)、總有、總會(huì)）的一階模態(tài)時(shí)態(tài)混合邏輯系統(tǒng)——AML（AUV心智邏輯）；基于Kripke可能世界語義模型給出了AML語義，構(gòu)造了AML公理系統(tǒng)及演繹規(guī)則，并證明了AML的可靠性與完備性。AML為建造AUV心智模型提供了有力的表示和處理工具，彌補(bǔ)了Agent理論在機(jī)器人應(yīng)用上的一道鴻溝。

關(guān)鍵詞：自治水下機(jī)器人； 智能體； BDI； 心智邏輯

中圖法分類號(hào)：TP24 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1001-3695(2006)10-0186-03

AUV Mental Logic

LIU Haibo，GU Guochang，SHEN Jing，KONG Xiaodong

(College of Computer Science Technology， Harbin Engineering University， Harbin Heilongjiang 150001， China)

Abstract:In order to represent the mental states and process the mental actions of AUV， this paper extends the BDI logic that proposed by Rao and Georgeff. Combining modal logic and temporal logic， a firstorder logic system， called AML (AUV Mental Logic)， with modal operators such as BEL， GOAL， CAP， INT and temporal operators such as L， N， P， F， H， and G， is defined. The AML semantics is given based on Kripke’s possible world semantic model. The AML axioms and rules are constructed and the soundness and the completeness of the system are proved. AML can be a powerful approach to construct AUV mental model， which will bridge the gap between the agent theories and their applications in robotics.

Key words： Autonomous Underwater Vehicle (AUV); Agent; BeliefDesireIntention (BDI); Mental Logic

Minsky在1986年出版的《The Society of Mind》一書中提出了Agent[1]。盡管Agent目前尚未有一個(gè)統(tǒng)一的定義，但因其卓越的主動(dòng)性（Proactiveness）、自治性（Autonomy）、反應(yīng)性（Reactivity）和社會(huì)性（Sociability）依然得到了蓬勃發(fā)展。AUV（Autonomous Underwater Vehicle，自治水下機(jī)器人）技術(shù)中亦引入了Agent理論[2，3]，即或?qū)UV個(gè)體抽象為Agent以實(shí)現(xiàn)AUV群體協(xié)作，或?qū)UV控制系統(tǒng)用MAS描述以實(shí)現(xiàn)控制系統(tǒng)內(nèi)部協(xié)調(diào)。目前的研究工作更多地強(qiáng)調(diào)和應(yīng)用了Agent表現(xiàn)出的外部特性，卻未真正探討和實(shí)現(xiàn)與外部特性相對應(yīng)的內(nèi)部表示和處理機(jī)制問題，AUV心智狀態(tài)和心智活動(dòng)的研究工作尚未見報(bào)道。

為了適應(yīng)環(huán)境變化和實(shí)現(xiàn)協(xié)作求解，AUV必須利用知識(shí)和感知信息修改內(nèi)部狀態(tài)，即心智狀態(tài)。在心理學(xué)上，心智狀態(tài)是指人的知識(shí)、信念、能力、意向、期望、動(dòng)機(jī)、選擇、承諾、目標(biāo)、策略等心理范疇。AUV的心智狀態(tài)為AUV如何行動(dòng)提供了一種解釋，也就是說AUV的行動(dòng)是由AUV的心智狀態(tài)驅(qū)動(dòng)的。從心理學(xué)觀點(diǎn)看[4]，人類心智狀態(tài)的主要要素有：①認(rèn)知（信念、學(xué)習(xí)、知識(shí)等）；②情感（愿望、偏好、興趣等）；③意向（目標(biāo)、意圖、規(guī)劃、承諾等）。在Agent模型理論中，人們側(cè)重研究信念（Belief）、愿望（Desire）、意圖（Intention）的關(guān)系和形式化描述，建立了BDI模型[5]。

本文結(jié)合近年來Agent理論的研究成果，以AUV為應(yīng)用背景，在Rao和Georgeff的BDI邏輯[6]基礎(chǔ)上拓展出AUV心智邏輯（AML）。

1 AML語形

為了表示AUV心智狀態(tài)中的信念、目標(biāo)、能力、意圖及時(shí)間概念，本文對BDI邏輯進(jìn)行了拓展，定義了一種含模態(tài)詞BEL（信念），GOAL（目標(biāo)），CAP（能力），INT（意圖）與L（上一次），N（下一次），P（曾經(jīng)），F(xiàn)（將會(huì)），H（總有），G（總會(huì)）的一階模態(tài)時(shí)態(tài)混合邏輯系統(tǒng)——AUV心智邏輯（AML）。

定義1 AML語言（簡記為La）的構(gòu)成為

（1）個(gè)體常項(xiàng)：c1， c2， c3…

（2）個(gè)體變項(xiàng)：x1， x2， x3…

（3）謂詞符號(hào)：P1， P2， P3…

（4）連接詞：，∨

（5）心智模態(tài)詞：BEL， GOAL， CAP， INT

（6）時(shí)態(tài)模態(tài)詞：L， N， P， F， H， G

（7）量詞：， 

（8）括號(hào)：(， )

定義2 La的公式定義為

（1）謂詞原子公式是La的公式；

（2）若φ和ψ是La的公式，則φ，(φ∨ψ)，xφ，xφ和X(φ)均是La的公式，其中X為定義1中給出的任一模態(tài)詞，公式最外層的括號(hào)可以省略；

（3）有限次應(yīng)用（1）和（2）構(gòu)成的非空符號(hào)串是La的公式。

定義3 為便于表達(dá)，擴(kuò)充∧和→兩個(gè)連接詞：

（1）φ∧ψ=def (φ∨ψ)

（2）φ→ψ=def φ∨ψ

本文將不含變項(xiàng)的公式稱為陳述語句。AUV的心智狀態(tài)中，信念、愿望、意圖均為陳述語句集，能力為三元組（s，a，g）的集合，其含義為：AUV有能力在狀態(tài)s采取動(dòng)作a達(dá)到目標(biāo)g，其中s和g均為陳述語句，a為標(biāo)志動(dòng)作名字符串。

2 AML語義

AML語義借助Kripke可能世界語義模型[7]給出，其模型由八元組 M = ( S， T， D， V， B， G， C， I ) 構(gòu)成。其中S為狀態(tài)集；TSZ，即從整數(shù)集Z到狀態(tài)集S的映射的集合，T中的任一元素σ稱為狀態(tài)序列，將它用來反映狀態(tài)隨時(shí)間的變化情況；D為個(gè)體域；VΦ×T×Z→{0，1}為對原子公式的真值指派，Φ為原子公式集；BT×Z×T為信念的可達(dá)關(guān)系；GT×Z×T為目標(biāo)的可達(dá)關(guān)系；CT×Z×T為能力的可達(dá)關(guān)系；IT×Z×T為意圖的可達(dá)關(guān)系。AML中的滿足關(guān)系可遞歸定義如下：對任何σ∈T，i∈Z，Pk(x1，x2，…，xn)∈Φ為原子公式，φ，ψ為La的公式，有

（1）M，σ，i，V╞Pk(x1，x2，…，xn)當(dāng)且僅當(dāng)V(Pk(x1，x2，…，xn)，σ，i)=1

（2）M，σ，i，V╞φ當(dāng)且僅當(dāng)M，σ，i，V╞φ不成立

（3）M，σ，i，V╞φ∨ψ當(dāng)且僅當(dāng)M，σ，i，V╞φ或M，σ，i，V╞ψ

（4）M，σ，i，V╞φ∧ψ當(dāng)且僅當(dāng)M，σ，i，V╞φ且M，σ，i，V╞ψ

（5）M，σ，i，V╞φ→ψ當(dāng)且僅當(dāng)M，σ，i，V╞φ或M，σ，i，V╞ψ

（6）M，σ，i，V╞BEL(φ)當(dāng)且僅當(dāng)對任何σ′∈T，若(σ，i，σ′)∈B，則M，σ′，i，V╞φ

（ 7）M，σ，i，V╞GOAL(φ)當(dāng)且僅當(dāng)對任何σ′∈T，若(σ，i，σ′)∈G，則M，σ′，i，V╞φ

（ 8）M，σ，i，V╞CAP(φ)當(dāng)且僅當(dāng)對任何σ′∈T，若(σ，i，σ′)∈C，則M，σ′，i，V╞φ

（ 9）M，σ，i，V╞INT(φ)當(dāng)且僅當(dāng)對任何σ′∈T，若(σ，i，σ′)∈I，則M，σ′，i，V╞φ

（10）M，σ，i，V╞L(φ)當(dāng)且僅當(dāng)i=0或M，σ，i-1，V╞φ

（11）M，σ，i，V╞N(φ)當(dāng)且僅當(dāng)M，σ，i+1，V╞φ

（12）M，σ，i，V╞P(φ)當(dāng)且僅當(dāng)存在i′∈Z，i′

（13）M，σ，i，V╞F(φ)當(dāng)且僅當(dāng)存在i′∈Z，i′≥i，M，σ，i′，V╞φ

（14）M，σ，i，V╞H(φ)當(dāng)且僅當(dāng)對任何i′∈Z，i′

（15）M，σ，i，V╞G(φ)當(dāng)且僅當(dāng)對任何i′∈Z，i′≥i，M，σ，i′，V╞φ

（16）M，σ，i，V╞xφ當(dāng)且僅當(dāng)對任何d∈D，M，σ，i，V(x/d)╞φ

（17）M，σ，i，V╞xφ當(dāng)且僅當(dāng)存在d∈D，M，σ，i，V(x/d)╞φ

3 AML公理與規(guī)則

AML公理集A由標(biāo)準(zhǔn)謂詞邏輯系統(tǒng)的公理擴(kuò)充以下公理構(gòu)成（φ，ψ和X定義同上）：

A1 GOAL(φ) → BEL(F(φ))

A2 INT(φ) → GOAL(φ)

A3 INT(N(φ)) → N(φ)

A4 INT(φ) → BEL(INT(φ))

A5 GOAL(φ) → BEL(GOAL(φ))

A6 INT(φ) → GOAL(INT(φ))

A7 L(φ) → BEL(L(φ))

A8 INT(φ) → F(INT(φ))

A 9 CAP(φ) → BEL(F(φ))

A10 GOAL(φ) → CAP(φ)

A11 CAP(φ) → BEL(CAP(φ))

A12 GOAL(φ) → CAP(GOAL(φ))

A13 INT(φ) → CAP(INT(φ))

A14 G(φ→ψ) → (G(φ)→G(ψ))

A15 H(φ→ψ) → (H(φ)→H(ψ))

A16 G(φ)→φ

A17 H(φ)→φ

A18 L(φ)→P(φ)

A19 N(φ)→F(φ)

A20 φ→H(F(φ))

A21 φ→G(P(φ))

A22 P(φ)→H(F(φ)∨φ∨P(φ))

A23 F(φ)→G(P(φ)∨φ∨F(φ))

A24 P(φ)→G(P(φ))

A25 F(φ)→H(F(φ))

A26 F(φ)→F(F(φ))

A27 G(φ∧φ)

A28 H(φ∧φ)

A29 X(xφ)→xX(φ)

A30 xX(φ)→X(xφ)

A31 X(xφ)→xX(φ)

A32 xX(φ)→X(xφ)

推理規(guī)則：

R1若φ和φ→ψ則ψ

R2若φ則xφ

AML公理和規(guī)則可作用于AUV的心智狀態(tài)集上，描述心智活動(dòng)。

4 AML的可靠性與完備性

4．1 AML可靠性

引理1 對任意公式φ和模型M，有

（1）若φ∈A，則M╞φ；

（2）若M╞φ且M╞φ→ψ，則ψ；

（3）若M╞φ，則xφ。

證明從略。

定理1 （AML可靠性定理）若├φ，則M╞φ。

證明：若├φ，則存在AML中的證明序列φ1，φ2，…，φn，使得φn=φ。施歸納于證明長度n：

（1）n=1，則φ∈A，由引理1（1）知M╞φ；

（2）設(shè)n1）時(shí)有M╞φ，則對n=k時(shí)有下列三種情況：

① φ∈A，由引理1（1）有M╞φ；

② φ是由φi和φj運(yùn)用R1推出的，φj=φi→φ，且i，j

③ φ形為xφm，是φm運(yùn)用R2推出的，m

由定理1（1）和定理2（2）可知，若├φ，則M╞φ，證畢。

4．2 AML完備性

為證明AML的完備性，事先需要作一些準(zhǔn)備。

定義4 EM形式遞歸定義如下:

（1）若x在公式φ中有自由出現(xiàn)，則稱公式xφ是一個(gè)0階的EM形式；

（2）若φ是一個(gè)n階EM形式，ψ是一個(gè)La公式，則X(ψ)→X(φ∧ψ)是一個(gè)n+1階的EM形式，其中X為定義1中給出的任一模態(tài)詞。

定義5 EM公式遞歸定義如下:

（1）若xiφ(xi)是一個(gè)EM形式，xj在φ中不出現(xiàn)，用xj取代φ中xi的每一次自由出現(xiàn)所得的公式為φ(xi)，則稱xiφ(xi)→φ(xj)是一個(gè)相對于xj的EM公式，并稱此EM公式具有EM形式xiφ；

（2）若φ是一個(gè)相對于xj的EM公式，且具有EM形式φ′，ψ是一個(gè)La公式，且xj在ψ中不出現(xiàn)，則稱X(ψ)→X(φ∧ψ)是一個(gè)相對于xj的EM公式，并稱這一公式具有EM形式X(ψ)→X(φ′∧ψ)。

定義6 若EM公式φ具有n階EM形式，則稱φ是一個(gè)n階EM公式。

定義7 Г是AML中的一個(gè)公式集，若對每一個(gè)EM形式均存在至少一個(gè)具有該形式的EM公式屬于Г，則稱公式集Г具有EM性質(zhì)。

定義8 設(shè)φ是AML任一公式，{φ1，φ2，…，φn}是任一有窮公式集，Г是任一無窮公式集:

（1）φ是AML相容的，當(dāng)且僅當(dāng)├/φ；

（2）{φ1，φ2，…，φn}是AML相容的，當(dāng)且僅當(dāng)φ1∧φ2∧…∧φn是AML相容的；

（3）Г是AML相容的，當(dāng)且僅當(dāng)Г的任意有窮子集是AML相容的。

定義9 設(shè)Г是AML的任一公式集，稱Г是AML極大相容集，當(dāng)且僅當(dāng)Г是AML相容的，并且對任意公式φ，若Г∪{φ}是AML相容的，則φ∈Г。

引理2 Σ是AML相容的非空公式集，φ是一個(gè)相對于xj的EM公式，且xj在Σ的任何公式中均不出現(xiàn)，則Σ∪{φ}是AML相容的。

引理3 若φ是AML相容的，則存在具有EM性質(zhì)的AML極大相容集Г，使得φ∈Г。

引理4 若φ是AML的任意公式，Г是具有EM性質(zhì)的AML極大相容集，則存在模型M=(S， T， D， V， B， G， C， I)在每一個(gè)狀態(tài)序列σ∈T和時(shí)刻i∈Z，有φ∈Г當(dāng)且僅當(dāng)V(φ，σ，i)=1。

引理2~引理4的證明請參閱文獻(xiàn)[8]。

定理2 （AML完備性定理）若M╞φ，則├φ。

證明：用反證法。假設(shè)M╞φ但├/φ，則φ是AML相容的，由引理4，存在模型M=(S， T， D， V， B， G， C， I)中的狀態(tài)序列σ∈T和時(shí)刻i∈Z，使得V(φ，σ，i)=1，因而V(φ，σ，i)=0，即M|≠φ，與假設(shè)中M╞φ矛盾，因此有，若M╞φ，則├φ。證畢。

5 結(jié)論

本文基于BDI邏輯拓展出了由模態(tài)邏輯和時(shí)態(tài)邏輯組合而成的一階謂詞邏輯系統(tǒng)——AML，它可用于建立AUV心智模型，詳細(xì)闡述了AML的語形、語義、公理和演繹規(guī)則并給出了系統(tǒng)可靠性和完備性證明。AML未采用K公理和N規(guī)則，因而不存在一般BDI邏輯中的邏輯全知問題和副作用問題[10]，這對資源有限的AUV來說是適用的、合理的。我們采用Visual C++ 6.0在CADCON仿真環(huán)境下實(shí)現(xiàn)了具備信念、愿望、能力、意圖等心智狀態(tài)以及學(xué)習(xí)、承諾、規(guī)劃等心智活動(dòng)的AUV，并與未建立心智模型的AUV進(jìn)行穿越水雷區(qū)對比實(shí)驗(yàn)。仿真結(jié)果表明，前者表現(xiàn)出了很好的主動(dòng)性，能夠在未知的三維水下環(huán)境中以較小的代價(jià)規(guī)劃出可行路徑并以較短的時(shí)間成功穿越水雷區(qū)。采用AML描述AUV心智狀態(tài)，表達(dá)能力強(qiáng)，易于處理，可以深入細(xì)致地刻畫AUV的內(nèi)部活動(dòng)機(jī)制，從而令A(yù)UV表現(xiàn)出更出色的特性。

參考文獻(xiàn)：

［1］Minsky M. The Society of Mind[M]. New York: Simon and Schuster， 1986.

［2］Batlle J， Ridao P， Carreras M. An Underwater Autonomous Agent: From Simulation to Experimentation[C/CD]. Dubrovnik， Croatia： Proc. of the 9th Mediterranean Conference on Control and Automation， 2001.

［3］Cruz N， et al. Operations with Multiple Autonomous Underwater Vehicles: The PISCIS Project[C/CD]. Palo Alto， USA： Proc. of the 2nd Annual Symposium on Autonomous Intelligent Networks and Systems， 2003.

［4］莫雷.心理學(xué)[M].廣州:廣東高等教育出版社，2000.

［5］Anand S Rao， Michael P Georgeff. BDI Agents: From Theory to Practice[C]. San Francisco， USA：Proc. of the 1st International Conference on MultiAgent Systems，1995.312-319.

［6］Rao A S， Georgeff M P. Modelling Rational Agents within a BDIArchitecture[C]. San Mateo， USA： Proc. of the 2nd International Conference on Principles of Knowledge Representation and Reasoning， 1991.473-484.

［7］Kripke S. A Completeness Theorem in Modal Logic[J]. The Journal of Symbolic Logic， 1959，24(1): 114.

［8］馮棉.廣義模態(tài)邏輯[M].上海:華東師范大學(xué)出版社，1990.

［9］Chappell S G， et al. Cooperative AUV Development Concept (CADCON) an Environment for Highlevel Multiple AUV Simulation[C]. Durham， USA: Proc. of the 11th International Symposium on Unmanned Untethered Submersible Technology， 1999.112120.

［10］楊鯤，陳建中，孫德剛，等.認(rèn)知邏輯中邏輯全知問題及其解決方法[J].吉林大學(xué)自然科學(xué)學(xué)報(bào)，1999，23(3):40-43.

作者簡介：

劉海波（1976-），男，博士研究生，主要研究方向?yàn)槎嘀悄荏w系統(tǒng)、機(jī)器人智能；顧國昌（1946-），男，教授，博導(dǎo)，主要研究方向?yàn)槿斯ぶ悄芘c機(jī)器人智能；沈晶（1969-），女，博士研究生，主要研究方向?yàn)槎嘀悄荏w強(qiáng)化學(xué)習(xí)、人工免疫系統(tǒng)、機(jī)器人智能；孔曉東（1982-），男，碩士研究生，主要研究方向?yàn)橹悄芟到y(tǒng)體系結(jié)構(gòu)。

注:本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文