道义逻辑：容错与责任推理，形式主义的新方法

理论计算机科学电子笔记258（2009）17-34www.elsevier.com/locate/entcs道义逻辑，与职责推理和容错相反3巴勃罗·F Castro1 T.S.E.迈鲍姆2加拿大麦克马斯特大学计算机与软件系摘要道义逻辑在上个世纪上半叶被引入，以形式化法律推理的各个方面。从那时起，许多学者都致力于改进形式主义并扩大其适用性，包括在计算机科学和软件工程中。 其中一部分工作集中在动作的使用上，基于的方法道义运营商，而不是传统的属性集中的运营商。 我们提出这种道义逻辑的一个新版本，具有非常好的元逻辑属性，避免了道义逻辑的许多传统问题，并有一个有吸引力的处理相反的责任推理。 这种推理提供了一种关于违反规范约束并描述结果的条件推理。我们将展示如何应用这种形式主义的容错机制的特点，然后原因的机制的属性关键词：容错，道义逻辑，软件规范，软件验证1引言道义逻辑是模态逻辑的一个分支，它专注于研究伦理和道德背景下产生的推理，通常涉及规范和规定（见[3，12]）。这些逻辑通常考虑两种新的模式：许可和义务。当然，与之相关的是禁止和违反的概念。这些概念在容错中自然出现，其中一些操作是“理想的”或“强制的”，而任何其他操作的执行都会产生错误状态。我们在[11]中提出了一种道义逻辑，在[9]中研究了这种逻辑在容错中的应用。在容错系统中，通常会有这样的情况，在违规之后，我们必须执行一些操作来从违规中恢复这是一个1电子邮件：castropf@mcmaster.ca2电子邮件：tom@maibaum.org3这项工作得到加拿大自然科学和工程研究理事会以及麦克马斯特大学计算机和软件系和工程学院的支助。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.12.01118P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）17→道义逻辑学家称之为违背职责（或简称CTD）推理。CTD推理一直是道义逻辑研究的重要对象，这种推理在法律场景中自然出现然而，在几个道义逻辑中，CTD情景在形式化时是不一致的;这有时被认为是矛盾的，因为这与我们的直觉相反（在这个意义上，直觉上，这些陈述并不矛盾）。在本文中，我们扩展了[11]中介绍的逻辑，目的是获得一个更具表达力的框架，使我们能够避免在与职责相反的场景中出现的经典问题。此外，我们提出了一些例子来说明，CTD语句是常见的，在指定的容错系统，我们展示了我们如何可以处理它们使用所提出的逻辑。本文的结构如下。 在第二节中，我们简要介绍了道义逻辑和相反的义务声明。在第3节中，我们描述了我们的版本的道义逻辑，我们提出了一个更具表现力的扩展。 分段在图4和图5中，我们展示了两个例子：一个简单的火车系统和拜占庭将军问题的形式化[18]。这些案例研究使我们能够证明CTD推理在容错中自然产生。 我们证明了一些性质的例子来说明使用道义逻辑来指定和验证容错系统的好处。2道义逻辑恩斯特·马利是第一个尝试使用形式系统来捕捉规范和规定背后的推理的人，特别是马利引入了义务作为谓词（以及其他相关算子），并为他的逻辑提供了一个公理系统。 然而，在马利的逻辑中，义务的概念是超级模糊的，这个意义是，如果我们把O（）看作是说应该是为真的情况，那么我们得到了使道义算子平凡化的KMO（k）。 从那时起，在文献中提出了几个道义逻辑。也许研究最多的是所谓的标准道义逻辑（SDL）[12]。SDL是正常模态逻辑的一个特例;这种逻辑具有模态O（O）（O是强制性的）;并且提出了以下公理来捕获义务的概念[20]：SDL 0。 所有的重言式SDL 1。O（π → π）→（O（π）→ O（π））。SDL 2。O（λ）→ <$O（<$λ）。对于我们的规则：• 如果你是一个人，你是一个人，• 如果是，则是（）。SDL的等价公理化可以在[12]中找到（这个系统被称为OK+在[3]中）。 第二个演绎规则意味着我们有一个正规模态系统。P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）1719不→→-哦H►∧ ¬ → ⊥SDL的语义是用Kripke结构[5]给出的，并且义务算子的解释与通常的模态必要性相同（尽管这种公理化在Kripke模型上强加了不同的结构;注意，公理暗示Kripke结构是串行的，即，每个国家都有一个继承者）。语义的直观性如下。如果一个状态w与另一个状态v相关，这意味着在w中发生的义务在v中为真（在某种程度上我们可以把v看作是w的一个这个公理系统的几个结果被批评为违背义务的直观属性。 例如，这些公理的一个推论是性质O（ ）（可以 可以理解为总是有义务的;至少我们有所有的tau- tologies都是有义务的）。有些人认为，可能存在没有义务的情况，而这些情况在SDL中是不可能的。另一个有问题的问题是许可的定义，它在逻辑中被引入为一种双重义务，即：P（）O（）。注意，这个定义和公理SDL 2一起，意味着我们有下面的定理：O（n）P（n），即，义务意味着许可。 如果我们把许可看作模态可能性（SDL就是这种情况），那么我们就有了有时被称为康德定律的东西暗示可能性（即，O（）Q）。不难找到这样的例子，财产不可取。 我们无意为这个逻辑体系辩护或反驳;读者可以采取自己的立场。关于这些主题的进一步讨论可以在[12]中找到正如在引言中所解释的，我们感兴趣的是与义务相反的状态。让我们介绍一个CTD陈述的标准例子，即所谓的温柔杀手悖论。它可以表述如下：• 禁止杀人。• 如果你杀人，你必须温柔地杀人。• 你杀人。在SDL中，这个悖论的形式化给了我们一组不一致的句子[24]。主要问题是，在SDL中，不相容的义务是不一致的，即，O（O）O（O）。在容错中，值班场景也是常见的。我们在第4节和第5节中用两个例子来说明这一事实。标准道义逻辑是一种应然道义逻辑，即：道义谓词被应用于谓词（例如，下雨是必须的）。许多作者（例如，[21，17]）指出，道义逻辑的几个问题（paradoxical语句和非直观属性）可以通过将道义算子应用于动作而不是谓词来解决。在[21]中，Meyer提出将道义谓词简化为模态运算符（在动态逻辑设置中[15]）。 这项工作背后的主要思想是使用一个常量谓词来指示何时违反已经发生了在动态道义逻辑中，我们有命题公式和[α]类型的公式，其中α是动作，是公式。 行动是由一组原子操作和操作符构建的。动态逻辑有以下操作符：;（顺序组合），（选择），（迭代）。 直觉上，公式[α]表示在执行动作α之后，公式变为真。20P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）17−H≡ ⟨ ⟩¬W⟨⟩--VVU ∈UU∈∈ H ∈ H ∈∈⊆ ∅∈∈ ∪ ∈ → ¬∈换句话说，使用这些公式，我们可以以前置/后置条件的方式来表达动作的具体化。Meyer将许可的概念简化为模态，如下：αv，即， 当且仅当存在某种执行方式使得我们获得没有违反的状态时，动作才被允许（其中v表示违反已经发生的想法）。FOREST项目[17，19]提出了类似的方法，其中引入了具有动作的模态逻辑（称为MAL），但MAL考虑了其他几个动作运算符，例如：（并行执行）和（动作补）。在文献中已经提出了许多其他形式的道义逻辑与行动。 所提出的逻辑之间的一个区别是在第3节和迈耶道义谓词和标准模态之间没有关系，即， 我们不把道义谓词简化为可能性或必然性的概念。我们拒绝将道义谓词还原为模态，因为我们认为规定（系统应该做什么）和描述（系统做什么）不能混淆。例如，根据Meyer对权限的定义，允许的操作也是恢复操作（它们将系统从错误状态恢复）。这在容错中是不可取的：允许的操作可能会带来违规;这也是Sergot在[23]中指出的3一种规范分层的道义行为逻辑我们在[11，8，7，10]中提出了道义行动逻辑;在本节中，我们简要回顾了这种逻辑的基本定义，并介绍了这种逻辑的扩展，以处理与职责相反的推理。我们使用词汇（或语言）来指代元组L=Δ 0，Φ 0，V0，I0，其中Δ 0是原始动作的有限集合：a1，.，一个N，它代表系统的一部分可能的动作，也许，它的环境。Φ 0是由p1，p2，.表示的命题符号的可解集。. . V0是的有限子集，其中 =v 1，v 2，v 3，. . 是一组无限的、可重复的“违反”命题。I0中的指数对应于范数概念的分层，其中分层对应于被建模系统中的故障程度。所有这些集合都是互不相交的。词汇表中的原子动作可以如下组合以形成更复杂的动作术语（用Δ表示）：Δ0Δ和，UΔ。如果α，βΔ，然后是αβΔ，αβΔ和αΔ。 没有其他表达式属于Δ。另一方面，这个逻辑的公式（用Φ表示）定义如下。如果φ 0V0，则φ 0。 如果和是公式，则我，ψΦ。 如果A是 公式和α是作用量，则[α]α是公式。 如果α是一个动作，我0，然后 Pi（α）和Pi（α）是公式。如果和是公式，则EN，A（）和E（）Φ。如果α和β是作用，SΔ 0，则DoneS（α）和α = actβ是公式。B是公式。模态和道义公式的直观解读如下：• [α]，在以任何可能的方式执行α之后，将保持不变。• [α1Hα2]，执行α1或α2的每种方式都会导致。P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）1721I.1对于每个Δ：（ ）（）（Δ）1.一.3=（）。WP 公司简介• [α]在执行与α不同的动作后，α成立。• [α1H α2]，执行α1和α2的每种方式都会导致。• P i（α），对于分层的层次i，允许所有不同的执行α的方式。• Pi（α），对于分层的层次i，至少有一种执行α的方式是允许的。• [U]，任何组件的执行都会产生。• 嗯，在某种程度上，在下一个瞬间，这是真的。• A（U），在每条路径上，公式都是真的，直到变为真。• E（U），在每条路径上，公式都是真的，直到变成真的。• 完成（α），α是最后执行的动作。B在时间开始时为真，因此表示任何系统执行的初始状态 时态运算符在分支时态逻辑中具有标准意义。 注意，如果我们考虑布尔代数Φ BA的某种完备公理化，则我们得到作用项的布尔（原子）代数Δ/ΦBA。重要的是要注意，这个布尔代数中的每个原子都被解释为单例或空集。定义3.1 [模型]给定语言L = Φ 0，Δ 0，V0，I0，L-结构是一个元组：M = W，R，E，I，{Pi|其中：• W是一组世界。• E，是一个非空的事件（名称）集合• R是世界之间的E标记关系。 我们要求，如果（w，wJ，e）∈ R且（w，wJJ，e）∈ R，则wJ=wJJ，即，R是功能性的。• I是一个函数：· 对每一个p∈ Φ0：I（p）<$W· 对于任何α∈ Δ0：I（α）∈ E，且I（α）是有限的。此外，解释I必须满足以下性质：αi∈0 |αj ∈ 0 − { α i }}|≤ |≤I.2对于每个e∈ I（a1H. H an）：如果e∈ I（αi）<$I（αj），其中αi/=αj∈Δ 0，则：<${I（αk）|αk∈ Δ 0<$e∈ I（αk）}={e}.Eαi∈Δ0Iαi• 每个i都是一个关系，该关系指示关于具有索引i的许可在哪个世界中允许哪个事件。粗略地说，该结构给出了一个带标签的变迁系统，其标签是事件，这些事件是由某些局部动作产生的，或者它们也可以对应于外部事件。请注意，我们有一组事件，但动作只在有限子集上解释，其交集满足Hausdor条件（由条件I.1和I.2暗示），即， 我们要求每个单点集都可以从组件的动作中生成;这确保了转换中的标签由组件中的动作的一些并行执行以及可能的一些环境动作唯一地确定。22P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）17→→ei+1→我我我{}我们使用极大迹给出时态算子的语义下面，我们使用以下符号。Givenaninfinitite trace（orpath）π=s0→e0 s1→e1第二季第二集... ，记为πi=si埃伊斯一期+1→……π的子路径起始于位置I. 符号πi=si用于表示路径中的第i个元素，我们写π[i，j]（其中i≤j）对于子路径sieiej...→sj+1. 其中π（i）表示事件E。最后，给定一条有限路径πJ= sJeJ0....公司简介，我们说πJ≤π，如果πJ是一个iJ0→J→n+1π的初始子路，即：si=si和ei=ei，其中0≤i≤n，我们记为的严格版本。关系π，i，M（在结构M中的时刻i为真）的形式定义可以在[6]中找到在[6]中，我们给出了这种逻辑的一个可靠而完整的拥有多个版本的权限在实践中很有用，特别是当我们有与职责相反的语句时。例如，考虑温和杀手悖论（在第2节中介绍）：• 禁止杀人。• 如果你杀人，你应该温柔地杀人。• 你杀人。如前所述，在SDL中，这个悖论的形式化给了我们一组不一致的句子[24]。我们可以将此场景形式化如下：•F1（k）• kg ±k• nkH k=act•O2（nkHkg）• ANDone（k）我们考虑k（杀死），kg（轻轻杀死）和nk（不杀死）。第一条公理说，禁止杀戮。第二个公式说，轻轻地杀死（公斤）的行动是一种杀死的方式。第三条公理表明，杀与不杀是不相交的行为。第四个公式说，如果我们要杀人，那么我们必须温和地杀人。在最后一个公式中，我们使用Done（）运算符来声明我们将杀死（这表示下一个动作是杀死）。 在这种情况下，我们在词汇表中考虑两个索引：1和2，指出在规范中有两个不同的规范水平。与标准的道义逻辑相反，这些句子在我们的背景下并不矛盾。例如，图1所示的结构是这组句子的模型。这个图中的结构有三个状态w，w1，w2，我们有（k）=e1，e2，（kg）=e1，（nk）= e3. 转换上的标签指示在每个转换中执行哪些操作，哪些操作不执行上面的虚线箭头表示相对于索引1而不是索引2被禁止的转变下面的虚线箭头表示两个索引都禁止的箭头 在[22]中，Meyer勾画了动态道义逻辑的扩展，他考虑了许可和义务的几个版本;他使用这个扩展来模拟一些悖论;然而，P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）1723e1、、、≤≤W≤≤≤ ≤ ≤≤w1W，， ，e2、 ZW2Fig. 1. 温柔杀手在这个版本中，道义谓词被简化为模态，因此，在逻辑中引入了几个违反谓词来对许可进行建模。正如我们上面所解释的，在对容错系统进行建模时，通过模态来定义许可并不总是一个好的选择：规定和描述的概念被混淆了，正如我们上面所说的，这在容错中是不可取的，其中允许或允许的动作的概念必须与恢复动作的概念不同。4第一个例子：一个简单的火车系统我们考虑一个简单的火车系统的例子。列车系统是控制列车通过铁路段网络的系统。容错是这些系统的一个关键方面：系统中的故障可能导致列车相撞和人员生命的损失。这些类型的系统是容错社区积极研究的对象，参见[2，16，1]。我们的系统是由一组列车组成的：t1，...，..r m（我们假设n n（k.） 这些公理说，当在r k回合中，一个忠诚的中尉没有收到至少k条他必须进攻的消息时，那么他就不发送或转发任何消息。11.rm +1→（li. d→AGli. （d）第一部分d→AG<$li. d）、(for任何1 我n.） 这些公理表示，在第m + 1轮中所做的决策是最终的。12.[1i. sendA（j）]lj. A我13.[1i. fwd（k，A，j）]lk. 一个j14. 伊尔岛Aj→[lj]。sendA（i）H1≤t≤nlt. fwd（i，A，j）]<$li. 一个j15. 伊尔岛沃勒岛d→[U]li. D16.长岛Aj→[U]li. 一个j（对于每1 k，i，jn.）这些公理规定了动作l i的行为。sendA（j）和lt. fwd（i，A，j）. 公理15说，如果一个中尉决定进攻，他会坚持他的决定;公理16说，中尉不会忘记收到的信息。最后，我们描述了行为背叛。17.[1i. 背叛]岛v18. 伊尔岛v→[l] i. 比特尔岛v具体化的公理依赖于一个数m，直观地说，这个数是具体化确保忠诚的副手们会同意一个决定的叛徒的数量。我们勾勒出这一事实的证据，如果我们有少于m个叛徒，那么忠诚的中尉达成协议。首先，考虑以下几点32P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）17≤≤−≤公式集Φ 1={1i. F3（fwd（k，A，j））→ANDone（li. fwd（k，A，j））|对于ny1≤i，j，k≤n}这套公式说，叛徒不会说谎。 下面的公式表明最多有m个叛徒：Φ 2=AG（Φ1，j 1）。v.. . 我知道。五）（对于一些不同的0 j 1，.，jn−mn.）另一个有用的假设是，忠诚的副手履行了他们的义务，这可以用以下公式表示：Φ3={1i. O2（α）→ANDone（α）|对于每一个1≤i≤n}。然后，如果我们假设至少有n m个中尉不是叛徒，叛徒不撒谎，忠诚的中尉履行了他们的义务，我们可以证明， 在第m+1轮，忠诚的副手们达成协议。这用以下公式表示：Φ1，Φ2，Φ3=Bizmmm+1→（lj1. d参加. . 参与jn−m。d）。(We用Bizm表示上述规格。） 如果我们证明任何两个忠诚的副手达成协议，那么这个性质就很容易得到。这由以下属性表示：属性1Φ1，Φ2，Φ3=Bizmmm+1→（1u1. d参与者j2。d）。（对于任意u 1，u 2∈ {j 1，.，jn-m}.）证明的草图 一开始，我们有一个。d和<$l u2. D. 如果，在任何一轮r k，k ≤m，我们有l u1。d由公理9，因为我们假设忠诚的副手履行他们的义务，我们知道行动l u1。sendA（l u2）将被执行，并且l u1也将转发他收到的带有攻击命令的所有k条消息。这意味着，在r k+1轮中，中尉l u2将收到k +1条攻击消息，因此，根据公理8，在r k+1轮中，我们有l u2。D. 同样的道理也适用于L2。d在r k轮中，k m。如果l k1. d在r m + 1轮中为真，在所有前几轮中为假，那么这个中尉收到了m+1条说“攻击”的消息，但是由于叛徒不会根据假设撒谎，而且我们假设我们最多有m个叛徒，中尉l u 1收到了来自某个忠诚中尉的攻击命令，该忠诚中尉根据公理9向中尉l u 2发送了相同的命令;这意味着在下一轮中，在收到来自忠诚中尉的命令后，两者都根据公理7决定攻击。Q有趣的是，当叛徒说谎时，上面显示的属性不是真的。假设我们有三个副手：l0，l1，l2，l1是叛徒。考虑m=1时的具体化（只有一个叛徒）。模型图图3显示了一个反例;我们有三个状态：s0，s1，s2，初始状态是s0。在每个状态下，显示在该状态下为真的谓词，不显示为假的谓词。一开始，我们知道没有一个中尉是叛徒，而且l0将军已经决定撤退。每个转换都标有在该转换中执行的操作 在第一次跃迁中，l1P.F. 卡斯特罗T.S.E.Maibaum/Electronic Notes in Theoretical Computer Science 258（2009）173312l1. 是t_rayHttl1。fwd（0_，A，2）Htts，s0.、，zsz、、、，zsr0r1，l1. tr2，l2。D图三. 反例当叛徒说谎成为叛徒;虚线箭头表示执行了禁止的操作之后，l1对l2撒谎，他转发了一条他没有收到的消息;这也是一个禁止的行为。结果，在r2回合中，中尉l2和l0不同意，因为一个决定进攻，另一个决定撤退。6结论和进一步工作本文介绍了文献[11，10，8，7]中提出的道义动作逻辑的一个推广。所获得的逻辑使我们能够捕捉相反的义务声明，这已被证明是很难处理的其他道义形式主义。CTD结构在容错方面是常见的。我们用两个例子为这个主张提供了基础：首先，我们描述了一个简单的火车系统的形式化，我们展示了在这种情况下如何出现与职责相反的语句;我们证明了这个例子的一些性质，我们展示了一个场景，在这个场景中，规范中的道义约束被违反，因此，达到了一个不可取的系统状态。作为第二个例子，我们描述了拜占庭将军问题的一个具体化[18]，这是容错的一个经典案例研究。 使用这个例子， 我们表明，道义谓词允许我们有几个层次的推理规格;这主要是通过使用分层规范来实现的，在这种规范中，在某个层次上违反规范是可以容忍的，而在其他层次上违反规范则是不可以容忍的。本文中提出的逻辑可以通过多种方式进行扩展，以获得更具表现力的框架。第一个扩展是用一阶运算符丰富逻辑;这将允许我们