BDI逻辑的心理状态一致性扩展及其可靠性和完备性

140理论计算机科学电子笔记70第5期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html13页扣除系统具有心理状态一致性的NIDE Naoyukia，1 Shiro Takatab，2 Tadashi ARARAGIc，3a奈良女子日本奈良县奈良市北宇屋西町630-8506bATR媒体信息科学实验室Hikaridai 2 - 2cNTT通信科学实验室Hikaridai 2-摘要Rao等人介绍的BDI逻辑，已被用作理性代理的具体化和实现的理论基础。我们研究的目的是充分利用BDI逻辑作为理性主体的可执行规范语言的表达能力。为此，我们以前提出的演绎系统基于CTL的命题BDI逻辑使用微积分。由于这些系统具有从Wang算法扩展的决策算法，因此它们适合于诸如自动证明之类的应用。然而，他们不包括心理状态的一致性特征，这是重要的处理理性的代理人。在本文中，我们通过引入心理状态一致性特征来扩展我们的演绎系统，并解释它们的可靠性和完备性。这种方法允许我们检查和证明BDI逻辑描述的理性代理的规范和属性。1介绍BDI逻辑[4]是CTL*[2]的扩展，它引入了CTL* 的一阶谓词变体和模态运算符BEL、INTEND和BDIRE来表示智能体的心理状态或信念-愿望-意图状态它们不仅被用作单主体或多主体环境中理性主体的形式化规范语言[8，4]，而且还被用作实现理性主体的BDI架构[6，7]的基本概念1电子邮件地址：nide@ics.nara-wu.ac.jp2电子邮件地址：shiro@atr.co.jp3电子邮件地址：araragi@cslab.kecl.ntt.co.jp2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。NIDE、TAKATA和 ARARAGI141∨¬¬ ¬ ¬ ¬ ¬¬⊃ ∧⊃∧ ⊃ ⇔ ¬ ¬ ¬ ∨ ¬ ¬∨∨¬为了充分利用BDI逻辑的表达能力，我们的目标是利用它们作为可执行的特定语言的fractional代理（如Prolog的扩展），特别是在BDI架构。作为实现这一目标的第一步，我们之前提出了基于CTL的命题BDI逻辑的演绎系统这些系统，不像希尔伯特式的饶等人。[5]的判决算法，该算法是对Wang算法的扩展因此，它们适用于BDI逻辑描述的规范的自动证明或检查等应用。另一方面，许多未解决的问题，包括扩展我们的系统，以CTL* 为基础的谓词逻辑，引入多代理BDI模态操作者，并纳入心理状态的一致性。特别是，第一个任务需要完成，以处理理性主体的行为在本文中，我们将心理状态的一致性特征纳入到我们的系统中，并提出了他们的健全和完整的演绎系统。这使我们能够应用我们的系统来描述和证明理性主体的属性本文件的结构如下。在第2章和第3章中，我们定义了公式的语法和语义。接下来，在第四章中，我们介绍了心理状态一致性的属性，这被认为是ratio- nal代理人所固有第五章给出了我们的演绎系统，第六章描述了它们的可靠性和完备性。第7章简要介绍了决策算法，最后我们将在第8章讨论未来的工作。2W的定义我们选择并固定一组命题符号P格式良好的公式基于命题CTL的BDI逻辑的（w_s）定义如下。• 如果p∈P，则p是一个w。（在这种情况下，我们称p为原子命题。）• 如果φ和是w s，那么φ、φ、AXφ、A（φU）、E（φU）、BEL（φ）、EURE（φ）和INTEND（φ）也是w s。此外，我们还介绍了以下缩写。true是q q的一个放大（这里，q是P的一个适当选择和固定的元素），false、φ、φ和φ是true的缩写， （（φ）（）），（φ） EXφ、AFφ、EFφ、AGφ和EGφ分别是AXφ、A（真Uφ）、E（真Uφ）、EFφ和AFφ必要时我们用括号来消除歧义。逻辑运算符的优先级顺序为一元运算符（如<$、AX）、。此外，和是左结合的。NIDE、TAKATA和 ARARAGI142CTLB DI3语义在本章中，我们定义了第2章中介绍的公式的语义3.1（BKD45DKD IKD）CTL-结构首先我们选择以下内容。• 可能世界的集合W（W/=W）• 对于W的每个元素w，一个状态集Stw（l= n）和Stw上的二元关系Rw（nStw×Stw）（这里，Rw必须是串行4;也就是说，对于每个t∈Stw，必须有tJ∈Stw满足t Rw tJ）• 对于W的元素w和Stw的元素t的每一对，赋值L（w，t）• 三元关系B，D，I对W，w∈WStw，W（即，B、D、I、W×w∈WStw×W）满足以下条件：如果（w，t，wJ）∈ B且t∈Stw，则t∈STWJ，以及类似的条件f或D和I。我们称元组M= mW，{St w|w∈W}，{R w|w∈W}，L，B，D，IKCTL- 结构。我们不要求对每个t∈Stw，满足t Rw tJ存在，因为我们没有任何时间操作符，回到过去同时满足以下条件：• （B-D）对于每个w∈W，存在满足（w，t，wJ）∈ B的wJ∈W• （B-4）对于每个w，WJ，WJJ∈W，如果（w，t，WJ）∈ B且（WJ，t，wjj）∈ B，则（w，t，WJJ）∈ B• （B-5）对于每个w，WJ，WJJ∈W，如果（WJ，t，w）∈ B且（WJ，t，wjj）∈ B，则（w，t，WJJ）∈ B• （D-D），（I-D）类似于（B-D）或D，I.我们称之为（BKD 45DKDIKD）CTL-结构。 (In下面，我们使用符号BDIX作为（BKD 45 DKD IKD）CTL的缩写。直观地说，状态对应于3.2解释如果w∈W，且Stw 的无穷多个态的级数（ t0， t1，···）满足条件 t0Rwt1，t1Rwt2，···，则我们称这个级数为w上的一条从t0开始的路。4Rao等人。我用“total”这个词来我们通常说一个序关系R是y R x.“BDINIDE、TAKATA和 ARARAGI143CTL⊃ ¬ ⊃¬∼我们定义一个公式φ为真（记为（M，w，t））|= φ），在BDI K中，结构M={Stw|w∈W}，{R w|w∈W}，L，B，D，I，一个世界w∈W，状态t∈Stw，如果满足下列条件• 如果φ是一个本原命题（φ ∈ P），则（M，w，t）|= φ i <$φ ∈ L（w，t）• （M，w，t）|=<$φ i（M，w，t）|= φ• （M，w，t）|= φ i（M，w，t）|= φ或（M，w，t）|=• （M，w，t）|= AX φ i，对于所有tJs. t。 t R wtJ，（M，w，tJ）|= φ• （M，w，t0）|= A（φ U）i对于W上从t0开始的每条路径（t0，t1，.），在路径s. t中存在状态t1。（M，w，t i）|= 0且对于所有j s. t. 0 ≤j

下载后可阅读完整内容，剩余1页未读，立即下载