概率动态认识逻辑框架下的符合概率计划推理

0人工智能 268（2019）54-840目录列表可在ScienceDirect上找到0人工智能0www.elsevier.com/locate/artint0一种用于推理符合概率计划的动态认识框架0Yanjun Li a , Barteld Kooi b , Yanjing Wang c , �0a  哲学学院，南开大学，天津300350，中国 b  哲学学院，格罗宁根大学，格罗宁根9712 GL，荷兰c  哲学系，北京大学，北京100871，中国0文章信息摘要0文章历史：2017年2月6日收到2018年7月3日修订稿收到2018年12月5日接受 2018年12月7日在线发布0关键词：符合概率规划 动态认识逻辑0在本文中，我们介绍了一个概率动态认识逻辑框架，可以用于推理和验证单一代理环境中的符合概率计划。在符合概率规划（CPP）中，我们寻找一个线性计划，使得执行该计划后实现目标的概率不低于给定的阈值概率δ。我们的逻辑框架可以追踪代理在执行计划过程中的信念状态的变化，并验证符合计划。此外，通过使用该逻辑，我们可以通过使用动作模态和概率信念在我们的语言中制定目标的公式来丰富CPP框架。至于主要的技术结果，我们提供了逻辑的完全公理化，并展示了其有效性问题的可决定性。0©  2018 Elsevier B.V. 版权所有。01. 引言01.1. 自动规划的背景0自动规划是人工智能的一个分支，涉及制定一个计划，该计划可能是一种策略或一系列动作，以实现代理的目标。自动规划技术广泛应用于各个领域，从控制航天器的操作到玩桥牌游戏[1]。经典规划是自动规划的最简单形式，处理的问题是在确定性转换系统中找到一个线性动作序列，使得在初始状态下执行该计划将实现目标（参见例如[1]）。经典规划有两个重要的简化假设：动作的确定性和完全可观测性。完全可观测性表示对系统和系统起始状态具有完全的知识。0符合规划通过放宽这两个限制来推广经典规划，即允许对系统状态的不知情（以及无法观察到自己的位置）并允许动作是非确定性的。前者意味着初始状态集不再必须是单例集（对应于代理的初始不确定性），但也意味着在执行计划期间无法通过观察获得关于自己位置的确定性。符合计划是一个动作序列，无论计划从哪个初始状态开始，无论（非确定性）计划如何执行，都能保证代理到达目标状态之一[1]。由于0* 通讯作者。0电子邮件地址：lyjlogic@nankai.edu.cn（Y. Li），b.p.kooi@rug.nl（B. Kooi），y.wang@pku.edu.cn（Y. Wang）。0https://doi.org/10.1016/j.artint.2018.12.001 0004-3702/ ©2018 Elsevier B.V. 版权所有。s1: GD0.7s30.3s2 : GD,BHs4 : BHb:0.05a:1b:0.95b:0.5b:0.5a:0.8a:0.2μπ(t) ={s0···sn|∀1≤i≤n:si−1ai→si,sn=t}B(s0) × Pr(s0,a1, s1) × ··· × Pr(sn−1,an, sn)μab(s2)= B(s1) × Pr(s1,a, s1) × Pr(s1,b, s2) + B(s3) × Pr(s3,a, s1) × Pr(s1,b, s2)= 0.7 × 1 × 0.95 + 0.3 × 0.8 × 0.95= 0.665 + 0.228 = 0.8930Y. Li et al. / 人工智能 268（2019）54-84 550符合规划会引出代理的不确定性，因此除了传统的人工智能方法，我们还可以从认识逻辑的角度来看待符合规划。0符合概率规划（CPP）是符合规划的一个重要推广。符合规划对解决方案的要求可能过于严格，因为解决方案必须在所有情况下都能找到。可能的情况是，从这个意义上讲，解决方案是不可能的，而仍然可能存在一些计划以非常高的概率达到目标状态。在CPP中，我们寻找一个线性计划，执行该计划后实现目标的概率不低于给定的阈值概率。CPP的模型包括对初始状态的概率分布以及某个动作导致某个后继状态的概率。0让我们考虑下面的CPP玩具例子。1拿一个可能湿的gripper的机器人。gripper需要拿住一个block，但是在gripper湿滑的情况下抓住block比干燥的情况更困难。这可以用以下具有概率的转换系统来建模，其中气泡表示关于gripper是否干燥的初始不确定性。0有两个命题：GD代表gripper-dry，BH代表block-held，有两个动作：a代表drying，b代表pickingup。请注意，在上面的模型图中（以及所有后续的模型图中），状态上只会提到正命题（例如BH，GD），如果一个命题没有被提到，可以假设它为假。我们通过概率分布B对系统的初始信念状态进行建模，该分布分配以下概率：B(s1) = 0.7和B(s3) =0.3。动作a以概率1使干燥的gripper变干燥，以概率0.8使湿的gripper变干燥。动作b以概率0.95拾取block，如果gripper是干燥的，则以概率0.5拾取block。在这个例子中，不可能找到一个计划，可以保证执行计划后机器人会持有block。然而，为了实际目的，可能找到一个计划以至少90%的概率成功持有block。0CPP在人工智能文献中得到了广泛研究（参见，例如，[2-6]）。通过以下方式计算通过执行计划π = a1 ∙∙∙ an 实现目标状态t的概率（参见[4]）：0其中Pr ( s i − 1 , a i , s i )表示在s i − 1处执行a i 后到达s i 的概率。例如，在滑动gripper的例子中，通过执行ab实现s 2 的概率如下所示：0为了提高持有block的概率，机器人必须（尝试）先将gripper干燥两次。01.2. 动机0为了形式化地捕捉CPP中的概率信念变化，我们提出了一个用于推理关于符合概率计划的单智能体动态认知框架，该框架基于具有概率标记转换和初始状态的概率转换系统作为我们的模型。前面提到的滑动gripper的图是这样一个模型的示例。该模型也是Wang和Li在[7]中用于非概率性动态认知框架的模型的自然概率扩展。然而，概率情况比非概率情况要复杂得多。01 这是[2, 3]中讨论的滑动抓手示例的变体。Moreover, the logical framework presented in this paper could make a contribution to CPP. First of all, by using a powerful logical language we can express more planning goals, such as epistemic goals, by formulas. The logical language can also help us to distinguish different conformant probabilistic plans for the same goal. Our proof system can help to capture the essential reasoning of CPP, where the axioms can reveal the underlying assumptions behind the probabilistic updates. Finally, the proof system also gives us a (syntactic) way to compute final probability after actions in terms of initial ones. We use the following toy example to illustrate our ideas:s10.5s20.5s3s4 : ps5a:0.6a:0.4b:1a:0.2a:0.8μb(p) = 0.5 × 1 + 0 = 0.5μa(p) = 0.5 × 0.8 + 0.5 × 0.4 = 0.6s10.5s20.5s3s4 : ps5a:0.8a:0.2b:1a:0.2a:0.8μb(p) = 0.5 × 1 + 0 = 0.5 = 0.5 × 0.8 + 0.5 × 0.2 = μa(p)0在处理CPP背后的推理时，我们不仅需要跟踪概率信念的更新，还需要处理计划的可执行性的概率。0例1.考虑一个病人在ICU中情况非常危急的场景。医生必须迅速决定该怎么做，没有第二次机会可以改变。现在病人的病因还不确定，可能是s1或s2。如果实际原因是s1，那么治疗b肯定可以挽救病人的生命（p）。然而，如果原因是s2，则b不可执行，但是尝试b可能会浪费宝贵的时间。另一方面，治疗a总是可以执行的，但是它的结果取决于实际原因：如果是s2，成功率为80%，否则成功率只有40%。该情况由以下模型N描述，其中气泡表示对s1和s2的半半（主观）概率分布的初始不确定性：0现在，作为医生，你应该选择哪个行动？0我们可以计算a和b成功实现目标p的概率：0作为一个理性的医生，我们可能会选择a而不是b来挽救病人的生命。0然而，情况可能更加微妙。让我们稍微降低给定s1的a的成功率，并考虑以下模型M描述的情景：0例2.0现在我们有：0在CPP中，我们对a和b是无所谓的。然而，直观上我们仍然有一些理由更喜欢a而不是b：做b意味着如果原因是s2，我们完全没有机会挽救病人，而使用a，无论原因是什么，我们总是有一些机会挽救病人。这可以通过B ϵ � b � p =  0 . 5和B ϵ � a � p =  1来在我们的语言中明确表示（Bϵ可以被视为一种信念运算符）。另一方面，我们也有一些理由更喜欢b而不是a：给定成功执行a的情况下p的概率为0.5，低于给定成功执行b的情况下p的概率为1。这可以通过[a]B ϵ p =  0 . 5和[b]B ϵ p =1在我们的语言中明确表示。这种条件概率可以通过考虑相应行动的更新模型来计算。回顾动态认知逻辑的核心思想是将行动视为模型的更新。直观上，在成功执行给定行动后，代理人沿着该行动标记的转换将气泡向前传递，然后相应地计算新气泡内的新概率分布。在我们的框架中，执行a和b将给出以下模型M | a和M | b（在我们的框架中将被准确地定义）：0Y. Li等/人工智能268（2019）54-84 570因此，尽管μa(p)=μb(p)，但是可能会影响决策的成功概率的更细的分解。正如我们将看到的，我们的语言可以使所有这些都变得明确和严格。0此外，对a优于b的偏好也可以通过具有认知目标来解释：确保（最终）智能体知道p的概率不小于0.5。这可以通过我们的语言中的公式ϕ =Bϵp≥0.5来表示。现在，如果我们根据这个目标重新计算概率，我们有μa(ϕ)=1，但μb(ϕ)=0.5。这是偏好a而不是b的另一个原因。0我们将提供这个逻辑的完整公理化（第4节）。公理化系统揭示了CPP中关于概率信念更新的隐含假设。公理ITSP表明在CPP中，我们假设智能体知道他相信自己相信的东西，也知道他不相信自己不相信的东西。公理CP表明我们假设智能体具有完美的回忆。完美回忆的公式直观地意味着智能体永远不会忘记：如果智能体知道a会使ϕ成立，那么在执行a之后，他确实知道ϕ。此外，基于这个公理化系统，我们证明每个公式都可以等价地转化为一个公式，在该公式中，每个概率模态Bπ永远不会出现在行动模态[a]或其他概率模态Bπ'的范围内。从规划的角度来看，这意味着在计划执行后检查认知公式等同于在初始模型中检查不同的认知公式（参见命题34）。例如，在示例2中，公式[a]Bϵp=0.5等同于Bap=0.5Bϵ�a��。对于公式[a]Bϵp=0.5，我们需要在更新后的模型中检查智能体的信念状态，而对于公式Bap=0.5Bϵ�a��，我们只需要在初始信念状态中检查。在介绍我们框架的细节之后，这将变得清楚。02. 相关工作02.1. DEL方法0动态认知逻辑（Dynamic EpistemicLogic，DEL）是为了模拟由于信息事件而导致的知识和信念的变化而发明的（参见[8]等）。其核心思想是将行动（或事件）视为对认知模型的更新，其中不确定性由系统状态的等价类编码。例如，当一个可信的来源公开宣布命题p时，我们会删除当前等价类中不满足p的状态。近年来，使用DEL处理带有不确定性的规划引起了越来越多的关注（参见[9-16]等）。在符合规划中，为了确保通过执行计划最终实现目标，跟踪信念状态的转换在关键。这就是DEL可以发挥作用的地方，因为DEL可以逐步跟踪信念的变化。例如，在单智能体DEL中，在宣布p的行动之后，初始的不确定集将被更新为一个子集，在每个状态中p都为真。与传统的人工智能方法相比，DEL可以使规划背后的推理更加明确。此外，DEL丰富的语言可以自然地表达认知目标。这对CPP可能会做出实质性贡献。正如示例2所示，成功实现目标p的a和b的概率是相同的，但是我们仍然可以进一步区分对a或b的偏好，正如我们所提到的。0由于传统的CPP是单智能体的，因此我们只关注DEL方法的单智能体情况。单智能体DEL的认知模型是一个不确定性集合，因此，为了处理概率规划背后的推理，我们确实需要用概率扩展DEL，例如概率DEL（PDEL）的工作（参见[17-19]等）。然而，将PDEL与自动化规划，特别是CPP联系起来的工作并不多。我们希望在本文中迈出第一步。我们的逻辑框架受到PDEL思想的启发，但并不是PDEL的标准形式。与我们的工作最相关的DEL风格的工作是[17]中提出和研究的PDEL框架。模型和逻辑语言分别存在两个显著的差异。首先，我们的模型是概率转换系统，而不是PDEL中没有明确行动的概率认知模型。为了用μπ（参见介绍）的术语来表达CPP的要求，我们确实需要模型中的行动（转换）的概率信息。μπ是02 Bπ大致捕捉了动作序列π发生后代理人的概率信念。58Y. Li et al. / Artificial Intelligence 268 (2019) 54–840不仅是关于可能当前状态的概率，还有一个关于由π成功执行的概率加权的状态的概率（从这个意义上说，它更接近先验概率），即：0μπ(t) = Pr(π成功执行) ∙ Pr(给定π执行，t被达到)。0相应地，在语言中，我们有一个模态Bπϕ≥q，它通过允许一个动作序列π（注意这里π可以是ϵ）作为每个模态的索引来推广了[17]中的模态，以表达通过π达到某个目标的概率。在PDEL中，我们只能表达当前状态中某个命题为真的概率，即Bϵϕ≥q。02.2.规划中的约简和回归0DEL方法通常还附带一个使用所谓的约简公理的证明系统，该公理在语法上将动作之后的信念与动作之前的信念相关联，并可以递归地消除动作模态。例如，在[17]中，公式[! p] B ϕ = 0.5（这意味着在动作p成功宣布为真的情况下，ϕ的代理人的信念程度为0.5）可以等价地约简为B（p ∧（p → ϕ））=0.5Bp。通常情况下，任何公式都可以等价地约简为一个没有动作模态的公式。因此，在执行一系列动作之后检查认知目标可以简化为在初始模型上检查一些纯粹的认知公式。约简公理通常会引发一种消除语言中动作模态的方法。从规划的角度来看，我们可以使用这种技术将在执行计划后检查公式的问题转化为在初始模型上检查不同公式的问题。这与使用情境演算的回归方法在规划中有一个明显的自然联系（参见，例如，[20,21]），这在DEL文献中也得到了解决（参见，例如，[22]）。然而，在我们的工作中，与通常的DEL风格逻辑不同，我们不能完全消除动作模态。尽管如此，我们仍然有一种方法将任意公式约简为一个没有非平凡嵌套模态的简单公式（参见命题34）。如前所述，例如2中的公式[a] B ϵ p = 0.5可以转化为Ba p = 0.5 B ϵ �a��。我们可以在语法上（在证明系统中）展示这一点，这也为设计CPP中的回归方法留下了可能性。02.3.编译为经典规划0尽管我们已经说过经典规划存在局限性，但有一条重要的工作线路试图将符合规划问题甚至符合概率规划问题转化为关于原始初始不确定性集合的不同子集的经典规划问题，且具有足够高的概率（参见，例如，[23,6]）。完全忠实的转换通常需要很高的计算成本，但我们可以找到一些声音但不完整的转换，在实践中可以很好地工作。这也给我们提出了一个自然的问题：我们是否也可以不使用概率，而是使用[24]中的先前的非概率逻辑框架来进行CPP。然而，仔细观察表明，[6]的转换依赖于动作是确定性的假设，但是在这里我们不想做出这个假设。请注意，尽管[23]表明了如何在非概率设置中不使用非确定性，但我们仍然不清楚如何在一般的概率设置中消除非确定性。然而，我们实际上可以在语义上和在我们的系统中的形式证明（参见命题16），如果动作是确定性的，我们确实可以做出[6]中描述的相应的约简。02.4. 关于MDP和POMDP的逻辑0我们的模型与部分可观察马尔可夫决策过程（POMDP）非常相似，参见[25,26]。然而，我们的框架隐含地假设在执行计划时，智能体没有任何观察能力，就像非概率符合规划一样。使用POMDP进行规划更接近于条件规划，其中假设了一定的观察能力。使用POMDP进行规划的目标通常是通过某个策略在有限或无限的时间范围内优化奖励（或成本），该策略可能永远运行下去。另一方面，对于我们来说，计划的概念是一系列有限的动作，目标是一个命题。最近也有一些关于基于POMDP的策略综合的论文，目标是用时间逻辑表达的目标（参见，例如，[27]），类似于在MDP与时间逻辑目标[28-30]的背景下的讨论。请注意，我们的语言侧重于认知方面而不是时间方面，并且允许我们表达概率认知目标。0我们的贡献可以总结如下：0• 我们提出了一个动态认知框架，用于推理关于符合概率计划的概率转换系统，具有以下特点：- 它形式化地捕捉了逐步概率信念变化。-我们可以形式化地验证标准的符合概率计划，这超出了现有的PDEL框架。-我们可以用一个非常丰富的语言通过公式表达规划目标，并形式化各种微妙的符合计划的概率准则，在没有强大的逻辑语言的情况下，这在标准CPP方法中是无法实现的。0• 我们提供了一个完备的证明系统，使得该逻辑具有以下特点：Y. Li et al. / Artificial Intelligence 268 (2019) 54–8459�ni=1 qi Bπiϕi ≥ q:=q1Bπ1ϕ1 + ··· + qnBπnϕn ≥ qq1Bπ1ϕ1 ≥ q2Bπ2ϕ2:=q1Bπ1ϕ1 + (−q2)Bπ2ϕ2 ≥ 0�ni=1 qi Bπiϕi ≤ q:=�ni=1(−qi)Bπiϕi ≥ (−q)�ni=1 qi Bπiϕi < q:=¬(�ni=1 qi Bπiϕi ≥ q)�ni=1 qi Bπiϕi > q:=¬(�ni=1 qi Bπiϕi ≤ q)�ni=1 qi Bπiϕi = q:=(�ni=1 qi Bπiϕi ≥ q) ∧ (�ni=1 qi Bπiϕi ≤ q)Bπϕ = Bπ′ϕ′:=1Bπϕ + (−1)Bπ′ϕ′ = 0Kϕ:=Bϵϕ = 1ˆKϕ:=¬K¬ϕ⟨a⟩ϕ:=¬[a]¬ϕ(|a|)ϕ:=[a]ϕ ∧ ⟨a⟩ϕ(|a1 ···an|)ϕ:=(|a1|)···(|an|)ϕ[a1 ···an]ϕ:=[a1]···[an]ϕ0- 它揭示了CPP中关于概率信念更新的隐含假设。- 在更新的信念状态中检查一个认知公式与在初始信念状态中检查一个公式是等价的。0• 我们展示了该逻辑是可判定的，这可以为CPP的自动定理证明器提供便利。0请注意，在本文中，我们还不能在我们的逻辑框架内自动生成计划（计划存在问题）。我们确实需要像[24]中那样更丰富的语言，将规划转化为模型检验问题。我们将这个问题以及与现有CPP工具的比较留给未来的工作。0本文的其余部分组织如下。第3节介绍了语言和语义，并且还根据我们的逻辑框架定义了符合概率规划。第4节介绍了该逻辑的公理系统并证明了其完备性。第5节证明了公理系统的完备性。第6节展示了该逻辑的可判定性。最后一节对一些未来的方向进行了总结。03. 语言和语义0在本节中，我们介绍了我们逻辑的语言。我们基于行动模态和加权概率项的线性不等式构建了我们的语言，这些概率项受到[31,17]的启发。概率项表示一系列动作到达某个状态集的概率。为了简化本文，我们专注于单智能体情况。这种语言与PDEL的通常语言不同，其中最重要的区别之一是这里的概率表达式由一系列动作索引，而在单智能体PDEL中，概率表达式没有索引或者可以等同地看作只有索引ϵ。0定义3（语言）。给定一个可数的命题变量集合P和一个有限的动作集合A，语言L定义如下BNF：0ϕ  ::=  p  | ¬ ϕ  |  ( ϕ  ∧  ϕ )  | [ a ] ϕ  | q 1 B π 1 ϕ 1  + ∙∙∙ +  q n B0其中 p ∈  P ，π i  ∈  A � ，即一串（可能为空）动作，q ， q i  ∈  Q ，对于每个 1 ≤  i ≤  n 。0除了常见的缩写，我们还有以下缩写。0让我们解释一下如何阅读语言中的公式。命题变量（如 p ）表示世界的基本属性，例如“硬币正面朝上”。然后我们有标准的否定和合取。我们将形式为[ a ] ϕ 的公式解读为“在执行动作 a 的所有执行之后，ϕ 成立”。为了阅读形如 q 1 B π 1 ϕ 1  + ∙∙∙ +  q n B π n ϕ n  ≥  q的线性不等式公式，我们首先解释如何阅读 B π ϕ 。其基本思想是它表示使用 π 得到 ϕ 的概率。更准确地说，它由两部分组成：在成功执行 π的情况下得到 ϕ 的概率，以及成功执行 π 的概率。粗略地说，B π ϕ 是 Pr ( ϕ  |  ex ( π )) ∙  Pr ( ex ( π )) ，其中 ex ( π ) 表示 π可以成功执行。在引入语义后，Pr ( ϕ  |  ex ( π )) 将在执行 π 后的更新模型中计算。换句话说，B π ϕ 是在执行 π 后得到的模型中 ϕ的非规范化概率。如果 π 无法执行，B π ϕ 应为零；如果可以执行，则为更新模型中 ϕ 的概率乘以 π 的可执行性的概率。0该语言在模型上解释，这些模型在某种意义上是（离散的）概率转移系统，具有初始不确定性。3这些模型中有两种概率元素。一种是表示代理人初始不确定性的先验概率分布，另一种是表示每个状态和每个动作的概率函数，该函数指示...03 你也可以将它们视为简化的无奖励和观察的部分可观察马尔可夫决策过程（POMDP）。60Y. Li et al. / Artificial Intelligence 268 (2019) 54–840可以在该状态执行的动作，有可能到达其他状态的概率为1。请注意，与非概率一致性规划模型一样，某些动作在某些状态下可能无法执行。4初始不确定性是所有状态的一个子集。0定义4（模型）。模型 M 是一个元组 � S M , R M , Pr M , U M , B M , V M � ，其中...0•  S M �= � ，一个有限状态集合； •  R M �  S M ×  A  ×  S M ，一个非确定性执行关系； •  Pr  :  R M → Q +，一个表示动作导致另一个状态的概率的概率函数，对于每个 a ∈  A ，它成立...0•  U M ，S M 的非空子集，由代理人认为可能的那些状态组成； •  B M :  U M → Q +0•  V M :  P  →  P ( S M ) ，一个估值函数，指示每个命题变量在哪个世界集合中成立。0对于任何s ∈ UM，(M, s)是一个指向模型。0给定M，(s, a, t) ∈ RM也表示为sa → t，(s, t) ∈ RMa或t ∈ RMa(s)。0在我们提供语义之前，我们首先提供定义模型如何通过执行一系列动作进行更新所需的概念，因为我们需要这些模型来解释动作和概率语句。首先，我们定义与一系列动作相关联的语义结构，称为执行路径集合。0定义5. 给定M，π = a1 ∙∙∙ an，如果s0 ∙∙∙ sn是π在M上的执行路径，并且对于每个1 ≤ i ≤ n，s i−1 ai → si，则称s0 ∙∙∙sn是π在M上的执行路径集合记为EPM(π)。0执行一系列π后，代理分配给模型状态的概率会发生变化。令UM | a为集合{t ∈ SM | sa → t对于某个s ∈ UM}，且UM | π = UM | a1 ∙∙∙| an其中π = a1∙∙∙ an。我们使用以下辅助概念来更新这个概率。0定义6. 给定M和π = a1 ∙∙∙ an ∈ A�，函数μMπ：UM | π → Q的定义如下：对于每个t ∈ UM | π，0μMπ(t) =0{s0 ∙∙∙ sn ∈ EPM(π) | sn = t}(BM(s0) ×�ni=1PrM(si−1, ai, si))0给定T � UM | π和π，令μMπ(T) = �0t ∈ T μMπ(t)，特别地，μMπ(�) = 0。0备注1. 类似于计算隐马尔可夫模型中特定可观察序列的前向算法（例如，[32]），我们也可以通过计算所有初始段π'的μMπ'(t')来递归地计算μMπ(t)。0π和相关状态t'的。0代理应用的更新概率适用于代理认为可能的一组可能更新的状态。现在我们定义代理的更新概率。0定义7. 给定M和π = a1 ∙∙∙ an A�，其中UM | π ≠ �，函数BM | π：UM | π → Q +的定义如下：对于每个t ∈ UM | π，0BM | π(t) = μMπ(t)0μMπ(UM | π)0注意，在这个定义中，分子和分母都是非零的，根据我们设置的方式。注意，假设UM |π非空，那么EPM(π)也是非空的。由于我们假设模型中的概率函数只分配正概率，并且t在UM | π中，分子和分母都是非零的。更正式地说：0命题8. 给定M，π = a1 ∙∙∙ an和U | π ≠ �，我们有BM | π是从UM | π到Q +的概率函数和�0t ∈ UM | π BM | π(t) =1。04 另一种方法是引入无法执行的动作的结果的垃圾状态。5限制为有限状态集是为了简化表示。我们可以轻松地去除这个限制并使用σ-代数和完全一般的概率理论，但这只会分散我们在本文中探讨的问题。(1) μMπ ([ [ϕ] ]M|π ) ≥ 0(2) μMπ ([ [ϕ] ]M|π ) + μMπ ([ [¬ϕ] ]M|π ) = μMπ ([ [⊤] ]M|π )(3) μMϵ ([ [⊤] ]M) = 1(4) μMπa ([ [⊤] ]M|πa) = μMπ ([ [⟨a⟩⊤] ]M|π )μMa1···an+1([[⊤]]M|a1···an+1 )=μMa1···an+1(UM|a1···an+1)=�s0···sn+1∈E PM(a1···an+1)(BM(s0) × �n+1i=1 PrM(si−1,ai, si))=�{s0···sn∈E PM(a1···an)|∃t:t∈RMa(sn)}(BM(s0) × �ni=1PrM(si−1,ai, si) × (�t∈RMa(sn)PrM(sn,a,t)))=�{s0···sn∈E PM(π)|∃t:t∈RMa(sn)}(BM(s0) × �ni=1PrM(si−1,ai, si))=�{s0···sn∈E PM(a1···an)|sn∈[[⟨a⟩⊤]]M|a1···an }(BM(s0) × �ni=1PrM(si−1,ai, si))=μMa1···an([[⟨a⟩⊤]]M|a1···an )0Y. Li et al. / Arti�cial Intelligence 268 (2019) 54–84 610在所有这些定义的基础上，现在很容易定义更新模型。0定义9. 给定模型M = �SM, RM, PrM, UM, BM, VM�和UM | π ≠ �，模型M | π定义为�SM, RM, PrM, UM | π, BM | π, VM�。0我们在动作的语义和概率的线性不等式中使用这个更新模型的定义。语义的其余部分要简单得多。0定义10（语义）。给定指向模型M，s，真实关系定义如下：0M ,  s  �  p �� s  ∈  V M ( p ) M ,  s  �  ¬ ϕ �� M ,  s  � ϕ M ,  s  �  ϕ  ∧  ψ �� M ,  s  �  ϕ 且  M ,  s  �  ψ0M ,  s  �  [ a ] ϕ �� 对于所有的  s ′ :  s a →  s ′，如果 M | a ,  s ′  �  ϕ，则成立 M ,  s  � �n i = 1 q i  B π i ϕ i  ≥  q �� � n i = 1 q i μ M π i ( [[ ϕ i ]] M | π i  )  ≥  q0其中[ [ ϕ ] ] M | π i = { s ∈  U M | π i |  M | π i , s �ϕ }。0注2. 注意，如果M , s 为指向模型，即 s ∈  U M，并且 s a →  s ′，那么M | a ,  s ′ 也是指向模型，即 s ′  ∈ U M | a =  U M | a。0注意，我们使用μ M π来定义更新模型中状态的概率分布。μ M π本身并没有被归一化。0命题11. μ M π是一个非归一化的概率函数，并且具有以下性质：0证明。由于[ [ ϕ ] ] M | π �  U M | π，根据定义6，(1)显然成立。由于[ [¬ ϕ ] ] M | π =  U M | π \ [ [ ϕ ] ] M | π和[ [�] ] M | π =  U M |π，根据定义6，(2)显然成立。由于μ M ϵ =  B M，(3)显然成立。对于(4)，令π  =  a 1  ∙∙∙ a n和a n + 1  =  a，然后我们有以下结果：0命题12. 给定π  =  a 1  ∙∙∙ a n，我们有μ M π ( [ [�] ] M | π  ) =  1  当且仅当M , s �  K ( | π | ) �。0证明。对于每个1 ≤  i ≤  n，令π ( i )  =  a 1  ∙∙∙ a i 以及π ( 0 )  =  ϵ，然后很容易证明如果M , s �  K ( | π | ) �，那么当且仅当对于每个0 ≤  i <  n和每个v∈  U M | π ( i )，M | π ( i ) , v �  � a i + 1 ��。62Y. Li et al. / Artificial Intelligence 268 (2019) 54–840从左到右：根据命题11，对于每个0 ≤  i <  n，我们有0μ M π ( i + 1 ) ( [[�]] M | π ( i + 1 )  )  =  μ M π ( i ) ( [[� a i + 1 ��]] M |0由于μ M π ( [ [�] ] M | π  ) =  1和μ M ϵ ( [ [�] ] M ) =  1，因此对于每个0 ≤  i <  n，μ M π ( i ) ( [ [� a i + 1 ��] ] M | π ( i )  ) =  μ M π ( i ) ( [ [�] ] M | π ( i0假设M , s �  K ( | π | ) �，那么存在0 ≤  j <  n和v ∈  U M | π (  j )，使得M , v �  � a  j + 1 ��。由于v ∈ U M | π (  j )，根据定义6，我们有μ M π (  j ) >0。因此，我们有μ M π (  j ) ( [ [� a  j + 1 ��] ] M | π (  j )  ) <  μ M π (  j ) ( [ [�] ] M | π (  j )  )。矛盾。因此，我们有M , s �  K ( | π | ) �。0从右到左：我们将通过对i进行归纳来证明对于每个0 ≤ i ≤ n，μ M π ( i ) ( [ [�] ] M | π ( i )  ) =  1。当i =  0时，显然成立。如果0i=j+1，其中0≤j 0.6 6. M, s1 � Bab p = 0.706 注意，q1 B π1 ϕ1 + ∙∙∙ + qn B πn ϕn ≥ q 公式无法区分同一不确定性集合中的状态，但[a]ϕ公式可以，因此[a]不能被消除。0Y. Li et al. / Arti�cial Intelligence 268 (2019) 54–84 6301. B ϵ � a �� = 1 表示代理知道a是可执行的，即动作a在集合U={s1,s2}中是可执行的，如气泡所示。02. [a] B ϵ p = 0.5表示执行动作a后，代理将概率0.5分配给p，即在M|a中{s3}的概率。0是0.5。03. B a p = 0.5表示代理将概率0.5分配给通过成功执行a最终进入p状态的概率，即成功执行a的概率（为1）乘以执行a后p的概率（为0.5）。04. Bϵ（|a|）（|b|）� = 0.5 表示最初动作序列 ab 的适用性概率为 0.5，因为（|a|）（|b|）� 只在 s2 处为真。05. [ab] Bϵp > 0.6 表示在每