人工基础智能及逻辑 9

第5章模态逻辑5.1自动驾驶中的模态逻辑推理模态逻辑的应用实例5.2模态语言和可能世界语义语言定义与语义模型5.3互模拟、有效性模型等价性与公式有效性5.4公理系统希尔伯特式公理化系统5.5元定理可靠性、完全性与判定问题5.6结语时态逻辑、动态逻辑等扩展学习目标理解"必然"和"可能"的形式化表达掌握可能世界语义和克里普克模型了解模态逻辑的公理系统和推理规则认识模态逻辑的扩展及应用第5章引言模态逻辑概述什么是模态逻辑？模态逻辑（ModalLogic）提供了一种形式化语言，使我们能够对自然语言中的"必然"和"可能"等概念进行精确定义和严格推理。为什么需要模态逻辑？我们经常需要推理事物的存在状态，以帮助我们做出决策。由于推理过程中常涉及不确定性，需要使用"必然"和"可能"等概念来表达不同的情况。本章内容基本的模态逻辑、语言和语义重要概念和形式推演系统判定问题的经典结果扩展：时态逻辑和动态逻辑5.1自动驾驶中的模态逻辑推理本节通过自动驾驶场景展示模态逻辑在实际问题中的应用。自动驾驶汽车行驶场景假设一辆自动驾驶汽车正行驶在高速公路上，系统需要判断是否可以安全继续行驶。命题定义p：前方道路畅通o：前方有障碍物s：传感器数据可靠（即所有传感器都正常工作）d：车辆可以安全行驶模态算子两个基本模态算子□p：必然p即所有情况下道路都畅通

p：可能p即在至少一种情况下道路畅通关系$$□φ↔¬

¬φ$$这两个模态算子可以互相定义。推理规则逻辑规则$$□p→d（如果前方必然畅通，则车辆可以安全行驶）$$$$□o→¬d（如果前方必然有障碍物，则车辆不能安全行驶）$$$$

p∧

o（在某些情况下前方畅通，而在某些情况下有障碍物，存在不确定性）$$$$□s→(□p∨□o)（如果传感器必然可靠，则可以判断前方是否畅通）$$情境1：理想情况所有传感器正常工作条件：$$□s$$为真（所有传感器都可靠）推理过程获取传感器信息系统根据传感器信息得到$$□p$$应用推理规则由推理规则(a)$$□p→d$$可得d得出必然结论这个结论是必然的，即$$□d$$结论：车辆必然可以安全行驶情境2：部分传感器失效存在不确定性场景：前方有雾，激光雷达无法检测远处的情况，但摄像头仍能部分探测。分析传感器状态¬□s（传感器数据不必然可靠）不确定性系统只能得出

p（道路可能畅通），同时可能得出

o（道路可能有障碍物）无法确定由于

p∧

o，系统无法确定$$□d$$决策：车辆应减速或依靠额外数据（如云端地图、V2X车联网信息）进一步做决策。情境3：障碍物不确定性前方有障碍物，但不确定是否可移动场景：汽车检测到前方可能有一辆静止的车，但无法判断它是否会移动。表示$$

o∧¬□o(可能有障碍物，但不必然有障碍物)$$推理若□o（必然有障碍物）则根据(b)得出¬d，即不能安全行驶若

¬o（障碍物可能会移开）则仍有

d，即可能可以继续行驶决策：系统可以选择短暂停止，或尝试换道，而不是直接继续前行。应用价值模态逻辑推理的作用不确定性推理高速公路驾驶过程中，当传感器不确定前方情况时，系统可以动态调整决策（如减速或变道）恶劣天气应对部分传感器失效时，帮助系统判断是否需要切换驾驶模式信息融合如果车辆的传感器无法确定前方是否畅通，系统可以通过联网获取其他车辆或基础设施的信息，弥补感知信息的不确定性普遍性：围绕可能性和必然性的推理在日常生活中也非常普遍。5.2模态语言和可能世界语义本节介绍模态逻辑的形式化语言和基于可能世界的语义模型。形式化语言定义模态逻辑的语法规则，包括原子命题、逻辑联结词和模态算子可能世界语义基于克里普克模型，通过可能世界和可及关系为模态公式提供语义解释真值条件递归定义公式在模型和状态上的真值，为推理提供形式化基础模态逻辑的语言定义35（模态逻辑的语言）令P是原子命题的集合，p表示任意的原子命题，模态逻辑的语言L由下面的规则定义：$$φ:=p|¬φ|(φ∧φ)|(φ∨φ)|(φ→φ)|(φ↔φ)|□φ|

