Agent数目守恒的规则系统的随机语义分解、抽象和重构方法

⋆可在www.sciencedirect.com在线获取理论计算机科学电子笔记284（2012）105-124www.elsevier.com/locate/entcs模型分解与随机碎片Arnab Ganguly2 Heinz Koeppl3瑞士苏黎世联邦理工学院自动控制实验室摘要本文讨论了Agent数目守恒的规则系统的随机语义的分解、抽象和重构方法。提取是通过计数片段而不是种类来诱导的，片段是分子信号传导中的标准信息实体。规则集可以分解为更小的规则集，从而使整个规则集的基于片段的动态性是由更小的规则集组成的基于物种的动态。基于物种的瞬态动力学的重建是可能的某些初始分布。 我们证明，如果一个规则中的所有规则集合是可逆的，基于物种的动态重建总是可能的平稳分布。 我们使用的胶体聚集的案例研究表明，该方法可以减少状态空间指数相对于标准的，基于物种的描述。保留字：细胞信号，连续时间马尔可夫链，集总性介绍信号蛋白的多位点翻译后修饰[22]和构象变化[4，21由于化学动力学[11]是基于完整分子复合物的描述来操作状态的，因此模型往往变得过于复杂而无法分析。这需要分解技术，即确定状态空间的有效维度。 作者在[2，5，7，9]中提出了他们首先构建的方法然而，在[14]中，我们采取了自底向上的方法，观察了每个代理的有效自由度，表示为代理Heinz Koeppl和Arnab Ganguly感谢瑞士国家科学基金会的支持，批准号PP00P 2 128503。Tatjana Petrov感谢来自SystemsX.ch的支持，这是瑞士系统生物学倡议。1电邮地址：tpetrov@control.ee.ethz.ch2电子邮件地址：gangulya@control.ee.ethz.ch3电子邮件：koeppl@ethz.ch1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.05.018106T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105（=（）== ）=的n（i，i，i）i i个A设置（x，y）到（ 0， 0）的实例，以及n（i，i）i2，i3，i4个A设置的实例（（）=（））=（=）（=））（）（）∈{（）}+=}（）联系我们x和y变量在时间n∈N时设置为1。 x和y的独立性使得即Zn=（0， 1， 1， 0），或A的不同实例，即Zn=（1， 0， 0， 1）.因此，我们认为，（（）=（））=（ ∈{（）（）}）意见.这是因为用于指定反应的语言Kappa允许通过使用位点图而不是无结构变量对反应物进行符号编码。分解是通过检测来执行的，例如，代理接口的一个站点上的修改永远不会影响同一代理接口上的另一个站点的状态。等价的观察在随机碎片的框架中被利用[8]，[9]为了说明分解和随机片段背后的思想，考虑包含两个布尔变量x和y的编程模块A。变量的值作为离散时间随机过程而变化，因此每个变量的下一个值仅取决于同一变量的当前值。假设模块可以被实例化多次，并且所有实例都并行运行。例如，考虑模块A的两个实例：A1和A2。设Z ni1，i2，i3，i4i1 I2 I3 I42表示状态i1，i2，i3，i4 在时间x，y分别为0，1，1，0和1，1。 由于变量x和y的独立更新，我们可以将模块A分解为两个较小的模块y.设随机变量X n0， 1， 2和Yn0， 1， 2表示我们可以计算正确的联合概率，例如，一个变量的状态x设为1，一个变量y设为1：PX，Yn1，1 P X n1 P Y n1 .一、 取值为1的站点x和y可能属于A的同一个实例，即PX，Yn一，一P Z n0， 1， 1， 0， 1， 0， 0， 1. 最后，已知有一个变量x设置为1，并且有一个变量y设置为1，则它们属于A的同一实例的条件概率为P Zn1， 0， 0， 1Xn 1和Yn10。5. 沿着这些思路，我们证明了基于规则的系统的分解[14]产生了计数碎片[9]而不是物种，并且我们可以通过只分析抽象系统来有效地重新构建关于具体系统的信息。我们首先对基于规则的模型进行编码，并将随机语义分配给它。在第2节中，我们详细介绍了如何对基于规则的模型进行编码在第3节中，我们定义了基于片段的抽象，以及如何将规则集分解为更小的独立单元。在定理3.6中，我们证明了这两个框架是如何联系的。在第四节中，我们使用了一个胶体聚集模型，以证明该方法可以指数减少状态空间。最后，在第5节中，我们回顾了使用基于片段的抽象的实践方面。特别地，基于物种的系统上的概率分布可以从某些初始分布的基于片段的抽象中重建。我们在定理5.2中表明，重建是适用于一组可逆的规则，regardless的初始分布，因为潜在的过程是一个非爆炸性的，不可约的CTMC与平稳分布。T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105107=（）●∶ × × →≥W（s，s′）=∑l−∑l∈L（）≠a（s，l，s）>0，也就是说，能够从s过渡到s的值。s）L（s）=。（）∈ ×∈′Var 分别，使得L<$L=，Var<$Var=。产品展示2 1 2 12x：Var→ {0， 1}。解释函数L ∶S→ Var（Var→ {0， 1}）指定为：● S=S×S，12iLf（分配给不同状态的属性集s′是不相交的：如果s∈s，Var=Var<$Var（符号<$表示不相交的并集），使得12（定义1.2（两个ILTS的C ross-product）考虑两个ILTS：M1，L1=s，s∈S，s，s∈S，l∈L和l∈L。11221 1 2212张力的功能L4的一组变量Var等于它们的Kr oene ckersumW=W<$W[3]。换句话说，存储过程12设（Xt）是状态空间S上的CTMC，其生成矩阵为1ML=M1，L1×M2，L2是定义在变量集上的ILTSML=（S，L，a）1预赛我们将经典随机化学动力学的框架嵌入到标记过渡系统（LTS）的形式主义中[18]。LTS的随机语义被定义为连续时间马尔可夫链（CTMC）。定义1.1（解释标记转换系统-ILTS）标记转换系统（LTS）是一个元组MS，L，a，其中S是状态的有限集合，L是一组有限的标签，● aSLSR 0是跃 迁 的活度。拉瓜岛∑l∈L，s′′∈Sa（s，l，s′′对于s s′） ，则s =s′。对于任何一对状态s，s′S S，将至多有一个标签l L，使得为了给LTS的状态分配一组属性，我们引入了布尔变量Var。属性由相应的估值编码：每个状态s∈S是一组赋值。被解释的LTS（ILTS）ML是良好定义的，两个ILTS它们的变量集互不相交。S1，L1，a1）和M2，L2=（S2，L2，a2），在一组变量Var1和● L=L1L2，"● a（（s1，s2），l1，（s1，s2））=a1（s1，l1，s1），且a（（s1，s2），l2，（s1，s2））=a2（s2，l2，s2），对于● L（（s1，s2））= L1（s1）<$Var<$L2（s2）<$Var，其中符号L1（s1）<$Var表示前-若ML1和ML2的生成元分别为W1和W2，则ML2的生成元矩阵分配给ML的过程可以看作是并行运行的过程M1、L1和M2、L24对于小的y，L1（s1）<$Var={x∈（Var→{0，1}）<$x <$Var∈L1（s1）}.●108T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105对所有的s，s∈S。111M2=（S2，L2，a2）是同构的，记为M1<$M2，如果它们的生成子是等式a-′两种等价关系：S×S和L×L。ILTSM=（S，L，a）是nlLs∈[′s]∑′a（s，l， s）=∑ ′a（s，l，s）;and12l∈L，s∈Sl∈L，s∈Sa（s，l，s）>0且a（s，l，s）>0，则a（s，l，s）=a（s，l，s）;11221212[]引理1.5（有效抽象）给定ILTSML=（S，L，a），M<$ L<$=（S<$，L<$，a<$）是有效的。集总状态[s]由包含的解释的联合来解释对于s，s1，s2∈S，使得s1<$s2，在两个集合之间存在一个双射设“[s]，[l]l，s]为从类到类的转换数● 每两个集总状态是后向均匀双相似的： 如果s1<$s2，且s∈S，s]s∈[s]，s′∈[s′]，l∈[l]la（[s]，[l]，[s′]）=a（s，l，s′）[[s]，[l]，s′][s′].抽象可以计算为相同的活性，（ii）每两个集总状态具有相同的总活性，以及（iii）当考虑底层CTMC的生成矩阵时，我们需要同构LTS的概念定义1.3（同构LTSLent，即，如果存在一个双射α∶S1→S2，使得W1（s1，s1）=W2（α（s1），α（s1））定义1.4（ILTS：有效抽象）考虑ILTSML=（S，L，a），并由y_n和y_l导出ML的抽象，使得S_n=S/n，L_n=L/n，并且a<$（[s]<$，[l]<$l，[s′]<$）=<$[1∑ a（s，l，s′）.状态：L（[s]）=′ L（s）.状态s∈S通过类[l]l. 抽象M<$ L<$=（S<$，L<$，a<$）是有效的，如果● 所有的lumpe′d标签建立了相同的活动：i′fl1<$l2和s1，s′1，s2，s′2∈S，● 每 两 成块的 国 有 相同的总活动：如果 S1 ∼S2，则则[[s]′n，[l]nl，s1]=[[s]n，[l]nl，s2]。′固定s，s∈S。状态[s]和[s]之间的活动通过有效的ll [s]抽象有效的条件在文献中被称为弱集块性（英语：weak lumpability）[13]或一致向后互模拟。在第2.1节中，分配给基于规则的模型的ILTS是这样的，每个状态都由来自VAR的变量的一个估值来解释。集总状态s由一个联合在包含状态的解释下面的引理提出了一个证明抽象有效的标准。alence关系：S×S和lL×L，如果（i）所有集总标签建立s1（s2）在类[s]中的sors，通过类[l]中的标签，然后抽象T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105109′ ′′MbyS={{s，s}，{s，s，s}}和L={{1，1，1，1}}。（图1）由于定义1的条件。412122 12L是一个有一个接口，即一组站点站点可以是内部站点，=E <${（（）（））<$（）（）∈V∈ ∈}′′L4D{（定义2.1（Sitegraph））Sitegraph是一个对G=（V，E），使得V定义2.2（注释站点图）注释站点图（V，E）是一个站点A，s），（A，s））∈ A，s∈ <$（A），s∈<$（A）}.′.[11]L[s1].[s]图1.一、V是LTS的一个概括. （左）LTS=（S，L，a），s u chS={s，s′，s1，s′1，s2，s′2}，′ ′′′L={l1，l2，l1，l′2}。 a（s′，l1′，s1）=a（s，l2，s2）=a（s′，l1′，s1）=a（s，l2，s2）=k. 抽象是诱导的满足，抽象是有效的，并且集 总 状 态 之 间 的活动是a（[s1] k，[l1] k，[s] k）= 2 2k = k。从DFN中可以明显看出这一点一点四2基于规则的模型：布尔编码和语义在本节中，将定义一个基于规则的系统，并说明如何将ILTS与之关联。该模型是基于一组代理名称和一组站点名称. 代理人通常模型蛋白质，和网站模型蛋白质结构域。 每个代理结合位点，但不是两者：吉吉好吧 假设每个站点处于两个修改状态之一，分别用0和1表示。 特别地，结合位点具有键当且仅当其修饰态为1。我们使用站点图来形式化模型。A，<$i，<$l） <$A∈ A且<$i，<$′l<$′<$（S）}是no′des′的集合，结合位点，A，s，A，sA，A，pH1，pH1，A，pH2，pH1，pH2，pH1 ，是一个一组边缘。 边的集合是对称关系。g{r（a（ph（V，E′），′），具有n个年龄nt-位点对的等价关系：在基于规则的建模中，我们使用站点图来形式化不同类型的对象（我们在第二节中正式定义了这些对象中的每一个2.1）：接触图是总结蛋白质名称及其可能结合的位点图[6];带注释的接触图是带注释的位点图;两个位点按注释关系分组，以形式化它们的值在感兴趣的行为（本文中为随机化学动力学）中彼此依赖（相关）;反应混合物图用于编码系统的一个状态，即整个反应混合物。它是一个站点s1。S.2s ′。1L1l2l1′.s ′。勒2.2S′●●●110T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105图，通过复制节点和边给定的次数，从接触图构建。T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105111A，v）和（A，v）的联系人地图。<${（）<$∈A∈S}<$E（紫外线系统中每个代理可以有更多的副本：假设n（A）个副本（A，B）V ={（（）（））<$∈ A =（）}（）下E = {（（）（））<$∈ A =（）=（）}形式上，接触图（V，E）上的反应混合物图是位点图一A、B）ILTS对应于一个反应混合物：L（s）∈（Var→ {0， 1}）。 ILTS文法p<$0$>1<$a∈Var <$$>p<$p<$p。我们用Varp表示变量VarnAi， A， A和i1，...，n A，il尽管通常只有它们的一小部分是可到达的。2.1编码反应混合物假设Var是分配给给定接触图的每个位点的一组变量：Var A，v A，v.对代理A的位点v的值进行编码的变量由vA表示。编码试剂A和B的位点u和v之间的键的变量表示为A的概率，则n B代理B的副本等。代理的每个副本由其上标的数字标识：A1，A2，. 键可以存在于被识别的代理（Vn，En）与一组已识别的代理名称An和站点名称S，使得而这组边是nA i，v，A′j，v′ A，A′和i1，...，nA，j1，...， n A′。设Varn是分配给完整接触图的每个位点的变量集合：Varn<${（A i，v）<$A i∈ An，v ∈ S}<$E n.i、j2019-05-22 00：00分配给代理Ai和Bj的位点u和v之间的键的变量。来自Varn的变量的一个赋值编码一个反应混合物。的每个状态n计数与Varn上的赋值一样多的状态，即S（Varn→ {0， 1}），2.2编码转换基于规则的模型的动力学由一组规则给出。经典化学反应由左手边（lhs）、右手边（rhs）和速率组成lhs是一组反应物，它们可以转化为一组产物，并且转化的类似地，规则的lhs和rhs是在它们的接口中具有不同的站点值的代理的集合假设。我们在这里提出的基于规则的模型受到基于规则的建模框架Kappa [6]的启发，但我们仅限于以下假设：(i) 代理在规则中最多出现一次(ii) 不能通过规则创建或删除代理考虑由下式生成的变量Var上的命题公式P的集合：112T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105（1）={0}（）∈P×P×=通过（i）反应混合物映射（Vn，En），和（ii）规则集R ={R，.，R}。1 mB =（V E R）（V E）●E●=（）∈R{}<$（（）（））∈<$A（（ "“一∶→s）∈<$p[/v]）。称为随机碎片。[和（A，v）<$（A，v）]或[A<$B和（A，v）<$（B，v）]。的等价类若u，v∈<$（A），且ν（u）∈<$（A），则ν（v）也∈ <$（A）. 如果有一个提议例如，如果一个变量v∈Var表示v在ntA时的值，则it∈A现在我们考虑一个反应混合映射（V，E），设V为r×V为sbLy（年龄定义函数ν表示为byp[/ν]。国家s，我解释的是，p =<$v的p[/v]=<$v。当variab leuv∈Var时，Ab可以是A（A，B）甲乙丙在一个连续映射上，它的最小熵是最小的● f′′对相同年龄位点的限制是过渡性的：对于任意a′′gentA∈A，例如，p′[v] =<$u3<$v3。注意，根据定义，一一一一一出现在命题P中。 公式p的满足区域表示为 通过px状态x满足命题p。定义2.3（规则）规则是一个三元组p，q，kR0，使得Varp Varq。定义2.4（基于规则的系统）基于规则的系统B =（V，E，n，R）被定义为如果接触图中的两个点都按某种规则出现，则它们处于随机标注定义2.5（接触图：随机注释，[8]）给定基于规则的系统，自同构对称关系<$$>{（（A，v），（A，v））<$A，A∈A，v，v∈S}，使得形成边缘的每两个位点是相关的，并且如果R p，q，k和vA，v′Varp，则A，v，A，v′，和使得v，v，v∈<$（A），如果（（A，v），（A，v））∈<$且（（A，v），（A，v））∈，则A，v），（A，v））∈ φ.无无无无无无无b是由变量集上的随机注释所诱导的最小等式关系such，即（Ai，v）∈（Bj，v′），如果[A=B，i=jvA]∈Var/Vars规则定义在变量Var的集合上。另一方面，反应混合物在变量Varn的集合上定义。通过主体识别的概念将规则应用于反应混合物形式化。定义2.6（代理标识）代理标识函数Var Varn为每个代理的变量分配一个标识版本，以这种方式，一个代理的站点变量映射到该代理的相同标识版本：我我p∈ P在变量集Var上，与变量改名L（s）满足lhs规则，如果对于某个识别函数ν，它成立，通过使用变量ν（v A）= v1∈ Var n来识别。 在特工身份确认后，由y定义，v（uv（A，B））=uv（2，4）∈Varn. 命题p′=<$uA<$vA例如p[v] =<$u3<$v5是不可能的。如果在一些试剂识别之后，反应混合物的解释函数满足规则的lhs，则在规则应用之后，相应地更新反应混合物T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105113Varn}，站L，也称为M站R，定义为●={}（→ {}），E，n，R），分配给interpre-L中的规则集合R的ILTSM =（S，L，a），等于k，即a（s，（R，v），s）=k，当且仅当：● 对于任意两个状态s，s′∈S，规则R=（p，q，k），和识别函数∈R∶<$y→y（k）22AA：<$→（）11A A即n（A）=2，对于规则R有两个不同的代理标识：1（R，A<$A）∶<$x1→x（R，A<$A）∶<$x1（）下→x与规则集相关的v个变量的值是Var={x，y}。因为没有任何规则规定你必须这样做={{}{}}AA A AA/S{A1，A2}n，且E={}。对于n（A）=2，CTMC是Var= {x，y，x，y}。 因此，解释ILTS的状态s∈S(i)L（s′）∈φp[/ν]），即状态s′满足规则的lhs，x，y};节点集由V = {（A，{x，y}，{}）}和边E = {}给出。集合一一一一ML=（S，L，a）分配给规则集R使得L（s）∈（{x1，y1，x2，y2} →{0， 1}）{ 0， 1}4. 例如，状态s，其中L（s）=（0， 0， 0， 0），表示变量x和y，随机片段为Varx，y。n1 1 22以便满足规则的RHS。转换由伴随着识别函数的规则的名称来标记。定义2.7（基于规则的系统的逻辑TS）状态空间S1，S2，.. . 变量n0，1，● 标号集L= {（R，ν）-ruleR=（p，q，k）∈R和标识ν∶Varp→ν∶Var→Varn，通过标号（R，ν）从s态跃迁到s态(ii) L（s）∈ <$q[/v]），即 国家满足规则的rhs，并且(iii) 如果没有变量被标识到站点v Varn，则其值在规则应用后保持定义的ILTS具有与定义连续时间马尔可夫链上的随机化学动力学的标准方式一致的动力学[11]，[1]，[8]。例2.8考虑下面的一组规则：R x x kR1−∶xA→<$xA（k1−）R2−∶yA→ <$yA（k2−）.其中R∶p→q（k）表示规则R=（p，q，k）。 如果有两个代理A的副本，1 1 1AA2 2 2AAk1，以及（k1）。S=T{他的连通图是一个网站图（V，E）与年龄nt名称A={A}和网站名称当n（A）=2时，反应混合映射是一个位置图（Vn，En），其中Vn=一一一一混合，其中所有位置值均设置为0。 ILTS的一部分，模型基于规则的系统的这个例子是显示在图.2d.114T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105R∶<$c，<$b，<$cb→c，b，cb（k）22BCBC（B，C）（B，C）B，c），（C，b））}。∶→（）（A，B）（A，B）对于n（A）=1，n（B）=2和n（C）=1，已识别代理的集合为A =名称S = {b，a，c};节点集合为V = {（A，{}，{b}），（B，{}，{a，c}），（C，{}，{b}）}，M=（S，L，a）赋给规则集R是L中的一个函数{（A1，{121b}，{}），（B，{}，{a，c}），（B，{}，{a，c}），（C，{}，{b}）}。该组相关联的L（）=（）一BB（A、B）（A、B）BBCC（B、C）（B、C）例2.9考虑下面的一组规则：R1bA，aB，ba bA，aB，ba k1R1−∶bA，aB，ba（A，B）→<$bA，<$aB，<$ba（A，B）（k1−）R2−∶cB，bC，cb（B，C）→ <$cB，<$bC，<$c b（B，C）（k2−）.联系地图是具有代理名称A ={A，B，C}和站点的站点图（V，E）（a）和边集合E是集合{（（A，b），（B，a））的对称闭包，{A1，B1，B2，C1}，反应混合物图是一个位置图（Vn，En），其中Vn=variables是Var={bA，aB，ab（A，B），cB，bC，bc（B，C）}。ILTS的状态s∈S的解释L（s）∈（{b1，a1，a2，ab1，1，ab1，2，c1，c2，b1，b2，bc1，1，公元前2，1} → {0，1}）。例如，状态s，使得s1， 1， 0， 1， 0， 1， 1， 0编码具有一个试剂A1，B1和C1之间的复合物和一个游离的B2试剂的混合物。统计碎片为Var/s={{bA，aB，ab（A，B）}，{cB，bC，bc（B，C）}}。a）、联络图b）、注释接触图c）、d）、A（x，y）A（x，y）1（1，0）2（0，0）A1A2A（x，y）1（0，0）2（1，0）xAy（R，A›→1A）1（R，A›→21A）...（R，A›→12A）A1A2（0，0）2（0，0）1X 一yT. 彼得罗夫等人理论计算机科学电子笔记284（2012）105115的1（）=A1A2A（x，y）X yXA2Y反应混合物图ILTS...图二.实施例2.8的图示：a）接触图（CM），b）注释接触图（ACM），c）反应混合物图，对于n A 2，d）分配给基于规则的 系统的ILTS的一部分。1（0，1）2（0，116T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105B=（VER）L（）（）Ll=（R，ν）（R，ν）=l.1122l（）=（）=（）=定义3.2设{σ∈ （{1，. n（A）} 一{1，. n（A）}}是每-AA∈A的族L×L当且仅当它们是通过识别相同规则的代理人而创建的：给定【详细】1、... n（A）} → {1，. n（A）}}，使得A∈As∈ps，如果在其标识符上存在一族置换：{σA∈国家与地区.Φσ：Varn→Varn：设等价关系pS×S是p的传递闭包.物种-Lp和集总标签，a）、c）、联络图b）、注释接触图图三.实施例2.9的说明：a）接触图（CM），b）注释的接触图（ACM），c）反应混合物图，对于n A1，nB2，n C 1。3从模型分解到随机碎片设M是基于规则的系统的ILTS，n，.我们介绍了M的两个有效抽象：（i）基于物种的抽象，这是经典化学动力学中的标准观察水平，以及（ii）基于片段的抽象，具体到基于规则的模型，首先在[9，8]中介绍这两种抽象都是由以下标签的集中引起的定义3.1（集总标签）两个标签l1，l2∈L通过关系式l一个规则R∈R，两个识别函数ν1，ν2：Var→Varn，它认为，基于物种的抽象是通过集中状态来完成的，这些状态是等价的直到对代理标识符的置换。例如，如果一个州有一个代理人，一个代理A的接口是0，0，一个代理A的接口是1， 1，哪个接口属于代理A1，哪个属于代理A2（例如，请参见状态s1和s2 在图4中）。集合上的突变1、... n A、代理人A的身份证每个这样的置换族在变量Varn的集合上诱导另一个置换，（σA（i））一如果w=viΦσw）=φσA（i），σB（j）一i、j如果w=uv（A，B），则为uv（A，B）。定义3.3（基于物种的抽象）状态s和s'是集中的，即（）在对任意u∈Var n，L（s）（u）= L（s′）（Φ σ（u））成立.基于抽象Mp=（Sp，Lp，ap）是由集总引起的ML的抽象pL一BBBCB1的1BBC1B2一BBBCT. 彼得罗夫等人理论计算机科学电子笔记284（2012）105117由关系式α集总。F去吧。 在例2.8中，有两个片段：Var={{x}，{y}}。A状态A/A定义3.4（Fragments-basedabstraction）设（V，E） 是一个城市的交通图接口（0， 0）的代理A和接口（1， 1）的代理A（图中的状态s）3）、1{σ2}l，.， {σ}，使得对于i= 1，2，.，l，A∈AA∈A我F规则R从集总状态[s2]→p到状态s2的应用集，对任意u∈Var n，L（′s）（u）= L（s）（Φ（u））成立.2σ2从集总状态[s]到状态s的规则R的应用集合。由Dfn。3.3、2、3、4、5、6、7、8、9、10、11、12、13、14、15、16、17、18、19、设s∈[s]是满足a（s，（R，ν），s） =k的状态，即应用n1 1<$12p则L（s）（v）= L（s）（v）。12′∶→∈<${（）<$ ∈}′对任意u∈Varn，L（s1）（u）=L（s′1）（Φσ（u））成立.现在我们已经有了一个很好的开端。 Tketw o表示s，s′∈S，并假设s∈ps′.基于规则的系统B =（V，E，n，R），带有随机注释，其中，即s∈fs，如果在其定义元上存在l个p突变族，{σ1}A∈A，设等价关系<$f<$S×S是<$f的一个过渡闭包. 碎片-的状态和标签，p和规则R规则R=（p，q，k）可以通过代理识别函数在状态s1上完成L设s′1为uchatL（s′1）∈p[v′]）和所有v′不能定义的变量Fp：pF.它可以应用于某些状态，S1p.在基于片段的抽象中，如果我们可以置换代理的标识符，则两个状态被集中，使得它们的接口的部分（片段）匹配站点1 2以及接口（0， 1）的代理A1和接口（1， 0）的代理A2（图3中的状态s3第三章随机片段的Var/Vcs= {Var1，.，Var l}。 状态s和s是集中的，一A A对任意u ∈ Var n，L（s）（u）= L（s′）（Φσi（u））成立.基于抽象MLf=（Sf，Lf，af）是由集总诱导的ML的抽象F分别。L引理3.5AbstractionsMLpMLfa revalid. Morereover，equivalencer∼ 是粗糙的，比pf证据 我们首先证明抽象Mpp 是有效的。 证明了a_b_l_f1pSS2p，有效性是相似的。考虑两个基于物种的国家[s][][]]/f∈ R[]设s2，s′2 ∈ [s2]<$p. 由Dfn。1.4，它表明，有一个双射之间，存在代理标识符σ A：{1，... n（A）} → {1，. n（A）}，这样Var→Var n. 由Dfn。 2.7，这意味着L（s1）∈<$p[/v]），L（s2）∈<$q[/v]），且所有未被识别的变量保持相同的值：如果vVar nν u瓦尔，设识别函数ν Var Varn是这样的，它首先映射一个站点，u通过函数ν，然后通过函数Φσ置换标识符：ν′（v）= Φ σ（ν（v））.设p是sa值：若v∈Varn<${v′（u）<$u∈Var}，则L（s1′）（v）=L（s′2）（v）.n，′ ′ ′ ′a（s1，（R，v），s2）=k. 此外，s1ps1，因为通过构造函数ν，118T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105然后，DFN。3.3，存在代理标识符σ A∶ {1，. n（A）→T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105119基于类的抽象，即是的。见证点为σ（1） =2， σ（2） =1。我是be-p12证明集总状态的合理性和s的关系。1 3f基于MENT的抽象：S/S。本文给出了两种情况下的最优值σ（1）=2，σ（2）=1和σ（1）=1，σ（2）=213f{x}{x}{y}{y}所以是s。2012年2月2日我LL分配给基于规则的系统B =（V，E，n，R），并且R = R... 最 大的1米IL1LMLI.Vari Var包含出现在规则子集中的变量集因为L（s1）（x1）= L（s2）（x2）（=0），L（s1）（y1）= L（s2）（y2）（=0），L（s1）（x2）= L（s2）（x1）（=1），{σ1} A∈A= {σ2} A∈A=. = {σl}A∈A={σA}A∈AMLf的基于片段的抽象Lfi李iLM1yAS2yA1 .一、 随机注释给出变量类VarSx，y. 物种采取一一一F 与物种的交叉产物同构s1=A（x，y）S2=A（x，y）s3=A（x，y）L（s1）=（0， 0， 1， 1）L（s2）=（1， 1， 0， 0）L（s3）=（0， 1， 1， 0）见图4。三个州s1，s2，s3∈S， 和 他们的 解释。国s1和S2是 集总 在L（s）（2） =LA（）（1）（=）/L={{}{}}A a a a As1和s3在基于物种的抽象中没有被集中，即（s1，s3）pklap，但它们在碎片中被集中{1， .. . n（A）}，则对任意u∈Varn，L（s1）（u）=L（s′1）（Φσ（u））成立.则对所有u∈Varn，L（s）（u）=L（s′）（Φσ1（u）），对i=1， . ，l，and我们现在展示一个对基于片段的抽象的补充观点：它是一个特定的组合运算符的结果，基于适当选择的较小的规则集的基于物种的抽象。更具体地，ILTSM可以表示为较小ILTS的叉积，使得每个小ILTS被分配给规则的子集。要做到这一点，两个选择的规则子集中的每一个都必须是独立的，在这个意义上，它们在相互不相交的网站集上运行。最后，我们表明，基于片段的抽象是一个交叉产品的基于物种的抽象较小的ILTS的。该定理如图5所示。定理3.6（分解ILTS，Prop. 4.2，[14]扩展）设ML为ILTS将规则集划分为较小的规则集，使得规则的每两个子集具有相互不相交的变量集。然后，M可以分解为以下形式：ML=M1L1×... ×MmLm，其中ILTS M i，Li（1 ≤ i ≤ m）是分配给规则集Ri的ILTS。此 外 ，委员会认为，基于所有较小ILTS的我's：MFF Mp×... × M p.引理3.7设ML=（S，L，a），M f=（S f，L f，af），且M p=（Sp，Lp，ap）. 让v i∈ Var是包含在规则子集Ri中的变量。 分割类[v i]s= R我我 我11（0，0）1（1，1）1（0，1）120T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105a）、（R，A›→1A）M1L一12S2一12X（一）b）、1（R，A›→1A）2[（R，A）→1A）]12∼L[（R，A）→1A）]∼L一12X（0）A xA xA xA xS1X（0）S3[s1]p[s2]p[s]′3吨1SMp1L1（R，A›→12A）一12S1y（0）一12y（一）（R，A›→22A）A x1[（R1，A<$→A）]LA x2[（R1，A<$→A）]L一 yA xS2一12y（0）S3[s1]2L2[s2][s3]M2L2s2′MpML=M1L1×M2L2MLf=M1L1×M2L2Fpp规则：R={R，R}，R={R，R}。a）分配给规则集R的nILTSM，和分配给规则集R的nILT SM1 1 211L2L1 2121L12L=pM2L2在DFN。2.5，对于R=（p，q，k），v∈Var，或由于p如果u∈Var且v∈Var，但Var， 其中i=1， . ， l−1。pp pp1i i+1l规则的子集不共享变量。◻，即， u表示如果和o表示它们属于同一规则子集，例如， R. DUES SI因为划分R=R. .假设最大值为1 m，我s∈S，...，s ∈S，其中含有变量s1 1 m m的子集的相应值图五、实施例2的分解方案。8−：规则集R={R1，R1−，R2，R2−}被分成两个较小的集合，从集合Var i，因此Var n=Var n. Varn. 考虑函数Varn，. Var n：对所有v∈Var i，令Li（s i）（v）= L（s）（v）. 然后，因为对于s∈fs′，p突变的第i个见证族{σi}A∈A恰好是L1L第一章（一）1（0）1（一）1（一）第二章（1）2（0）2（0）2（一）第一章（一）1（0）1（一）1（一）第二章（1）2（0）2（0）2（一）分配给规则集R2。b ）基于物种的预测M p;基于人口的投影M p。2定理3.6指出，MfF1L1 ×M p.我是。 回想一下，对于nytw个变量u，v∈Var，它们通过关系传递闭包相关，存在规则序列R1=（p1，q1，k1），.，Rl =（pl，ql，kl），反之，若两个变量u，v∈ Var出现在规则Ri的子集中，则u ∈v，证据（ Thm。3.6）设VarnVar是标识代理的变量集α∶S →S1×…×Sm，取状态s，赋值为L（s），并选择状态1Lsfs′ifandoifs1ps′1，s2ps′2， . . smps′m，T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105121（[ ] ）=（[][]）=（）我普西岛因此，函数αSS1...SMs的证明置换族′∶f→p× ×p一α˜sfs1p，.，smp所以sα s1， . 、sm.是一个定义良好的双射函数。122T. 彼得罗夫等人理论计算机科学电子笔记284（2012）105一AyxyxA规则R∈Ri，并假设对于某个定义函数ν∶Var→Var，−图G的标号为G={（（A，y），（B，x）），（（A，x），（B，y））}。Setofv−ariablesis−A，y），（B，x）），（（A，x），（B，y））}. 带注释的联系人地图是联系人地图R∶<$y，<$x，<$yx→y，x，yx @k，2 BABA（B，A）（B，A）此外，我们证明了状态sf，sf′∈Sf之间的速率等于：<$$><$→（A，B）（A，B）1M仅在ILTSMp，因为来自其他类的规则不与我们有a（s，（R，ν），s）=k。 标签为（R，ν）的跃迁将发生i，因此Varp。？yxK？？？k−K？yx？？？k−见图6。 实施例4.1州际汇率α<$（sf），α<$（sf ′）∈Sp×. ×Sp.Le t[s]，[s′]∈Sf，anRiLi中的变量故（），[（R，ν）]π，[s′]π）=LFai （ （ [s1]bsp ， . ， [si]numerical ， . ， [s1]np ） ， [ （ R ， v ） ]nl ， （ [s1]np， . ，[s′i]puerp， . ，[sl][p]））。◻4案例研究：胶体聚集在下文中，我们举例说明了胶体聚集的简单模型的框架[15]。这种聚集动力学代表了自组装的最简单形式- 在分子细胞生物学中普遍存在的过程。微管组装[10]、肌动蛋白薄膜聚合[19]或朊病毒复制[20]都属于这一类-仅举几例。通过这个案例研究，我们证明了使用基于片段的抽象而不是标准的基于物种的抽象会带来指数级更小的状态空间。例4.1考虑一个含有A型和B型粒子的系统，每个粒子都有两个位置，x和y。当两个复合物相遇时，它们可以在自由位点y和自由位点x之间以速率k5形成键。债券可以以利率k发行。在图形符号中，该模型总结在图中。第六