空间逻辑在分布式系统中的观测模型

理论计算机科学电子笔记142（2006）229-254www.elsevier.com/locate/entcs空间逻辑的观测模型Emilio Tuosto1DipartimmtodiInformatica，UiversitadiPisa乌戈·托雷斯·维埃拉2DepartamentodeInforma'tica，FCT，UniversidadeNovadeLisboa摘要空间性是分布式系统的一个重要方面，因为它们的计算依赖于它们的动态行为和组成部分的结构。空间逻辑被认为是表达系统空间属性的形式化工具我们定义CCS||，一个类似CCS的演算，其语义允许人们观察在这些系统之上，我们定义了空间逻辑的模型。我们的替代定义的模型被证明是等价的标准。此外，还利用CCS的双相似性来刻画逻辑等价||.保留字： 空间逻辑、双相似性、观测框架1介绍在过去的几年里，许多研究人员对系统的所谓空间性质的研究越来越感兴趣，即那些与系统结构密切相关的性质，而不是与系统的动态行为密切相关的性质[8，11，13]。许多工作也致力于探索数据结构的空间属性[9，10]和ad-hoc逻辑的可判定性属性[18，14]。空间性是一个重要的方面*这项工作由欧盟项目FET IST-2001-33100 Profundis资助。1电子邮件：etuosto@di.unipi.it2电子邮件：htv@di.fct.unl.pt1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.028230E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229事实上，随着分布式系统的发展，越来越明显的是，分布式计算既依赖于其组件的动态行为，又依赖于这些组件所确定的系统结构。这在广域网中甚至更为重要，在广域网中，系统的拓扑结构可能遍布全球。例如，分布式文件共享应用程序考虑到信息的分发和用于下载的链接的带宽。最近，空间逻辑[6，8，7]已被提出作为表达系统的空间属性的形式化设备。空间逻辑的一个典型公式是一|B类（1）它表示由两部分组成的系统的性质，一部分满足A，另一部分满足B。空间逻辑以一种非常优雅的方式表达分布式系统的属性，因为分布式系统拥有许多本质上是空间的属性。为了提供一些直觉，考虑唯一处理的属性，该属性表示只有一个实体准备好在确定的通道上接收消息，因此只有系统的一个部分可以在该通道上执行输入操作。还考虑独占资源访问的特性，其特征在于具有仅对单个组件已知的资源的系统。在类似的术语中，保密可以被解释为一些信息，其知识被限制在系统的一部分请注意，保密性在共享秘密信息的进程上引入了空间界限的概念空间逻辑公式A的模型通常被定义为具有由A表示的属性的系统的集合。一般来说，系统是用一个给定的过程演算来表示的，这个过程演算配备了操作语义，定义蕴涵关系的典型方法是利用底层的结构同余。例如，公式（1）的模型是那些过程P≠Q|R使得Q满足A，R满足B。根据[25]的术语，这种定义模型的方式可以被称为完全有意的，因为它依赖于结构一致性（不同的方法在1.1节中讨论）。在这项工作中，我们考虑了[5]中提出的逻辑，并在CCS [19]的一个简单变体上解释了它的本文的第一个贡献是模型的另一种定义，它不是基于结构一致性，而是依赖于演算的操作语义。直觉是，一旦空间逻辑和过程演算及其观察语义被固定，我们就用空间观察来丰富观察。也就是说，我们扩展的语义过程，使结构信息可以明确地观察到，产生的空间语义。因此，我们定义E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229231并证明了新定义与标准定义的等价性。空间语义自然地导致了一种双相似性，即空间双相似性。第三个结果是空间双相似性的逻辑等价的特征，事实上，我们证明了它们是一致的。值得注意的是，空间双相似性的定义是完全扩展的，即它不依赖于结构一致性。最后，我们给出了逻辑等价和双相似的另一种刻画，证明了它们与一个扩展的结构同余一致。在这项工作中，我们不解决实现问题，但是，我们的主要动机是提出可以用于开发算法，验证技术和工具包以检查逻辑等价性的结果。开发针对空间逻辑规范的分布式系统验证工具和技术确实很有意义。这种工具的一个例子是空间逻辑模型[27]，它使用π演算来建模系统和[5]的空间逻辑来表达空间属性。尽管根据公式对给定系统进行模型检查是非常有用的，但检查两个系统在逻辑上是否等价也可能很重要，即检查它们是否满足同一组公式。在我们的方法中，这可能是通过利用空间双相似性来完成的，换句话说，检查逻辑等价性减少到检查空间双相似性，因为它们是一致的。我们注意到，具有完全扩展双相似性的逻辑等价特征也具有语用影响，因为我们可以利用现有的工具包，例如[16，26]，依赖于这种行为等价性。适应双相似性检查算法的逻辑等价性检查是留给未来的工作。1.1相关工作在正式定义并发和分布式系统的可能方法中，我们讨论那些与我们的环境更密切相关的方法，即明确考虑系统空间方面的框架。 我们并不假装详尽无遗，不排除许多与我们的工作没有密切联系的办法。进程演算及其操作语义允许将语法视为结构的具体化，而语义则是侧重于系统动态行为的语法特征的抽象。在这种情况下，基本上有两种方法来检索系统结构的信息。人们利用结构一致性来检查系统是否符合某些要求[11，7]。另一个可以追溯到[3]的开创性工作，它引入了一个观察语义。232E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229CCS [19，20]的tics，其中空间信息系统是从系统的可观察行为推导出来的。另一个例子是瓦片模型[15，4]，其中结构重构的观察结果与其行为的观察结果完全分离。 事实上，在瓦片模型中，系统在两个维度上演化：然而，系统的结构重构只考虑其界面的变化。值得注意的是，所有这些方法都定义了抽象地表示系统结构的观测（在[25]之后，它们可以被称为扩展的）。最近在[23]中遵循了一种不同的方法，其中并发系统通过一对函子的相互作用用共代数术语描述。第一个函子负责表示系统的动态行为，而第二个函子则负责重构系统的空间结构。基本上，[23]区分了两种不同类型的可观察性，并分别处理它们。在[25]和[18]中，研究了移动环境[12]（方言）的空间逻辑，并将相关的逻辑等价与观察等价进行了对比，例如，倒钩全等和内涵双相似。基本上，当微积分的可观测量缺乏系统空间结构的充分信息。此外，[25]讨论了需要口吃技术来应对递归。口吃有助于对比内涵的双相似性和带刺的一致性。这些方法可以被认为是[23]和[3]的混合方法我们的方法类似于[23]，但是，我们统一处理空间和行为观察，而不是单独处理它们。实际上，我们期望空间语义的余代数定义依赖于单个函子的余代数，而不是一对函子的余代数虽然这两种方法的目的都是建立一个处理行为和结构观察的过渡系统，但它们在实现目标的方式上主要事实上，在我们的工作中，这两种观察虽然性质上有些不同，但以统一的方式处理（通过为过渡配备结构检查）。如第6节所述，在考虑实现问题时，这种一致性带来了一些好处尽管所采用的微积分和逻辑存在技术上的差异，但我们遵循的方法与[25，18]有许多相似之处，因为我们的目的是给出逻辑等价的共归纳特征。然而，我们注意到，这里引入的空间双相似性的定义完全是E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229233延伸的，而[25，18]的双相似性利用结构一致性。这是可能的，因为我们丰富了可观测量所携带的信息，在我们的情况下，这些可观测量是表征系统空间信息的表面进一步的说明是，我们的目标是应用现有的验证技术来检查逻辑等价性，而在[25，18]中，主要动机是研究等价性的表达性。论文的布局我们在第2节中定义了基本的微积分，而逻辑在第3节中报告。第四节介绍了空间语义、空间互模拟及其性质。第五节给出了该逻辑的观测模型，并证明了空间双相似性、逻辑等价性和扩展结构同余性是一致的。最后一次机会-在第6节中进行了选择。我们在附录A和B中收集了我们结果的详细证明。2过程模型本节的目的是介绍一种微积分，它为定义空间逻辑的模型提供了基础。我 们 介绍CCS||微积分，锚定的CCS，基本上平滑地扩展了CCS [19，20]。迪埃杰伦特可以使用演算，但我们更喜欢坚持使用一个简单的CCS变体，因为我们的首要目的是简单介绍本文的主要思想我们首先给出了共同名称、动作和过程的定义。定义2.1[别名、动作和过程]给定无限集合N，名字（rang e doverbya，b . . . n，m 。 . . ）thesetsN<$行动的定义如下：和A的N<${n<$|n∈N}（co-name s）AN<$N<$<${τ}（action s）.我们让α在A上值域，记na（α）为出现在α中的名字的集合。过程的集合P由下式给出：P，Q：：= 0 |α.P |P |Q|（ν n）P |P ||Q.二氧化碳捕获和储存||process要么是空的，要么是一个由动作前缀的进程，要么是两个进程的并行/锚组合，要么是一个名称受到限制的进程。234E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229CCS的语法||除了一些小的差异之外，与[ 20 ]中提出的CCS非常相似。首先，CCS中缺少选择运算符||然而，它可以容易地添加，而无需对以下内容进行任何改变。第二，CCS||缺乏递归或迭代;在考虑递归过程时没有概念上的困难，然而（与选择运算符不同）这将使证明更加复杂。最后，隐藏运算符被限制（在[20]的精神）取代，并引入锚运算符。前者只是一种句法变化，并允许我们也摆脱重新标记运算符（它被名称替换所取代），而后者是必要的，以便对逻辑的并行模态进行建模;这一点将在后面更清楚地说明。给定一个过程P，P的自由名和有界名的集合（分别用fn（P）和bn（P）表示）对于标准构造和锚点都是按以下方式定义的。fn（P ||Q）= fn（P）<$fn（Q），bn（P ||Q）= bn（P）bn（Q）。当一个过程通过α-重命名另一个过程的束缚名得到时，两个过程是不可区分的;当P和Q通过α-重命名等价时，我们记为P<$αQ。定 义 2.2 【 结 构 同 余 】 结 构 同 余 记 为 ， 是 CCS 的 算 子 的 最 小 同 余（wrt||）关系，使得它包含了过程的α，（P，0，|）是一个交换幺半群，下面的公理成立。（ν n）0 <$0 n/∈fn（P）<$P|（ν n）Q∈（ν n）（P |Q）（ν n）（ν m）P（ν m）（ν n）P.让我们注意到，定义2.2不涉及锚算子。如稍后将更清楚的，||既不是可交换的，结合的，也没有中性元素。CCS的行为语义||这是一个标记的转移系统。定义2.3 [CCS的行为语义||指定CCS行为的语义||过程由表1中的规则指定的关系−→ Δ P ×A ×P给出。目前，λ在A上变化（与α一样）;稍后，我们将扩展CCS的观测值||从而使结构一致性规则具有更广泛的应用。值得注意的是，表1中的规则没有给出从锚定过程。原因是锚过程只有“结构”转换，不暴露任何“行为”观察。不可能观察到锚的行为，因为它包含在观察中E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229235α。P−α→P（Act）P−α→PJP|Q−α→PJ|Q（Par）P−a→<$PJQ−a→QJP|Q−τ→PJ|QJP−α→Q（通讯）（νn）P−α→（νn）Qn/∈fn（α）（RES）P<$PJ−λ→QJ<$QP−λ→Q表1行为语义（丛）空间限制，有点类似于限制，当涉及到受限制的名字时，也会过滤可能的行为转变3逻辑在本节中，我们将介绍逻辑的语法和语义，与[5]中的内容非常相似。需要注意的是，这里没有递归公式，并且并行公式的解释被扩展以满足这里考虑的过程模型。逻辑的语法和语义在定义3.1中给出，后者是通过公式的表示来给出的，即，这些过程的集合式（A）{P|P| = A}）。定义3.1[空间逻辑]空间逻辑的公式由以下语法定义：A：：=T（True）|欧元（否定）|A组B组（连词）|0（无效）|一|B（组成）|<α>.A （行动）|n A（启示录）| Ix.A（新鲜名称）|A.A.（不确定性）。236E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229（T）P（A）P\（A）（A）（A）（B）（0）{P|P0}A|B）{P|科瓦克河PQ|R<$Q<$A）<$R<$B）}{P ||Q |P ∈A）<$Q∈B）}（<1）. A）{P|你好。 P−α→Q<$Q∈A）}nA）{P|你好。P<$（ν n）Q<$Q∈A）}第一章A） SSn/∈fn（A）（<$A{x<$n}）\{P | n ∈ fn(P)})1000美元。A）、n∈N<$A{x<$n}）表2逻辑的语义学我们让A，B，C在公式上值域.表2中报告了逻辑的语义。定义3.1在公式中使用名称（n，m∈ N）和名称变量（x，y∈ V考虑的逻辑运算符包括命题，空间和时间运算符，新鲜度量化和一阶量化。布尔连接词有标准的解释，空间连接词解释的结构的过程和时间连接词解释的行为的 更确切地说，空间连接词有以下解释：0被空过程满足，A|通过考虑两个过程的平行合成或锚定，B被可以分解为两个部分的过程满足，使得一个满足A，另一个满足B，并且满足以<α>.A的形式存在的时态运算符被在执行动作α之后保持A的进程所满足 。 最 后 ， freshnameuani fi erIx 。 Aisitisfied dby proprocessesttt ， forsommenamem新的过程和公式，持有A{x←m}，存在quanti fierx. A表示对于某个名称m，持有A{x←m}的过程。在两个量化器中，x的出现与作用域A绑定。关于[5]中提出的逻辑，重要的是要注意，假定两个过程是内部公式的模型，则两个过程的锚组合是逻辑的并行模态的模型。请注意，进程的分离和左/右放置是由锚点给出的，沿着将锚点解释为固定空间边界的路线，甚至不能考虑结构重排锚点构造的简单描述可以是它表示E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229237系统的快照，在这个意义上，它捕获了确定的配置，并且不允许任何重新配置或观察，而不是锚正在分割的系统的两个部分的投影。为了加深锚上的直觉，P|=a. 0|a'. 0和P||=a. 0||a¯. 0、nP||=<τ>。TwhilstP||= τ >。|=<τ>. Tandal s oP||=。TwhilstP||=|=. 这一点可以在并行计算中观察到，但在并行计算中则无法观察到。更重要的是，我们有P||=。不|。TwhilstP||= a <$>。|=. 不|。其中，过程的并行部分是可交换的，而锚点不是。 对于满足f或mula的锚进程的示例，请注意，||= a>。|=. 不|. 由于内部组件，的锚满足相应的子公式的并行模态。最后考虑0||0 |= 0，表明由于诱导的空间约束，即使空隙过程的锚定成分也不能被视为空隙过程在锚。这一部分由逻辑等价的定义来概括。定义3.2 [逻辑等价]两个过程P和Q是逻辑等价的，记为P = LQ，i它们满足完全相同的公式集，即i，P| = AQ| = A对任何公式A成立。4观察结构我们的主要目的是用双相似性来刻画逻辑等价。基本上，这相当于说CCS的观察语义学||必须包含一些信息，使我们能够推断（部分）系统的结构。主要有两种不同的方式来获得这些信息。按照[3，15]的思路，一种可能性是用标签来丰富行为观察，这些标签携带着关于激发给定动作的系统部分的信息。我们采用了完全分离行为和结构观察的不同解决方案。我们选择的原因在于启示和平行模态的高度区分力。一方面，过程（νn）n<$在逻辑上不等于0，这是根据模型的定义在第3节中给出：（νn）n<$|=n。0 0|=n。0的情况。相反，从过程的行为推断过程的结构的语义学不能区分这两个过程，因为它们都没有暴露任何转换。因此，由这样的语义引起的互模拟不能238E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）2290νn（Void）0−→0（νn）P−→P（Reveal）φ φ（冻结） P|Q−→ P ||QP||Q−→ P ||Q（锚）[（左）P||Q −→ PP||Q −→ Q（右）表3空间语义是逻辑上的对等。另一方面，并行模态的解释需要精确地确定一个子系统和相应的其余部分。可能，这也可以通过空间/行为观察的代数结构来确定，然而，所得到的框架通常特别复杂和复杂。定义4.1 [空间可观测量]标签集Λ由Λ A i给出，其中i{ν n|n∈N}<${0，φ，<$，[}.空间检查的要素是空间检查。 标签由λ排列。定义4.1引入了可观测量，它提供了系统空间结构的信息。标签既可以是定义2.1中的动作，也可以是产生系统空间结构信息的空间检查。一个标号νn将被用来观察受限制的名称，0表示系统是过程0，φ是通过“冻结”系统的平行组合而引起的观察，空间可观测量用于定义CCS的空间语义||.定义4.2 [CCS的空间语义||CCS的空间语义||通过将表3中的公理添加到表1的推理规则中来获得。让我们评论一下表3中的公理。 第一个公理指出，0进程显示0转换。公理（Reveal）指出，一个有n个限制的过程有一个标记为νn的过渡到一个限制已经被揭示的过程。一方面，这让人想起π演算的开放规则，其中限制名称可以在绑定输出转换中挤出。另一方面，CCS||没有任何规定，对应于π-演算的封闭规则;一旦一个名字被打开，无法关闭。第三和第四条公理指出，两个进程P和Q的并行或锚定组合可以“冻结”到相应的锚定进程P中||Q，分别。由于锚算子不遵守幺半群定律，直观地冻结一个系统对应，以避免通过结构同余重新配置它，并认为它完全由两部分组成，左和右分量。 事实上，最后两个公理基本上给出了E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229239锚运算符的语义，即P||Q只能通过分别确定左投影或右投影的过渡移动到P或Q。请注意，不可能观察到从锚点的内部组件导出的任何转换，因此锚点就像一个句法空间边界，它过滤了所有转换，除了投影和冻结，这意味着 一个冻结的系统只会进化成它的一个组成部分如前所述，P||Q可以直观地被认为是由两个平行分量组成的系统，它们要么投射到第一个分量，要么投射到第二个分量。因此，我们认为，||在某种程度上表示具有有限“交织容量”的并行系统。同样，乍一看，人们可能会假设锚运算符可以用[1，2]中引入的同步，左和右合并运算符进行编码。我们推测这是不可能的，因为所有这些算子都与并行算子密切相关（即，在转换之后，到达过程仍然是并行过程），而锚定过程仅演变成它们的组成部分之一。我们为未来的工作留下更深入的比较。现在，我们介绍CCS的观察语义||.我们简单地通过将经典定义投射到行为和空间观察的情况下来定义空间双相似性。根据这个定义，互模拟关系的基本性质也适用于空间互模拟定义4.3 [CCS的空间互模拟||二元关系BP ×P是一个互模拟i ∈ B，当（P，Q）∈B时，则P−λ→PJQ−λ→QJ。（PJ，QJ）∈B（2）Q−λ→QJP−λ→PJ。（PJ，QJ）∈B.（三）定义4.3是应用于CCS空间语义转换系统的通常互模拟定义||.在附录A中，我们证明了互模拟的通常性质适用于空间互模拟（证明这些性质的模仿那些通常的语义和互模拟的CCS[19]）。我们称i∈IBi是空间双相似性，并将其表示为π。 通过提案-第A.2节，互模拟是一种互模拟，并包含任何其他定义的互模拟。命题4.4空间双相似性是等价关系。证据 我们证明了它是自反的、对称的和传递的。回复性。根据命题A.1（2），过程上的恒等式关系是互模拟;因此它包含在互模拟中。传递性。 由于根据命题A.1（3），互模拟是互模拟，我们得出结论：240E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229空间双相似性的传递性（transitivity of spatial bissimilarity）。对称性根据命题A.1（1）和A.2，-1是互模拟，而根据定义-1是互模拟。Q备注4.5锚机操作人员不规范。它的运算语义与（内部）选择运算符的语义大致相似，但它不具有相同的代数性质：||既不是可交换的、结合的、幂等的，也没有中性元素;甚至，P||Q/Q ||P，P||（Q||R）/P ||Q）||R，P||P/P||0/1000在CCS中不是有效法律||.此外，P||Q不是死锁的，因为一旦执行左或右投影，它就可以演化。基本上，||仅防止系统在提交到其组件之一之前暴露行为转换。5描述逻辑等价性在丰富了过程模型之后，现在可以在定义4.2中给出的转移系统上定义逻辑的模型，同时考虑时间算子的更丰富的观察集，因为现在我们不仅可以观察动作，而且可以观察空间检查。我们选择将冻结和投影添加到时间模态的可观测量集合定义5.1[时间观测量]时间观测量的集合由下式给出：A我们让ω的范围超过Ω。语法与定义3.1中给出的语法相同，唯一的区别是（动作）情态<α>.A现在被<ω>.A取代。表4给出了逻辑模型的新定义。下面是对表4条款的一些评论讨论了命题公式在明显的方式，而其余的情况下，利用CCS的空间语义||.例如，为了满足空公式，进程必须暴露标记为0的转换;空间语义（上的引理B.1）第20页）保证这些进程在结构上与空进程一致一个过程满足一个平行公式A|当它可以被冻结到一个过程，该过程投影到分别包含A和B的两个组件时。为了保持nA，一个过程必须表现出一个νn跃迁，E. Tuosto，H.T.Vieira/Electronic Notes in Theoretical Computer Science 142（2006）229241−→−→−→oo−→−→P|=o TalwaysP|=o <$AP|=o AP|=O A组B组P|=o A P|=oB0P|=o 0P−→ QP|=Oφ一|BP−→ PjPjQPJ[罗克|=OAR|=oBP|=O nA PνnQQ|=oAP|=<ω>。AP−ω→Q<$Q|=AP|=O IX. A<$n/∈fn（A）. Pνn QP|=OA{x←n}P|=ox。An∈ N。 P|=oA{x←n}表4通过观察一个保持A的过程（第20页上的引理B.2指出，如果PνxQ然后P（ν x）Q），对于时间模态也是如此;然而，请注意，ω在时间可观测量范围内，因此它也可以是φ，或[。Thefor mulaIx. A是通过这样一种方法来定义的，即对于一个既不出现在过程中（因此，过程可以揭示n）也不出现在过程中的名称nA. 最后一个案例是微不足道的。注5.2值得注意的是，把投影和冻结加到时间观测量上，可以用时间模态改写平行公式实际上，平行模态可以用以下方式书写：一|B<φ>。A<. A.

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