φ$$核心特点语言基础在命题逻辑语言的基础上添加了两个模态算子□φ读作"必然φ"或者"φ必然为真"

φ读作"可能φ"或者"φ可能为真"互定义性：$$□φ⟺¬

¬φ$$练习31：模态语言表达用模态逻辑的语言表示下面的句子如果一个人工智能系统缺乏适当的训练数据，它就不可能做出准确的预测。为了使人工智能高效运行，拥有大量数据是必要的。如果一个人工智能存在偏见，它的决策不一定是公平的。未来人工智能生成的内容可能会主导网络媒体。如果计算能力持续提升，人工智能有可能实现类人推理。克里普克模型定义36（模态逻辑的模型）一个克里普克模型M是一个三元组(S,R,V)，其中：(a)S是可能世界（或可能状态）的集合(b)R是可能世界之间的二元可及关系(c)V是赋值函数：P→𝒫(S)其中，𝒫(S)是S的幂集V(p)是p为真的所有世界的集合可及关系的解释可能世界之间的可及关系可以有多种解释认知上的可及性（认知逻辑）道义上更理想的状态（道义逻辑）执行了一个程序使得状态发生了变化（动态逻辑）赋值函数：告诉我们哪些命题在哪些世界上为真这种灵活性为其他逻辑语言的解释奠定基础。例14：克里普克模型示例图5-1克里普克模型模型组成世界集合：W={w₁,w₂,w₃,w₄}，在图中用节点表示可及关系：用节点之间带箭头的线表示w₁Rw₂,w₁Rw₃,w₂Rw₄,w₃Rw₃,w₃Rw₄赋值函数：V(p)={w₁,w₃,w₄},V(q)={w₂,w₃}注意：w₃有一个自反箭头，表示对自身可及。框架框架的定义当不考虑赋值函数时，就得到$$𝔉=(S,R)$$，称为框架（Frame）。赋值函数的多样性赋值函数可以有很多，基于同一个框架的模型也可能有很多框架的用途定义有效性概念的时候将会用到框架的概念框架与模型的关系框架提供了模型的结构基础，模型在框架上添加了具体的命题赋值真值条件（1）定义37（真值条件）给定一个模型M和一个状态s∈S，以下递归定义一个公式在M,s上是真的：$$𝔐,s⊨p当且仅当s∈V(p)$$$$𝔐,s⊨¬φ当且仅当并非𝔐,s⊨φ$$$$𝔐,s⊨φ∧ψ当且仅当𝔐,s⊨φ并且𝔐,s⊨ψ$$真值条件（2）模态算子的真值条件$$𝔐,s⊨□φ当且仅当所有的t,若sRt,则𝔐,t⊨φ$$$$𝔐,s⊨

φ当且仅当存在t,sRt且𝔐,t⊨φ$$解释□φ的语义在所有从s可及的世界t中，φ都为真

φ的语义存在至少一个从s可及的世界t，使得φ为真其余形式公式的真值条件可以类似定义。练习32：真值判断考虑例14中的模型，判断下面公式分别在4个世界上的真假□p

q□□q□(p→q)

