Kappa模型中的刚性几何约束及其对模型状态空间的影响

可在www.sciencedirect.com在线获取理论计算机科学电子笔记313（2015）23-46www.elsevier.com/locate/entcsKappa模型的刚性几何约束Vincent Danosa，1 Ricardo Honorato-Zimmerb，2Sebastian Jaramillo-Riveric，3 Sandro Stuckid，4a爱丁堡大学信息学院联合王国爱丁堡大学信息学生命科学研究所联合王国爱丁堡大学联合王国dPPSLaboratoryUniversit'eParisDiderot法国巴黎摘要基于规则的建模语言，如Kappa [11，7]和BNGL [3，2]，允许对组合复杂的生物化学过程进行简明描述，以及对所得模型进行有效模拟[8，7]。基于规则的建模方法的一个关键方面是部分暴露所涉及的化学物质的结构。然而，上述语言没有提供直接表达化学物质的三维几何形状的手段。因此，模型通常只捕捉所涉及物种的网络拓扑结构.对于某些生物化学过程，例如分子复合物的组装，空间限制起着关键作用，对物种的几何结构进行建模似乎是很自然的。 我们提出了一个扩展的Kappa建模语言，允许注释的化学物种的结构与三维几何信息。这自然地引入了对物种的刚性约束，并减小了所得到的模型的状态空间排除那些在几何学上不合理的物种 我们表明，以这种方式扩展的模型仍然可以尽管以在模拟期间发生更大数量的空事件为代价。扩展引入的几何约束本质上是非局部的，因为它们可能会纠缠在一起在诸如聚合物的大物质中任意距离处的子结构的位置和取向。 我们给出了一个正式的定义的概念的局部性的基础上的直觉，局部修改应该只在一个有限的半径内的修改发生的点周围的子结构。我们表明确实存在非局部的几何增强的Kappa模型，相反，每个局部模型都可以使用有限的经典Kappa模型精确地模拟，代价是其规则集可能的组合爆炸。 我们还给出了模型局部性的一些充分条件但表明局部性一般是不可判定的关键词：基于规则的建模，Kappa，几何约束，分子结构，三维，刚体http://dx.doi.org/10.1016/j.entcs.2015.04.0171571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。24诉Danos等人/理论计算机科学电子笔记313（2015）231介绍基于规则的建模语言，如Kappa [11，7]或BNGL [3，2]，允许对组合复杂的生化过程（如细胞信号传导途径）进行简明描述和有效模拟与基于反应的方法相比，基于规则的建模框架不依赖于过程中涉及的所有化学物质的枚举。过程的组合复杂性很容易使这种枚举变得棘手甚至不可能，例如在聚合反应的情况下，其中涉及的可能物种的数量原则上是无限的。由于它们的稳定性，诸如核酸和蛋白质的分子可以表示为基本分子实体，或具有它们通过其相互作用的位点界面的试剂。在这种情况下，位点可以代表分子内负责它们参与的相互作用的官能团。经典的例子是结合位点、磷酸化位点、甲基化位点等。特别是，试剂可以在位点之间形成弱的分子间键。 这些键也被称为链接，它们与代理一起定义了代表分子复合物网络拓扑结构的位点图在基于规则的建模中，反应被规则取代。与反应不同，规则作用于化学物种的子结构模式，而不是整个物种。因此，一个规则可以捕捉一组多个化学反应，甚至可能是无限多个。然而，上述基于规则的语言并不直接支持在三维空间中描述Agent的几何结构及其链接结构。因此，限制分子相互作用的空间效应不容易翻译成基于规则的语言，并且不清楚是否总是可以这样做在本文中，我们提出了几何增强Kappa，一个最小的扩展Kappa语言。与Kappa一样，化学物种由站点图表示，并通过站点图重写规则进行修改。此外，我们的扩展允许注释的个别代理，网站和链接，半径，位置和方向，分别介绍了相应的网站图上的隐含刚性约束。重写规则可以包括对位点图的几何注释的更新，以便捕获分子复合物的构象变化我们的推广只涉及分子复合物的几何可实现性或可靠性，而不涉及模拟它们在三维欧氏空间中的物理嵌入的演化。特别是，我们不跟踪代理的绝对位置和方向，因此不能明确地处理冲突或碰撞过程。相反，我们保留了一个搅拌均匀的混合物的假设，从经典的，几何少Kappa。事实上，我们的几何框架-1电子邮件：vdanos@inf.ed.ac.uk2电子邮件：s1066652@sms.ed.ac.uk3电子邮件：sjaramil@staffmail.ed.ac.uk4电子邮件：sandro. epfl.ch诉Danos等人/理论计算机科学电子笔记313（2015）2325cally增强的网站图重写包含几何无Kappa作为一个特定的子集，我们表明，对于我们的几何注释的限制集，模拟仍然易于处理，确实可以使用稍微修改的版本来实现 已知的高效Kappa模拟算法[8]。原则上，几何约束可以在任意距离上关联和传播试剂的位置和取向，例如在诸如聚合物链的大分子复合物中。因此，我们的扩展违反了经典Kappa的核心原则，即规则只能对系统的状态进行局部更改。为了使这个想法更精确，我们给出了Kappa模型局部性的正式定义，它捕捉了局部作用规则的效果关于场地图的几何约束，不应超出由规则修改的子结构周围的固定有限半径δ。我们证明了确实存在非局部的几何增强Kappa模型，这意味着这些模型不存在这样的δ我们还表明，对于纯粹的本地模型，它总是可以将几何增强模型转化为几何少模型，虽然在指数增加模型的规则的数量的成本。这进一步证明了非定域性对我们扩展的重要性。最后，我们表明，在一般情况下，它是不可判定的模型是否是本地的，因此是否从几何增强模型到几何模型的减少是可能的。开发这个扩展的主要动机是找到一个基本框架来描述蛋白质复合物的自组装等过程[12，16，18，15]，其中代理可以被认为具有固定大小的体积，相对于代理质心的固定可能位置集的站点，以及相对于相互作用代理的固定方向的链接。 例如，蛋白酶体的组装就是这种情况，其结构由四个堆叠的七聚体环组成（见图1）。在这个蛋白质复合物中，单体之间的相互作用有一个特殊的几何形状，我们稍后会重新讨论最后，我们还希望这项工作作为一个正式的起点，为更先进的扩展建模空间方面，如更广义的空间约束，区分和compartmentaliza- tion，或粗粒度的分子动力学在基于规则的语言，将在未来的工作中探索的定义和实施。1.1相关工作在[14] Gruenert et al.介绍了一种通过将粗粒度的基于粒子的空间模拟与用于触发粒子之间的缔合和解离事件的基于规则的语言相结合来模拟组合复杂化学系统的方法与我们的方法不同，模拟不仅处理空间约束，而且根据力场和微分项的组合来跟踪和更新单个粒子的位置，这些力场和微分项分别模拟粒子之间的相互作用及其布朗运动。另一个基于粒子的生物系统模拟器是BioShape [4]。BioShape是一个基于进程代数的独立于规模的仿真环境26诉Danos等人/理论计算机科学电子笔记313（2015）23(a)（b）第（1）款图1. (a)酵母蛋白酶体20S核心颗粒（PDB ID 1RYP）的结构。使用PyMol创建的图像。（b）蛋白酶体结构示意图组成蛋白质的催化β亚基内部两个环以蓝色显示，组成两个外部环的α亚基以绿色显示。图片取自Wikipedia。对于系统生物学，形状演算[1]，其中每个过程都被分配了位置，速度和质量。进程根据物理定律移动，并可以根据它们在某些通道上的通信与其他进程碰撞和绑定。Cardelli和Gardner的3 π [ 5 ]是使用过程代数描述空间现象的一种不同方法3π是一个几何进程代数，它将π演算的交互原语与几何变换相结合。3π中的过程是局部化的，并通过移码操作明确地移动. 3π是一个功能强大的进程代数，但并不直接支持生物建模：进程之间的几何约束或运动定律必须显式实现。也没有时间流的概念，尽管可以很容易地从例如随机π演算中本文的其余部分结构如下：在第2节中，我们定义了几何增强Kappa及其随机语义，并概述了一个基本的模拟算法。在第3节中，我们介绍了局部性的概念，给出了局部和非局部Kappa模型的例子，表明局部性一般是不可判定的，最后展示了如何将局部模型简化为无几何模型。第4节载有一些结论性意见，并概述了今后的工作。2几何增强Kappa我们现在将介绍我们对Kappa的扩展作为一种简单的分类语言。下面给出的定义，在很大程度上，是那些给出的定义的直接扩展。[17]和[10]。稍微熟悉Kappa语言的读者会认识到这里介绍的许多概念，例如接触图，站点图和嵌入，作为经典的无几何Kappa中使用的概念的变体诉Danos等人/理论计算机科学电子笔记313（2015）2327Σ.P→P.Σ22.1符号给定一个集合族（Ai，i∈I），我们将它们的不交并记为i∈IAi，即i∈I{（x，i）：x∈Ai}。我们写A−B为两个集合A和B的集差或B在A中的相对补，P（A）为A的幂集，即A的子集，以及A为不相交的并集A+{*}添加如果f：A→B是一个从A到B的映射，我们写f（A）<$B作为它的像（或值域）。 如果f是部分的，我们写dom（f）A作为它的定义域。 如果AJ∈ A是f 的 定义域的子集，则我们记为f|A′对于f到 AJ的限制，|A′：AJ→B，x→f（x）. 我们把从A到自身的IDENTITY映射记为1A。如果R<$A×B是两个集合A和B之间的二元关系，我们有时将其视为部分映射R：A→ P（B），并将其定义域记为dom（R）<$A，即dom（R）={a∈A：R（a）/=<$}，并将其像记为R（A类似地，我们经常将部分映射f：A→ P（B）和g：A→B分别处理为关系f<$A×B和函数关系g<$A×B定义2.1集合A上的部分配对是A上的一个不相关的、对称的和一对一的二元关系，也就是说，A的每个元素至多与A中的一个其他元素相关，并且A中没有元素与自身相关2.2接触图和部位图定义2.2接触图是一个元组C=（A，S，I，N， Λ，I，P，S，Ω），其中• A、S和I分别是代理类型、站点名称和内部状态名称的有限集合，• A → P（S）将站点名称集合分配给代理类型，• Λ（）− {（*，*）}是一个对称二元关系，表示可能的链接在站点之间，• I：N→ P（I）为站点分配内部状态名称• P：A → P（R）将半径的有限集合分配给代理类型，• S：FIG.10为站点分配有限的位置集，以及• Ω：Λ ε2→ P（SO（3））为链（A，a，B，b）分配有限组方向，使得O∈ Ω（A，a，B，b）惠O−1∈ Ω（B，b，A，a）。我们把A∈ A的签名记为λ（A），把λ和Λ分别记为接触图C的集体签名和链接结构。我们经常把接触图的集体签名Λ和链接结构Λ看作集合对和四元组，分别（即，作为对应关系的图形），如上面的Λ，I，S和Ω的定义。 我们称P、S和Ω分别为C的施体、站址和链几何，称组合映射（P，S，Ω）为C的几何。定义2.3站点图是元组s=（V，C，Γ，λ，i，p，s，ω），其中• V是一组有限的代理人，28诉Danos等人/理论计算机科学电子笔记313（2015）23∈∈.Σ∈∈ρ（ v）u图2.站点图的几何图形。 圆圈代表代理u V和v V，灰色箭头代表它们的参考系（或方向）。 网站A σ（ u）和bσ（v）（及其位置s（u，a），s（v，b））用彩色箭头表示链接（u，a，v，b）的 存 在 强制站 点 的绝对位置（u，a）和（v，b）重合。• C是接触图，• Γ：V→ A是将类型分配给代理的映射，• σ=r将站点名称集合分配给代理，• λ（σ）2− {（*，*）}是表示站点之间链接的部分配对• i：σ→ I是将内部状态名称分配给站点的部分映射，• ρ：V→ R是一个部分映射，它为智能体分配半径• s：σ→R3是一个局部映射，它为位点分配位置• ω：λ<$σ2→SO（3）是将方向ω（u，a，v，b）分配给链路（u，a，v，b）的部分映射，使得（u，a，v，b）∈ dom（ω）<$ω（v，b，u，a）= ω（u，a，v，b）−1.我们称r为s的接触映射。 具有接触图Γ的站点图s被称为定义良好或类型良好，如果(i) Γ保持链接：（u，a）λ（v，b）<$（Γ（u），a）Λ（Γ（v），b），(ii) Γ保留存根：（u，a）λ*<$（Γ（u），a）Λ*，(iii) Γ保持内部状态：（u，a）∈dom（i）<$i（u，a）∈I（Γ（u），a），(iv) Γ保持代理几何：ρ<$P <$Γ，(v) Γ保持场地几何：（u，a）∈dom（s）<$s（u，a）∈S（Γ（u），a），并且(vi) Γ保留链路几何形状：（u，a，v，b）∈ dom（ω）<$ω（u，a，v，b）∈ Ω（Γ（u），a，Γ（v），b）.我们将只考虑定义良好的网站图我们把σ和λ分别称为s的集体接口和链接结构，我们把σ（u）称为智能体u的接口。对于一个主体u和一个场地a∈σ（u），我们说（u，a）是有界的，如果<$（v，b）：（u，a）λ（v，b）.相反，我们说（u，a）是自由的或（u，a）有一个存根，如果（u，a）λ *。我们称ρ，s和ω分别为s的施事几何、场所s（v，b）vs（u，a）ρ（ u）ω（u，a，v，b）诉Danos等人/理论计算机科学电子笔记313（2015）2329几何和链几何，称组合映射（ρ，s，ω）为s的几何。位置（u，a）的位置s（u，a）是相对于代理联合如果定义了链路（u，a，v，b）∈λ的方向ω（u，a，v，b），则站点（u，a）30诉Danos等人/理论计算机科学电子笔记313（2015）23⎛⎜⎜⎝{›→}{→−›→}⎛⎜⎝⎜⎝⎛⎜Vs={u,v},C,Γs={u›→A,v›→A},σs=Σ◦Γs,⎞⎟和（v，b）被认为是对齐的，并且ω（u，a，v，b）对应于v相对于u的取向。图2示出了根据本发明的一个实施例的半导体器件的几何形状的各种部件。网站地图如果有路径，则称站点图s的两个代理u和v是连通的（u，a）λ（w1，c1），（w1，CJ1）λ（w2，c2），.，（wN，cJN）λ（v，b）在s中连接u和v。一个站点图s是连通的，如果s中的每对代理（u，v）∈V2是连通的.定义2.4一个站点图（V，C，Γ，λ，i，ρ，s，ω）被称为完备的，如果它的集合接口，链路结构，状态映射和几何都是关于到它的接触图，也就是说，• （r（u），a）∈dom（Λ）<$（u，a）∈dom（λ），• （Γ（u），a）∈dom（I）<$（u，a）∈dom（I），• dom（ρ）= dom（P<$r），• （Γ（u），a）∈dom（S）<$（u，a）∈dom（s），• （r（u），a，r（v），b）∈dom（Ω）<$（u，a，v，b）∈dom（ω）.不完整的站点图称为局部站点图。注意，站点（u，a）的链接状态λ（u，a）或内部状态I（u，a）可以在完整站点图中保持未定义，只要接触图中的对应站点（r（u），a）的可能链接状态Λ（r（u），a）或内部状态I（r（u），a）的集合为空。 类似地，一个完整的几何增强的站点图不需要定义其所有的几何，只要在接触图中未定义相应的几何部分即可。这使我们能够将普通的、无几何的站点图（如[8]中定义的站点图）视为几何增强的站点图的特例。 它还允许我们建模半刚性结构，即只有某些子结构受到刚性几何约束的结构。现在让我们来看看一些联系人和网站图的例子。我们的第一个例子介绍了一组简单的小图，我们将在这一节中建立这些图来说明几何增强型网站图理论的各种概念。例2.5考虑以下接触图C和两个位置图t和s的定义：A={A}，S={l，r}，I=N，N ={A<$→l，A<$→r}，C=Λ ={（A，l，A，r），（A，r，A，l）}×{}{}×，I=，P= A1，S=（A，l）（2，0，0），（A，r）（ 2，0，0），Ω=，（A，l，A，r）<$→，1，Rz.ππ，，（A，r，A，l）<$→，1，Rz. −π，，2但是，2Vt={ u}，C，Γt={u<$→ A}，σt= ππΓt，t=λt=σt× {ε} ε { ε}× σt，ιt= ε，ρt={u<$→1}，st={（u，l）<$→（−2，0，0），（u，r）<$→（2，0，0）}，ωt=ω但是，s=λs={（u，l，n），（v，r，n），（n，u，l），（n，v，r）}，it=n，ρs={u<$→1，v<$→1}，、⎟⎠诉Danos等人/理论计算机科学电子笔记313（2015）2331ss={（u，l）<$→（−2，0，0），（v，r）<$→（2，0，0）}，ωs=ω32诉Danos等人/理论计算机科学电子笔记313（2015）23、、、⎜⎟⎜7Λ ={（β，lt，β，rt），（β，rt，β，lt），（β，lb，β，lb），（β，rb，β，rb）}×{}{}×，7722142214⎟yz22B测试：s：x：y：（一）(a)(b)图3.联系图和站点图的示例x=Vs，C，Γs，σs，λx ={（u，l，v，r），（v，r，u，l）}，ιs，ρs，ss，、ωx={（u，l，v，r）<$→1，（v，l，u，r）<$→1}，Vs，C，Γs，σs，λy={（u，l，v，r），（v，r，u，l）}，ιs，ρs，ss，，y=ω=，（u，l，v，r）<$→R. ππ，（v，r，u，l）›→ Rz. −π，，其中1是恒等式，Rz（θ）是θ绕z轴的旋转角图3a示出了四个位置图s、t、x和y。直观地，接触图C使得能够构造具有90°匝的线性链。 站点图t表示单个未连接的代理，而s表示可以连接以形成长度为2的链的一对代理。请注意，网站的链接状态s中的代理u和v的r∈σ（u）和l∈σ（v）是未定义的。 两个站点图x和y分别是线性扩展和转弯的示例。 t、x和y都是连通的，而s不是。t是完全的，而s、x和y不是。现在，让我们来看看一个更复杂的系统，即蛋白酶体的两个内环。图3b显示了这种结构的可能的位置图表示。例2.6在由蛋白酶体β亚基形成的两个内七聚体环的组装模型中，像图3c所示的无几何接触图将是一个明显的选择。我们通过添加相应的几何形状来扩展此接触图，如下所示：A={β}，S={lt，rt，lb，rb}，I={β，β={β <$→lt， β<$→rt， β<$→lb， β<$→rb}，⎞⎟P={β→. 1}，ππ77B.，π πC=（β，l t）›→−cos，sin，0，（β，r t）›→cos，sin，0，S=（β，l）›→。−1，1tanπ，−1，（β，r）›→。1，1tanπ，−1，（β，lt， β，rt）›→Rz。−2π，（β，rt， β，lt）<$→Rz. 2π，， πΩ=（β，l，β，l一一一一一ββββββββββββββ一一β.7BBz7yBBz7y诉Danos等人/理论计算机科学电子笔记313（2015）2333）›→R. −πR（π），（β，r，β，r）›→ R. πR（π）接触图C允许我们构建如图3b所示的站点图。事实上，图3b的站点图是最大的声音站点图，其中C为它的接触图。我们将定义站点图的合理性意味着什么，第2.6节。34诉Danos等人/理论计算机科学电子笔记313（2015）23∈2.3嵌入定义2.7从一个站点图x到另一个站点图y的嵌入是一个映射f：Vx→Vy，使得(i) f是内射的。(ii) f保持类型：Γx= Γy<$f，(iii) f保留位点：σx<$σy <$f，(iv) f保持链接：（u，a）λx（v，b）<$（f（u），a）λy（f（v），b），(v) f保留存根：（u，a）λx*<$（f（u），a）λy*，(vi) f保持状态：（u，a）∈dom（ix）<$ix（u，a）=iy（f（u），a），(vii) f保持代理几何：ρx <$ρy<$f，(viii) f保持场地几何：（u，a）∈dom（sx）<$sx（u，a）=sy（f（u），a），(ix) f保留链接几何图形：（u，a，v，b）∈ dom（ωx）<$ωx（u，a，v，b）= ωy（f（u），a，f（v），b）.我们写[x;y]为从x到y的嵌入集合。 当f[x; y]时，我们写Fx−→y，并且说y嵌入x，或者x通过f嵌入y。我们写f（x）对于y，f∈[x;y]的靶点图，不要与f的图像f（Vx）<$Vy混淆。站点图和它们的嵌入一起形成几何增强的站点图的类别GS，站点图作为对象，嵌入作为箭头。在本文档的其余部分，我们将互换使用术语对象和站点图，以及术语嵌入、态射和箭头。嵌入的概念为我们定义子图提供了一种直接的方法一般事务人员职类：定义2.8站点图t是站点图s的站点子图，记为ts，1Vt如果V≠V且t s.称一个站址子图对于某些性质是最小的t s−→ jJ JP如果，对于P成立的每一个其它的站址子图t∈s，t∈t蕴涵t=t，如果t<$tJ意味着t=tJ，则对P是最大的。 称一个站址子图s[W]s是诱导的，如果给定其代理集Vs[W]=W，它是极大的。一个站址图t是s的连通分支，如果它是s的一个极大连通站址子图。在这一点上，似乎应该注意到，尽管许多图论概念，如子图、连通分量、路径等以直观的方式扩展到站点图，但由于每个站点一个链接的限制和注入性，站点图的类别也具有一些令人惊讶的性质morphisms。其中一个特性是刚性：引理2.9（刚性）设x和y是图，且x连通，则从Vx到Vy的任意非空部分注入f在[ x ; y ]中至多有一个嵌入.诉Danos等人/理论计算机科学电子笔记313（2015）2335这是一个已知的结果，从理论的geometry-less网站的图形，它的扩展不变的几何增强网站的图形。我们建议感兴趣的读者参考[17，10]的证明。引理2.9的一个推论是，存在一个多项式时间算法来计算嵌入数|[s; x]|即计算x中与s同构的子图的个数。这是[8]中提出的Kappa模型的有效模拟算法我们用GSC表示具有接触图C的站点图的子范畴。在几何增强Kappa的其余部分中，大多数定义都是相对于给定的GSC而不是GS来制定的。这种限制反映了这样一种直觉：在某些生化过程的背景下，给定类型的基本分子的活性位点（由某种媒介类型A∈ AC的界面A（A）表示），其潜在构型集（I（A），P（A），S（A）），以及其与其他类型分子的潜在相互作用（Λ（A），Ω（A））都是固定的，而不管A的特定实例在何处以及如何嵌入某些分子复合物中。2.4行动和规则为了定义站点图上的重写规则，我们需要能够将应用给定规则之前和之后的站点图。一种选择是从图重写中扩展一种经典的语义方法，例如double或单推出重写，已被定义为几何无Kappa [6，10]。相反，我们将采用动作脚本作为序列的更多句法概念 原子重写指令，这已被广泛用于Kappa文献[8，17]。定义2.10在GSC中的位置图s上的原子作用α是以下之一：•GSC中完全站点图t的子图加法+t，• 在GSC中的完全站点图t的子图删除-t，• 一个环加法+（u，a，v，b，Q），其中方向Q∈Ω（u，a，v，b）<$，• 连接缺失−（u，a，v，b），• 状态变化I（u，a）←p到p∈I（u，a），• 半径ρ（u）←r到r∈P（u）的变化，• 站点位置s（u，a）←p到p∈S（u，a）的变化，或• 当u∈Vs，v∈Vs，a∈σs（u），b∈σs（v）时，链环方向ω（u，a，v，b）←O变为O∈Ω（u，a，v动作α =（α1，α2，...，αN）是原子作用序列αi在（αi−1·αi−2···α1·s）。链接的添加和删除是对称的。我们用α·s表示GSC中原子作用α对s的结果。一个作用α在s上是良好定义的，如果它的结果α·s是36诉Danos等人/理论计算机科学电子笔记313（2015）2320. ..ΣΣΣαs α·sff（α）α·fxf（α）·x=（α·f）（α·s）图4. 图中的各种物体、箭头和动作定义在s、α、x和f上。一个定义明确的网站图。一个定义良好的链路加法的参数Q可以是Q=*iΩ（u，a，v，b）=Ω，在这种情况下，ωα·s（u，a，v，b）保持未知。 链接删除仅适用于完整的链接。我们只考虑今后的明确行动。行动结果的正式定义见附录A.1。给定GSC中两个位图s和x之间的嵌入f∈[s;x]，我们将原子作用α沿f的传递f（α）定义为原子作用序列f（αi），使得每个f（αi）在x中s的像的对应位子图上执行作用αi的模拟（形式定义见附录A.2）。如果s和x都是GSC中的位置图，则α是s上的定义良好的作用，并且f∈[s;x]，则上述定义确保(i) α沿f的迁移f（α）是明确定义的，(ii) 有一个反作用α−1使得α−1·α·s=s，(iii) 如果x是完备，那么f（α）·x也是完备的，(iv) 存在唯一的映射（α·f）∈[α·s;f（α）·x]，称为作用α的结果在f上，使得（α·f）（α·s）=f（α）·x（详见A.3）。图4展示了在s、α、x和f上定义的各种对象、箭头和动作。使用上述定义，我们现在可以定义站点图重写系统的规则例2.11设t、s、x和y如例2.5所定义，则我们可以定义两个动作α1和α2如下：α1=+（u，l，v，r，1）， α2= + u，l，v，r，Rz−π，+t。那么α1是定义在s上的原子作用，它给s增加了一个直链，即，α1·s=x.α2是定义在s上的一个非原子动作，它首先给s添加一个链接（90度转弯），然后添加子图t，即α1·s= +t·y。定义2.12规则是一个三元组r=（s，α，k），其中s是一个位点图，α是定义在s上的一个作用，k∈ R+是一个速率。例2.13设t和s如例2.5所定义，α1和α2如例2.11所定义，那么我们可以定义两个规则r1和r2如下：r1=（s，（α1，+t），k1），r2=（s，α2，k2）.诉Danos等人/理论计算机科学电子笔记313（2015）2337ΣΣΣ0.r1：r2：k1k2图5.表示示例2.13的规则集的图。最后，我们准备好定义我们的几何增强Kappa模型的概念。定义2.14Kappa模型是一个对K =（x0，R），其中x0是GS C K中的一个完整的位点图，称为K的初始状态，R ={r1，r2，.，rN}一个有限的规则集ri =（si，αi，ki），称为K的规则集，其左侧si在GSCK中。为了简单起见，我们将在下文中写GSK而不是GSCK。例2.15令C，t，s，r1和r2如例2.13所定义。然后我们可以定义Kappa模型K=（x0，R），初始状态x0= +t·t，规则集R={r1，r2}。2.5事件和概率每个Kappa模型K在完整的站点图上都有一个相关的加权标记转换系统（WLTS）[13定义2.16设r=（s，α，k）是一条规则，R是一组规则，x是一个完全的站点图。我们定义• 与r相关联的x中的事件的集合为E（x，r）= [s;x]，• 与R相关的x中的事件集合为ER（x）=r∈RE（x，r），• r在x中作为a（x，r）= k活度|[s; x]|得双曲正弦值.• R在x中的活动为aR（x）=r∈Ra（x，r）。这为每个Kappa模型K=（x0，R）定义了一个WLTSWK=（KK，ER，w，π0），其中• 状态空间KK <$GSK，GSK中的完全站点图类，• 标号ER=x∈KKER（x），KK中与R相关的事件的集合，• 权函数w：ER× KK→R+定义为w（x，e，XJ）= k如果e=（（s，α，k），f）∈ ER（x）且XJ=f（α）·x，0否则，• 初始概率分布π0=1{x= x0}。一一一一一一一一一一38诉Danos等人/理论计算机科学电子笔记313（2015）23aR（x）e1e2.Σ2.Σ123−→ · · ·−−−→A跃迁x−→e xJ，在WK中有概率yP{x−→e xJ}=w（x，e，x′）如果R（x）>0，并且随后的时间提前量是指数随机变量δt（x），使得P{δt（x）> t}= e−aR（x）t。如果有一系列跃迁，我们写x1→n×Nx−→ x−→xN−1x在WK中，其中w（xi，ei，xi +1）> 0，并且用reach（K）<$KK表示K的可达状态集：reach（K）={x：x0→<$x}。2.6实现和限制定义2.17几何增强的站点图s的实现π：V→ R3×SO（3）是s在三维欧几里德空间中的嵌入，即映射u<$→（r（u），R（u）），它将位置r（u）和方向R（u）分配给代理u∈V。给定一个站点图s的实现π=（r，R），我们称r和R分别为s的位置图和方向图我们现在可以定义站点图和Kappa模型的几何可靠性约束定义2.18具有相关几何（ρ，s，ω）的位置图s称为：sound当且仅当存在s的实现π=（r，R），使得• 对于s的链结构中的每个链（u，a，v，b）∈λ，（u，a），（v，b）和（u，a，v，b）的几何是一致的，即，n（u，a，v，b）∈dom（ω）dom（s）2：R（v）=ω（u，a，v，b）R（u）r（v）+R（v）s（v，b）=r（u）+R（u）s（u，a）和• s中没有冲突，也就是说，n（u，v）∈dom（ρ）：u=/vr（u）−r（v）≥ρ（u）+ ρ（v）。我们用G表示几何上合理的站点图的集合，s∈ G，如果站点图s是健全的。我们说一个Kappa模型K=（x0，R）在几何上是可靠的，如果它的初始状态x0在几何上是可靠的。我们说，一对代理（u，v）在一个网站图s的几何连接如果u和v由具有完全特定几何的链路（w，a，wJ，b）组成的路径连接：（w，a，wJ，b）∈dom（ω）dom（s）2。我们说s是几何连通的，如果s中的每一对（u，v）∈V2都是几何连通的.设s是 具有几何连通分量{c1，c2，...， cN}，则我们有s∈ G惠i≤N：ci∈G，Ne3诉Danos等人/理论计算机科学电子笔记313（2015）2339+^ ^您的位置：.^^^因为没有几何连接的任何代理可以位于任意远的位置而不违反任何可靠性约束。很容易看出，如果在s的每个几何连通分量ci中固定任意主体ui的位置r（ui）和方向R（ui），则定义2.18中的方程组变得过约束。 这是一个简单的O（n2）算法（其中n = 1）。|λi|）计算一个点图s的可靠性s∈G：对每个ci∈s(i) 设r（ui）=0且R（ui）=1，对任意代理ui∈Vi，(ii) 求解并检查其余（r，R）的可靠性方程|Vi通过遍历i|λi|）时间），(iii) 1）在O（）中，i = 0（|Vi|2）时间）。详见附录B中的算法B.1定义2.19设WK=（KK，ER，w，π0）为与几何上合理的Kappa模型K=（x0，R）相关的WLTS，则几何上合理的过渡系统wJ：ERJWK定义为WLTSWK =（KK，ER，wJ，π0），具有权函数× KK→ R0定义为w（x，e，XJ）= k如果e=（（s，α，k），f）∈ ER（x）且XJ=f（α）·x且XJ∈ G，0否则。（r，f）换句话说，WK是WLTS，其中跃迁x−→f（αr）·x限制为WK中f（αr）·x是合理的那些跃迁假设我们从一个几何上合理的初始状态x0开始，一个几何上合理的过渡系统WK将只沿着其状态x0→x xx也是几何上合理的轨迹演化。利用算法B.1，我们可以修改Kappa系统的著名模拟算法[8]，只要算法B.1返回f（αr）·x∈/G（对于状态x中的某个ve nt（r，f）），就通过生成零事件（即没有跃迁的时间推进）来有效地模拟任何几何上可靠的模型K的W K。3局部性在本节中，我们将介绍Kappa模型局部性的概念。局部性背后的核心思想如下：如果可以通过只检查f（α）·x中右侧图像α·s周围的有限数量的上下文来决定任何事件（（s，α，k），f）∈ ER（x）是否会产生一个健全的站点图f（α）·x，则Kappa模型K=（x0，R）被称为局部的。 请注意， 局部模型与非局部模型的对比只对几何增强的Kappa有意义，因为所有无几何的站点图在定义上都是几何上合理的，因此无几何的Kappa模型中的事件永远不会产生几何上不合理的图。实际上，非局部Kappa模型的存在是几何增强Kappa和无几何Kappa之间40诉Danos等人/理论计算机科学电子笔记313（2015）23⎪2M超声波清洗机2N（一）M⎩N（b）第（1）款图6.例2.15中模型K的可能状态：（a）有2（N + M）−1个链环和一圈的开链;（b）有2（N + M）− 1个链环但有三圈的几乎闭链。为了使局部性的概念更精确，我们首先需要定义我们所说的上下文到底是什么意思。为此，我们将使用封闭球的概念，在一个网站图的代理的子集。定义3.1给定一个站点图s的一对连通主体（u，v）∈V2，u和v之间的距离d（u，v）定义为u和v之间的最短路径的长度，即最小链接数。定义3.2站点图x的代理u∈Vx周围半径为δ的闭球Bδ（u，x）定义为位于x中u的距离δ内的代理Bδ（u，x）={v∈Vx：d（u，v）≤δ}的集合。围绕嵌入f∈[s;x]的半径为δ的闭球Bδ（f）是诱导位子图Bδ（f）=xu∈VsBδ（f（u），x）≠.定义3.3Kappa模型K=（x0，R），初始状态x0，规则集R为对于一个有限半径δ∈ N，称之为δ-局部的，如果对每个状态x∈reach（K）在K中可达，规则（s，α，k）∈R，嵌入f∈[s;x]，则下列成立Bδ（α·f）∈ G <$f（α）·x ∈ G.称K是局部的 ，如果存在一个有限半径δ ∈ N使得K是δ-局部的。我们用Lδ表示δ-局部Kappa模型的集合，用L=iLi 表 示局部Kappa模型的集合。例3.4为了证明确实存在非局部Kappa模型K∈/L，考虑Kappa模型K=（x0，R），如例2.15所定义：在n个事件之后，该模型的状态xn∈reach（K）由两个或多个连通分量组成，这些连通分量要么是A型自由主体t，要么是由m+ 1个A型主体wi组成的开链cm，m≤n，相邻主体wi和wi+1通过m个链接（wi，l，wi+1，r）相连，要么是环，即已经闭合的链。一个给定的状态xn可以包含许多环，但最多包含两个自由主体t，或者一个自由主体t和一个开链cm。大多数事件将连接单免费⎧⎪⎨⎪⎩⎧⎪⎨⎪⎩诉Danos等人/理论计算机科学电子笔记313（2015）2341代理t到现有链cm，产生新链cm+1。 涉及规则r1的事件在现有链cm的一端创建了而规则R2分别在CM的L端或R端创建左转或右转。r1和r2也为cm+1的进一步扩展创建了一个新的自由主体t。有时，模型会产生链c2N+2M−1，如图6b所示，它可以被事件（r2，f={u<$→w2N+2M−1，v<$→w0}）闭合成一个N×M维的矩形环rN，M。给定任意δ∈ N，设x2δ+1=+t·c2δ+1是一个站点图，其中c2δ+1是一个如图6a所示的链，N=δ，M=1，设f2δ+1={u<$→w2δ+1，v<$→w0}，其中w2δ+1和w0分别是c2δ+1的l-端和r-端的主体显然，x2δ+1∈reach（K）和f2δ+1∈ E（x2δ+1，r2）.假设我们将f2δ+1（α2）应用于x2δ+1，也就是说，我们试图闭合链c2δ+1。那么所得到的站点图f2δ+1（α2）·x2δ+1一定是不可靠的，因为链c2δ+1的圈数太少而不能闭合（只有圈数为3或更多的链，如图6b中的链，才能闭合，）. 然而，封闭球Bδ（α2·f2δ+1）是可靠的，因为它不是封闭的（施事wδBδ（α2·f2δ+1））中缺失 我们的结论是Bδ∈N：Bδ（α2·f2δ+1）∈G<$f（α2）·x2δ+1∈/G，因此K∈/L。3.1局部性的充分条件以下是模型K局部性的充分条件：(i) 一个模型K是局部的，如果它的接触图CK是无圈的。正如我们在2.6节中所看到的，如果一个站点图x的所有连通分支cx都是合理的，则该站点图x如果CK是非循环的，则没有连通分支c可以具有比C K中的主体类型更多的主体，即，|Vc| ≤ |一个K|.因此，（s，α，k）∈RK可以在大于δ =的距离上选择任何agent。|一个K|在它的左手边s周围，它遵循K是|一个K|- 本地的