q→□p提示：根据可及关系和赋值函数，逐步检查每个公式在每个世界上的真值。5.3互模拟、有效性本节介绍模型之间的等价性概念和公式的有效性。模态等价描述从模态逻辑角度看"无法区分"的状态互模拟两个模型之间的结构对应关系，类似于一阶逻辑的同构概念有效性公式在框架、框架类或所有框架上普遍为真的性质模态等价模态等价的定义给定两个模态逻辑的模型M和M'，若M中的状态s和M'中的状态s'满足相同的模态公式集，则它们是模态等价的，记作$$s↔s'$$。模态等价的意义模态等价描述了从模态逻辑角度看"无法区分"的状态跨模型等价即使两个状态在不同的模型中，只要它们满足相同的模态公式，就是等价的互模拟定义38（互模拟）设$$𝔐=(S,R,V),𝔐'=(S',R',V')$$为两个模型。称一个非空的二元关系$$Z⊆S×S'$$是两个模型之间的互模拟，(记作$$Z:𝔐↔𝔐'$$)，如果$$Z$$满足下面的条件：(1)原子命题一致若$$sZs'$$，则$$s,s'$$满足相同的命题变元(2)前向条件如果$$sZs'$$并且$$sRt$$，那么$$𝔐'$$中存在$$t'$$满足$$s'R't'$$并且$$tZt'$$(3)后向条件如果$$sZs'$$并且$$s'R't'$$，那么$$𝔐$$中存在$$t$$满足$$sRt$$并且$$tZt'$$互模拟的记号记号简化当Z是连接𝔐中的s和𝔐'中的s'互模拟时，可以说s和s'互模拟，记作𝔐,s↔𝔐',s'。当𝔐和𝔐'在上下文中清楚时，简写为s↔s'。例15：互模拟验证图5-2互模拟的两个模型验证方法检查原子命题检查对应状态的原子命题是否一致检查前向条件每个可及的后继状态都有对应检查后向条件对应关系是双向的互模拟的意义互模拟揭示的模态语言局限性类比互模拟类似于一阶逻辑的同构概念，用来描述两个模态模型之间的关系局限性使用模态语言无法区分两个互模拟的模型应用价值模型简化可以用更小的互模拟模型替代原模型模型验证在保留原模型信息的前提下，显著减少需要分析的模型大小命题1：互模拟的不变性命题1（互模拟的不变性）对两个模型M,M'之间的任一互模拟关系Z，如果sZt，则s,t是模态等价的。证明方法：可以通过对公式结构的归纳证明得到。互模拟蕴涵模态等价互模拟关系保证了两个状态在模态逻辑意义下的等价性公式满足一致性互模拟的状态满足相同的模态公式轩尼诗-米尔纳定理像有穷模型如果对一个模型M中的每个状态s、关系R，集合{t|sRt}是有穷的，称该模型是像有穷的（Image-Finite）。定理18（轩尼诗-米尔纳定理）给定两个像有穷的模型𝔐=(S,R,V),𝔐'=(S',R',V')，有：$$s↔s'\quad\text{当且仅当}\quads∼s'$$意义：在像有穷模型中，模态等价当且仅当互模拟。互模拟收缩互模拟收缩的定义对于每一个模型(𝔐,s)，总存在一个最小的与之互模拟的模型(𝔑,s)，称为它的互模拟收缩（Contraction）。意义收缩模型可以看作原模型中模态信息的最简表达形式简化方法通过寻找互模拟收缩模型可以对模型进行简化应用在模型检测的理论与实践中，互模拟是一项关键技术，因为它能够在保留原模型信息的前提下，显著减少需要分析的模型大小模型上的真值定义39（模型上普遍为真）若一个公式φ在模型M的所有世界上都为真，我们称该公式在模型M上是普遍为真的。定义40（模型上可满足）若模型中有一些世界使得公式φ为真，称该公式在模型上是可满足的。扩展到公式集公式集普遍为真一个公式集Σ在一个模型M的所有世界上为真，称该公式集在模型M上是普遍为真的公式集可满足若公式集在模型的一些世界上为真，称该公式集在模型上是可满足的有效性定义41（有效性）框架上的有效性（世界）若一个公式φ在基于框架𝔉的任意模型中的世界s上都是真的，称公式φ在框架𝔉的世界s上是有效的，记作𝔉,s⊨φ框架上的有效性（全局）若公式φ在框架𝔉的任意世界上是有效的，称φ在框架𝔉上是有效的，记作𝔉⊨φ框架类上的有效性若一个公式φ在框架类F中的任一框架F上是有效的，则公式在该框架类上是有效的，记作F⊨φ普遍有效若一个公式φ在所有框架类上是有效的，称该公式是有效的，记作⊨φ框架类框架性质与框架类根据框架中可及关系所满足的性质，可以定义框架类：自反框架类满足自反性的框架传递框架类满足传递性的框架对称框架类满足对称性的框架这些框架的性质可以对应模态逻辑的公式，见下表。表5-1：公式与框架性质对应表5-1模态逻辑公式与框架性质的对应关系模态逻辑公式对应的框架性质T:□p→p自反性（每个状态可及自身）4:□p→□□p传递性（如果状态x可及y，y可及z，则x可及z）D:□p→

p持续性（每个状态至少存在一个可及状态）B:p→□

p对称性（如果x可及y，则y也可及x）5:

p→□

p欧几里得性质（如果x可及y且x可及z，则y与z之间可及）公式性质解释各公式的意义T（自反性）表明每个状态都能"看见"自己4（传递性）强调状态之间的传递联系D（持续性）确保每个状态都有至少一个后继状态B（对称性）强调状态之间的双向可及5（欧几里得性质）描述了状态之间的广泛联系框架类的逻辑：当一个公式集在一框架类F上是有效的，称它是该框架类的逻辑，记作$$Λ_F$$。例16：有效性证明（1）例16：证明□p→p不是有效的，但是它对于自反的框架类是有效的证明第一部分（不是有效的）要证明□p→p不是有效的，只需要找到一个模型，使得公式在该模型的某个世界上为假。构造反模型构造模型考虑模型𝔐，其中W={w}，R为空关系，V(p)=∅验证□p为真有𝔐,w⊨□p（因为不存在可及的世界）验证p为假且𝔐,w⊭p（因为w∉V(p)）得出结论因此，𝔐,w⊭□p→p，这样构造的模型，又称为反模型例16：有效性证明（2）证明第二部分（对自反框架类有效）令$$(W,R)$$为一自反框架，即对于任意$$w∈W$$都有$$wRw$$成立。任取基于该框架的模型$$𝔐=(W,R,V)$$，并任取一个世界$$w∈W$$。推理过程假设前提为了证明$$𝔐,w⊨□p→p$$，假设$$𝔐,w⊨□p$$应用语义由$$□p$$的语义可知：对于所有世界$$v∈W$$，若$$wRv$$，则$$𝔐,v⊨p$$利用自反性由于框架是自反的，故$$wRw$$成立得出结论从而得$$𝔐,w⊨p$$结论：在任何基于自反框架的模型中，$$□p→p$$都普遍为真。故该公式对自反的框架类是有效的。□练习33：有效性证明证明以下命题命题(1)□p→□□p不是有效的，但对于传递的框架类是有效的。命题(2)p→□

p不是有效的，但对于对称的框架类是有效的。命题(3)□(p→q)→(□p→□q)在所有框架类上是有效的。提示对于(1)和(2)，先构造反模型证明不是普遍有效然后在相应框架类上证明有效性对于(3)，在任意框架上证明5.4公理系统本节介绍模态逻辑的希尔伯特式公理化系统。希尔伯特式公理化系统希尔伯特式的公理化系统跟自然演绎系统不同，它是由一些普遍有效的公理和推演规则构成的。公理的多样性在模态逻辑中，普遍的公理对于不同的系统有所不同选择希尔伯特式系统的原因为了强调不同系统中公理的差异，在本章选择了希尔伯特式的公理化系统公理系统K定义42（公理系统K）模态逻辑K由下面的公理和推理规则构成：(1)公理模式所有命题逻辑重言式的特例$$□(φ→ψ)→(□φ→□ψ)$$(2)推理规则分离规则（MP）从φ→ψ和φ，推出ψ必然化规则（Nec）从φ，推出□φ意义：K是最小的正规模态逻辑，是关于框架类推理的正规系统中最弱的系统。例17：定理证明例17：给出下面定理的证明$$⊢K□(p∧q)→(□p∧□q)$$证明步骤第一步$$(p∧q)→p$$（重言式）第二步$$□((p∧q)→p)$$（(1);必然化规则Nec）第三步$$□((p∧q)→p)→(□(p∧q)→□p)$$（K公理实例）第四步$$□(p∧q)→□p$$（(2),(3);分离规则MP）例17：证明过程（1）证明$$(p∧q)→p$$（重言式）$$□((p∧q)→p)$$（(1);必然化规则Nec）$$□((p∧q)→p)→(□(p∧q)→□p)$$（K公理实例）$$□(p∧q)→□p$$（(2),(3);分离规则MP）$$(p∧q)→q$$（重言式）$$□((p∧q)→q)$$（(5);必然化规则Nec）例17：证明过程（2）$$□((p∧q)→q)→(□(p∧q)→□q)$$（K公理实例）$$□(p∧q)→□q$$（(6),(7);分离规则MP）$$(□(p∧q)→□p)→((□(p∧q)→□q)→(□(p∧q)→(□p∧□q)))$$（重言式）$$(□(p∧q)→□q)→(□(p∧q)→(□p∧□q))$$（(4),(9);MP）$$□(p∧q)→(□p∧□q)$$（(8),(10);MP）□练习34：定理证明给出下面定理的证明定理(1)$$(□p∧□q)→□(p∧q)$$定理(2)$$

(p∨q)↔(

p∨

q)$$定理(3)$$(

p∧□(p→q))→

q$$提示利用K公理和推理规则可能需要用到□和

的互定义关系注意使用命题逻辑的重言式其他模态逻辑系统通过添加公理获得更强系统K是最小的正规模态逻辑。通过添加其他的公理，可以获得其他更强的模态逻辑系统。S4系统在系统K的基础上添加T和4T:$$□p→p$$（自反性）4:$$□p→□□p$$（传递性）S5系统在S4基础上进一步添加BB:$$p→□

p$$（对称性）或者：S5=KT5（在KT基础上添加公理5）5:$$

p→□

p$$（欧几里得性质）注意：在自反的前提下，欧几里得公理可以推出对称性和传递性。5.5元定理本节介绍模态逻辑的可靠性、完全性定理以及判定问题的复杂度。定理19（可靠性和完全性）对任意的模态公式φ，$$⊢_Kφ当且仅当⊨φ$$可靠性凡是可证的都是有效的完全性凡是有效的都是可证的意义建立了语法证明和语义有效性之间的完美对应判定问题模态逻辑中的判定问题模型检测给定一个具体的克里普克模型M（通常有穷）和一个公式φ判断M,w⊨φ是否成立（或对所有w都成立）可满足性给定一个模态公式φ是否存在一个克里普克模型M和世界w，使得M,w⊨φ？换句话说，φ能不能在某个模型的某个状态下被满足？有效性给定模态公式φ是否在所有的克里普克模型、所有世界上都为真？这等价于¬φ是否不可满足定理20：可满足性复杂度定理20（可满足性）在单一模态算子的正规模态逻辑K中，公式的可满足性问题是PSPACE完全的。其他系统系统可满足性复杂度KPSPACE完全TPSPACE完全S4PSPACE完全S5NP完全意义：S5相对简单是因为其可及关系是等价关系（自反、传递和对称）。证明思路：可满足性证明思路（Ladner1977）上界（PSPACE）使用表列法（Tableau）或过滤法（Filtration）在多项式空间内完成可满足性的判定下界将某些典型的PSPACE困难问题（如量化布尔公式的某些变形）多项式时间还原至模态逻辑可满足性特殊情况添加自反（T）、传递（S4）并不会降低问题复杂度S5的等价关系结构使模型更紧凑，降低了复杂度详细讨论参见Blackburnetal.(2001)、vanBenthem(2010)和Ladner(1977)。定理21：模型检测（1）定理21（模型检测）令$$𝔐=(W,R,V)$$为克里普克模型，其中$$|W|=n$$，R⊆W×W为可及关系，V为命题变元的赋值函数。给定基本模态逻辑K（或其扩展系统如T、S4、S5）中的公式φ，则以下判定问题都可在关于$$|W|+|R|$$与$$|φ|$$的多项式时间内求解（P完全）。(1)点模型检测判断对某个固定世界w∈W，是否有$$𝔐,w⊨φ$$成立(2)全局模型检测判断在模型M中是否所有世界都满足φ，即∀w∈W:$$𝔐,w⊨φ$$定理21：模型检测（2）复杂度更具体地，存在算法能在$$O((n+|R|)·|φ|)$$或其他多项式量级的时间内完成此判定。证明思路（标记算法）分解公式将公式φ逐步分解为子公式标记真值对每个子公式在模型的每个世界上标记其真值更新标记反复利用□与

的语义规则（即对后继可及世界的检查）更新标记完成判定该过程可在多项式时间内完成系统扩展：在系统T、S4、S5等中，可及关系具备自反、传递、对称或欧几里得性等性质，但这不会实质增加局部检查的复杂度.模型检测的应用实践意义该定理为在实践中进行可扩展的自动验证（如程序或系统模型检测）提供了坚实理论支持。并发系统验证对多线程、多进程系统的正确性进行自动验证分布式系统验证验证分布式系统中各节点行为的一致性硬件设计验证在芯片设计阶段自动检测逻辑错误时态逻辑：时态逻辑是对模态逻辑的进一步扩展，通常也能在多项式或指数级时间内做模型检测。这也是它在工业界被广泛用于"程序性质自动验证"的一个重要原因。定理22：有效性复杂度定理22（有效性）在单一模态算子的正规模态逻辑K中，公式的有效性问题是PSPACE完全的。其他系统系统有效性复杂度KPSPACE完全TPSPACE完全S4PSPACE完全S5co-NP完全证明细节：参考Ladner(1977)的论文。注记2：问题关系可满足性vs模型检测可满足性关心的是"有没有某个模型可让公式为真"要对"任意"模型都要考虑故算法复杂度更高，在PSPACE范围模型检测给定一个具体模型通常其复杂度与可满足性不处于相同量级在P范围内关系：这两个问题处理的对象和目标不同，导致复杂度差异。注记3：模态逻辑vs一阶逻辑一阶逻辑的不可判定性一阶逻辑的有效性问题为不可判定不存在一个算法可以在有限时间内对所有一阶公式给出正确的"有效/无效"答案一阶逻辑的可满足性同样不可判定模态逻辑的可判定性模态逻辑只有可能和必然两个算子虽然也有量化的意义，但其作用是局部的与一阶逻辑的全局量化有着本质的区别模态逻辑在理论上是可判定的意义：对很多需要自动推理的计算机应用来说是个好消息。5.6结语：时态逻辑、动态逻辑等扩展本章探讨了模态逻辑的语言和语义，并介绍了公理系统、元定理和判定问题的经典结果。这为后续的模态逻辑的扩展奠定了基础。在结束本章之际，将简要介绍与模态逻辑及其应用紧密相关的两个方向：模型检测中的时态逻辑通过引入时间维度，精确表达系统状态随时间的演化性质程序执行语境下的动态逻辑专门用于描述和分析程序行为的模态逻辑扩展认知逻辑（下一章）将引入下一章的认知逻辑，进一步扩展模态逻辑的应用范围5.6.1时态逻辑时态逻辑主要用于描述系统状态随时间的演化。时态逻辑的作用在模型检测中，时态逻辑是核心工具之一。通过引入时间维度，可以精确表达诸如："最终会发生"描述在未来某个时刻必然成立的性质"始终满足"描述在所有未来时刻都成立的性质"直到某一条件成立"描述在某条件成立之前一直保持的性质从而对系统的行为进行形式化描述和检测。基础：这些逻辑都建立在克里普克结构的基础上，利用状态与状态之间的可及关系描述自动验证系统的各项性质，为复杂系统的可靠性提供了理论支持。常见时态逻辑系统三种主要系统LTL（LinearTemporalLogic，线性时态逻辑）LTL聚焦于线性时间模型，以序列方式刻画状态的演化CTL（ComputationTreeLogic，计算树逻辑）在CTL中，状态公式和路径公式结合使用，可以对分支结构进行精细刻画CTL*作为CTL的推广，CTL*允许更加灵活的时间和路径量化，使得表达能力更强LTL的基本假设线性时间假设LTL的基本假设是时间是单一线性序列。换句话说，LTL关注的是单一路径上的状态演化，而不区分不同分支。适用场景假定系统行为可以用一条单一的"时间线"描述非常适合于描述单个执行轨迹上的行为优点语法和语义较为直观局限性在表达需要考虑多个分支的性质时可能不如CTL或CTL*灵活LTL的算子LTL中常用的算子Xφ下一个状态φ成立Fφ在未来某个时刻φ会成立（最终成立）Gφ在所有未来时刻φ始终成立φUψφ一直成立，直到ψ成立为止参考文献Prior(1967)的先驱性工作Pnueli(1977)在计算机领域影响很大的工作5.6.2命题动态逻辑命题动态逻辑（PropositionalDynamicLogic，PDL）是一种专门用于描述和分析程序行为的模态逻辑。核心思想PDL将程序执行视为状态之间的转换，通过模态算子描述程序执行前后的状态关系与模态逻辑的关系PDL是模态逻辑的扩展，其中可及关系由程序的执行语义决定应用领域程序验证、软件规范描述、人工智能规划等领域PDL的核心思想程序执行的抽象PDL的核心思想是将程序的执行过程抽象为状态之间的转换，并利用模态算子描述程序执行后的性质。形式化定义在PDL中，每个程序α对应一个二元关系$$R_α$$定义在一个克里普克结构的状态集合S上如果$$(s,t)∈R_α$$，则表示在状态s执行程序α后，系统可能转移到状态t这种抽象将程序执行转化为状态之间的"跳转"，从而为形式化分析提供了直观的图模型。PDL的模态算子两种表达方式[α]φ："必然性"在当前状态下，如果程序α可执行则对于所有通过α转移可达的状态，命题φ都成立表达了程序执行后无论如何演化，φ都得满足⟨α⟩φ："可能性"存在一条程序α的执行路径使得执行后达到的某个状态满足φ说明至少有一种执行方式可以达到满足φ的状态PDL的程序构造算子复杂程序的构造序列组合：α;β先执行α再执行β对应的状态转换关系是$$R_