带钩进程代数：理论计算机科学电子笔记中的模式形成模型

理论计算机科学电子笔记268（2010）31-47www.elsevier.com/locate/entcs模式形成模型的带钩进程代数Andrea Degashte1和Mu Zarey Calder2格拉斯哥大学计算机科学系英国格拉斯哥摘要本文介绍了带钩子的进程代数（PAH）。在PAH中，过程代表不同的抽象层，从生物化学到组织，通过钩子动作的特殊同步确保这些抽象之间的一致性。有一个明确的表示几何空间和代数有一个随机语义的基础上的功能反应率关键词：进程代数，标号迁移系统，模式形成，几何空间1介绍软件和生物化学过程之间似乎存在深刻的类比，导致了几种基于分子作为过程、物种作为过程或途径作为过程的抽象的建模方法[3]。现有的形式主义已被应用于生物系统的建模，如π-演算[17，15]和PEPA [10，2]，而新的形式主义已被开发用于此特定目的，如Beta- Binders [14]，Bio-PEPA [6]，κ-演算[8]，BIOCHAM [4]。注意力也转向了行为的空间方面，有几种方法将空间考虑在内，通常以拓扑位置的形式[5，16]。在这一研究流程之后，我们考虑包含空间几何概念的模型[9]。在这里，我们提出了进程代数与钩子（PAH），一个进程代数，旨在捕捉模式形成的模型的基本特征。我们的方法受到模式形成的数学模型的启发，这些模型源于图灵的早期形态发生工作[18]。图灵支持1电子邮件地址：andrea@dcs.gla.ac.uk2电子邮件：muffy@dcs.gla.ac.uk1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.12.00432A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31假设给定具有相同且均匀分布的细胞的区域，仅由于细胞中存在的分子的不同和局部反应活性而出现不同表型的特征。这些想法启发了新的模型，今天被越来越多的实验证据所验证[12]。此外，图灵还引入了形态发生素这个术语，这是一种特殊的分子，其浓度决定了空间区域的表型。今天，我们知道这种表型通常取决于形态发生素的绝对浓度[11]，在某些情况下取决于相对浓度[13]。遵循这些概念，在PAH中，我们使用过程来表示不同的抽象层这些层通过称为钩子的动作自底向上同步，确保了抽象的一致性此外，一个明确的概念，几何空间是嵌入在代数。其他功能是从Bio-PEPA借来的，如多路同步，功能速率和语法的简约性。在本文中，我们主要集中在多层次方面的PAH，而不是空间方面。最后，使用PAH，我们产生了一个临时标记的过渡系统（临时LTS），我们称之为临时的，以强调它不打算直接使用转换上的标签表示来自每个抽象层的动作，因此需要对它们进行过滤，以选择我们感兴趣的抽象层。最终，我们的目标是使用基于动作的关系，如概率版本互模拟来测试具有不同生物化学的两个系统是否形成相同的模式集。总之，本文的贡献如下：• 以几何位置和抽象层为特征的过程代数的标记转移语义的语法，其中生化层是最低的• 作用于两个抽象层的可扩展活动;• 包括笛卡尔坐标中的空间位置或表示位置之间的平移的动作;• 监听操作符，用于同步不同抽象层的进程;• 实例包括由涉及两个位置的生化反应确定的组织行为的模型• 扩展到随机标记转移系统。本文的组织结构如下。在第2节中，我们通过例子介绍PAH，然后在第3节中介绍正式的语法和语义。在第4节中，我们展示了如何模拟PAH中的生化层，同时给出了使用PAH在第5节中。 最后，我们将在第6节讨论相关工作结论和未来的工作在第7节。感兴趣的读者会发现随机语义在附录A中，其他正式定义在附录B中，函数率形式化的细节在附录C中。A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3133我v我2带钩子的过程代数举例例2.1使用过程作为浓度抽象层，设M v（i = 0，.，3）是表示在空间中的位置v处的形态原M的过程，具有浓度水平i。此外，设Tv和Tv是更高层的进程0 1表示位置v处的组织T的可能状态（表型）。考虑下面并发进程Mv和Tv的图形表示，0 0其中箭头表示流程可以执行的操作：动作a：v和b：v分别表示增加或降低位置v处M浓度的生化反应。 当M的绝对浓度超过阈值时，T的状态发生变化。在这种情况下，动作x：v表示当Mv变成Mv时Tv变成Tv;反之Tv变成Tv0 1 1 2 1 0当Mv变成（通过b：v）Mv时，具有y：v作用。重要的是注意到2 1组织层动作x：v和y：v仅与某些生物化学的实例同步，层动作a：v和b：v。这些实例表示浓度阈值，并由不同的符号a：v[x：v]和b：v[y：v]表示。x：v和y：v被称为钩子，因为它们自底向上地链接不同抽象层上的操作。a：v和x：v实际上是相同的动作，从两个不同的抽象层解释。它们携带不同但互补的信息片段：a：v意味着生化反应Ra：v已经发生，而x：v意味着组织层的变化已经被触发。注意，我们并没有将a：v[x：v]的执行表示为动作名称a：v和x：v的交错。相反，a：v[x：v]生成一个形式Mva：v，x：v[x：v]T M电视，其中载有整个1x：v，y：v0−−−−−−−→2x：v，y：v1发生了什么事的信息。 监听操作符x：v，y：v 组成进程不同的抽象层可以同步集合{x：v，y：v}中的动作。这个操作符不是可交换的：左边的过程位于较低的抽象层。例2.2生物化学和组织之间的关系更为复杂.在这个例子中，当形态发生素A的浓度超过形态发生素B的浓度我们定义一个额外的效用过程Pi来表示A和B的浓度水平之间的差异。A可以降解（dA：v），B可以产生（pB：v），而A和B都可以同步（s：v），从而将B的水平转换为A的水平Pv表示v34A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31nnnMvm+1图1.一、示例4：进程A的传输动作的图形表示。差异A-B，而a：v和b：v动作分别表示使该差异增加2和减少1的事件。的转变的示例是（（AvDBv）Pv）s：v，a：v，x：v[a：v，x：v]不（（AvDBv）P v）电视1s：v2a：v，b：v−1x：v，y：v0−−−−−−−−−−−→2s：v1a：v，b：v1x：v，y：v1并行操作符D 在同一抽象层上组成流程，s：v可以同步集合{s：v}中的操作。例2.3如果一个抽象层触发了多个钩子，结果钩子集可以被多个监听器按顺序捕获，也可以被单个监听器并行捕获。考虑以下过程：给定这些过程，两个可能的过渡示例是（（AvD Bv）Pv）Q vs：v，x：v，y：v[x：v，y：v]（（AvD B v）Pv）Q v和0s：v1x：v0y：v0−−−−−−−−−−−→1s：v0x：v1y：v1（AvD） Bv）R vs：v，x：v，y：v[x：v，y：v]（A vDB v）R v，表示0s：v1x：v，y：v 0−−−−−−−−−−−→1s：v0x：v，y：v 1分别以顺序和并行方式进行钩子同步例2.4在生化层的动作上放置钩子简化了效用过程的构造，在几何空间被认为是位置的网格。 设Ae表示代表一个在位置e处的物质A的浓度水平n。浓度可以迁移到位置e和从位置e迁移，许多不同的迁移作用将具有降低或增加空间中一个位置的浓度的相同效果，如图1中的图表所示。例如，A可以降低浓度水平，到Aen−1，通过形式为t：（e→s），s∈ {b，d，f，h}的输运作用. t是动作名称，e和s是位置。 （e→s）表示从位置e到位置S。在位置s，进程As将同步并变为As。如果我们想表示当在e处从A的级别n传递到n-1时越过了一个阈值，我们可以向四个传输动作添加一个钩子，例如变成t：（e→s）[y：v]。作为对读者的帮助，我们以行动及其组成的术语解释来结束这篇介绍到目前为止，我们一直在使用a：v[x：v]或b：v类型的动作。a、b和x是动作名称，v是位置，并且动作名称和位置的组合，例如b：v，被称为动作。一组动作{a：v，b：s，. . . 我们称之为活动。事实上，进程只能执行A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3135LL′我们称之为可扩展活动，写作A[H]，其中A和H是活动。如果H是空的，则A[H]的简写为A。为了简化符号，我们省略了花括号{和}，如果这不会产生歧义。最后，当我们写a：v[x：v]时，我们指的是由两个活动组成的可扩展活动，都是单例活动，而当我们写b：v时，我们指的是由两个活动组成的可扩展活动，其中第一个活动是单例活动，第二个活动是空的，因此被省略。3带钩子的过程代数通过描述形式化的、可执行的模型以及通过关系对模型进行比较，提供了比传统的离散方程更丰富的建模和分析范例，例如：模拟和互模拟。本文提出了一种新的进程代数PAH。由于篇幅限制，我们在这里集中讨论语法、语义和使用示例虽然我们在这里没有定义关系，但读者应该记住，我们对这个代数的总体动机是比较具有不同基础生物化学的系统语法的显著特征是：可扩展活动，作用于两个抽象层，包括空间位置或位置之间的传输的动作，以及在抽象的不同层同步过程的监听操作符此外，还有标准的操作符，如并行组合，前缀和选择。我们现在正式定义PAH。肺动脉高压。 PAH的语法定义为：S：：=零|LJ[LJJ].C v|S + SP：：= PD P|PC v|C vL：：= 100 |LJLJ：：= a：m|a：m，LJ LJJ：：= 0|a：m m：：= v|（v → v）v：：=（z，z，z）C vS其中：• S∈Ps和P∈Pm分别是序列成分，用于表示生物化学物种或更高抽象层的行为，以及模型成分，表示模型的状态。Ps是序列成分的集合，而Pm是模型成分的集合。 Cv是一个常数，Cv∈Pc<$Pm，其中Pc是常数集。顺序组件和模型组件通常被称为组件或过程，并形成过程集合P=PmPs;• a∈A，A ={a，b，c，. }，是属于A的动作名称;• a：m∈Act，Act ={a：m1，b：m2，c：m3，. }，是属于动作集合Act的动作。一组动作一个动作也被称为一个活动;• m是位置v，用于确定常数或作用在三个笛卡尔坐标（z，z，z）（z∈Z）中的空间位置，或者是运输作用的位置对（v→v）;36A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31A HLA H• nil是死锁进程。L，LJ，LJJ是动作集（L，LJ，LJJ≠Act），LJ是非空集，LJJ是空集或单例集;• LJ [LJJ] ∈Ext，Ext ={A [H] |A，HAct}，是一个可扩展活动，属于扩展活动Ext.给定A[H]∈Ext，A是正则动作的集合，H是钩子的集合。• A[H].Cv是可扩展活动对常数的前缀• S+S是顺序元件之间的选择;PD P是模型组件的协作，在LL;• PCv是模型组件在层之间同步的协作，抽象了L.工艺Cv它可以同步或忽略;是P中动作的监听器，• CvS是一个恒定的定义。顺序分量S捕获常数Cv的连续性。设A[H]∈Ext，若H= H，则A[H]可以写成A。PAH的语义 PAH的语义由临时LTS给出Lu=（Pm，Act，→u），其中Pm是模型分量的集合，Act是动作的集合，→u是一个转移关系，使得→u≠Pm×Ext×Pm. Lu由以下推导规则定义Prefix常数SA[H]v、A[H]∈Ext1−→C2，CvSA[H]vA[H]v11A [H].Cv −−→CvC1 −→C2选择左选择右SA[H]vA[H]v1−−−→C3S2−−−→C3S+SA[H]vA[H]v1 2−→C3S1+S2−→C3合作左合作右PA[H]A[H]1−→P3，A L=P2−−→P4，A L=P1DL[客户端]2−→P3DP2LP1DL[客户端]2−→P1DP4L定期合作钩忽略PA[E]B[F]A[H]1−−−→P3P2−−→P4，A <$B<$L=<$P1−−→P2，H<$L=<$PDPA B[E F]PDPPCvA[H]PCv1L2−→3L41L−−→2L钩同步PA[E]vB[F]v1−→P2C′ −→C′′ 、 B[F]condPCvA B[E F]PCv1L′ −−→2L′′·A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3137′→111222nnn我B[F] cond：给定C vB [F].C v+ B [F].C v+. +B[F].Cv，设B为B，B1，B2，...，Bn，使得Bi∈ E和Bi∈ L（即Bi ∈E ∈ L），并且在B1，B2，...中没有Bj， Bn具有比B i更大的基数，使得BjE L。我们在定义B.1中正式定义了这一点。作为挂钩同步的示例，考虑以下顺序组件，其中省略位置以提高可读性：Ax[a].A Bx[b].B Cx[c].C Q0a.Q1+a，b.Q2+a，b，d.Q3的 过渡 （AD BD C）、Qx，a，b[a，b，c]（AD BD C）、q为x xa，b，c0−−−−−−→x x a，b，c2执行，因为虽然{a} /={x}和{a}|{a，b，c}|{a，b，c}，Q0不能因为{a，b}/={x}，{a，b} ≠ {a，b，c} ≠ {a，b，c}，|{a，b}|>>|{a}|.那么Q0可以变成Q2，因为|{a，b，d}|>>|{a，b}|，我们也有{a，b，d}<${a，b，c}<${a，b，c}。形式良好的PAH模型。我们现在引入额外的定义，这是定义一个良好的PAH模型所必需的定义3.1生物化学物种。物种集合是生物化学物种的集合。每个生化物种S∈Species都与一个或多个常数，即生化过程有关，这些常数代表了S的不同浓度水平定义3.2函数种类和水平。 “species:如果Cv是与生物化学物种无关，物种（Cv）返回。类似地，“水平：Pc → N“是将过程转换到其相应浓度水平的函数。与物种函数类似，如果Cv与生物化学物种无关，则level（Cv）返回定义3.3生化作用。集合BioAct是生物化学作用的集合。定义3.4 PAH模型。如果满足以下条件，则PAH模型形成良好：• 在序贯分量A[H].Cv中，若A含有生化作用a：m，则A={a：m};• 物种一致性，即如果一个常数Cv在执行扩展后变为Cv1 2活性A[H]，则物种（Cv）=物种（Cv）;1 2• 钩子从不包含生化作用;• 抽象的最低层包含生物化学过程，并且模型中的每个物种只有一个过程我们在定义B.2中正式定义了这一点。38A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31−−−→图二.一个临时的标签转换系统（左）被过滤，删除了不在集合{x，y}中的钩子和标签（右）。过滤LTS。LTSLu被称为临时的，因为它不打算直接使用. 给定一个跃迁PA[H] A是一个有着丰富内涵的词，移除钩子并过滤正则操作A的集合。特别是，A包含几个动作，但从不同的抽象层来看，它们可能只是同一个动作。在过滤系统中，根据要考虑的抽象层，只有属于该层的那些动作将被保留在标签上。以下curried函数用于过滤临时LTS：过滤器：2Act−→（2Pm×Ext×Pm−→2Pm×2Act×Pm）给定一组动作T，其中包含与特定抽象层相关的动作，函数filter（T）将每个转换（P，A[H]，Q）替换为转换（P，B，Q），其中B是T和A的交集。 如果这样的交集为空，则B等于{τ}，其中τ是隐藏动作。函数过滤器在定义B.3中正式定义。定义3.5过滤LTS。给定一个临时的LTSLu =（Pm，Act，→u）和一组动作T，过滤的LTSLp =（Pm，Act，→p），其中→p=Pm×2Act×Pm，由（Pm，Act，filter（T）（→u））给出。LTS过滤的示例如图2所示。随机语义学我们的目标是形式化模式形成的模式，其中模式出现由于生化反应和差异。为了提供准确的定量预测，我们开发了一个随机语义PAH的基础上，功能率。这意味着我们可以从任意的动力学定律中推导出LTS跃迁的速率。感兴趣的读者可以在附录A中找到PAH的随机语义。4生物化学的抽象多环芳烃已被设计为模拟生化相互作用定位在空间中，使用的过程作为浓度抽象的水平。每个分子S的浓度被分成N个S级（NS+ 1与0），具有共同的步长或粒度h。S具有最大浓度MS，其中h=MS/NS。给定两个连续的水平n和n+ 1，范围（h·n，h·（n+1）]内的浓度由离散水平n+ 1表示。因此，0不被认为是一个水平，但它代表不存在浓度。A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3139vn我我1110010几何空间以类似网格的方式被划分为相同形状和体积的槽，其中每个槽由位置v=（i，j，k）标识，其中（i，j，k）∈Z3。槽是长方体，边长为Δx、Δy和Δz。给定笛卡尔坐标轴的原点（0，0，0），槽的角的笛卡尔位置由（i·Δx，j· Δy，k· Δz）给出。例如，关于维度x，槽i的边界在位置i·Δx和（i+1）·Δx处。每个物种S都由它所处的槽的位置v来标识，记为S。 的浓度 物种被认为均匀地分布在槽内生化反应可以通过名称a∈A和发生的位置v来识别，或者如果是传递反应，则可以通过位置v→vJ我们用NS+1常数过程形式化了一种物质的浓度SVSv，Sv，...，S v，它们代表Sv浓度的不同水平，0 1NS浓度可简单地由水平（Sv）·h计算。我们使用一个过程来表示物质S可能存在的每个位置的浓度水平。5更详细的例子考虑组织的一部分，被分成两个相邻的槽，分别具有位置v和s。 在这些槽中，可以产生或降解两种物质A和B，A可以变成B，B变成A。此外，A和B可以在两个插槽。例如，为了表示槽v中的分子A，我们使用符号Av。在化学形式中，系统的反应和相应的作用是（i，j∈ {v，s}，i/=j）：反应化学行动反应化学行动R1：→Air1：iR5：Ai→ Bir5：iR2：Ai→r2：iR6：Bi→ Ai建议6：iR3：→Bir3：iR7：Ai→ AjtA：（i→j）R4：Bi→r4：iR8：Bi→ BjtB：（i→j）我们使用过程Mj来表示在位置j处的物种M∈ {A，B}具有浓度水平i ∈ {0，1，2}。在这个例子中，我们想表达一个动作发生在组织层，当A和B都达到第二层时。我们使用一个实用程序过程Pj（j∈ {v，s}，i∈ {0， 1， 2}），它计算有多少A或B处于水平两个在位置j。Pj表示它们中没有一个，Pj表示它们中的一个，Pj表示0j12两者最后，我们用一个过程Ti来表示槽（组织层）的状态在位置j，其可以是不活动的（Tj）或活动的（T j）。 对于i，j∈ {v，s}，i = j，PAH模型给出了以下恒定定义：我 r1：i.Ai+r6：i.Ai+tA：（j→i）.AiA我r1：i[p：i].Ai+r 6：i[p：i].Ai+r2：i. Ai+r5：i. Ai+tA：（j→i）[p：i].Ai+1 2tA：（i→j）.Ai2 0 0 2一40A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3111100121101201120图3.第三章。过程的图形表示ir2：i[q：i].Ai+r5：i[q：i].Ai+tA：（i→j）[q：i].AiBir3：i.Bi+r5：i.Bi+tB：（j→i）.Bi0 1B我r3：i[p：i].Bi1 1+r 5：i[p：i].Bi+r4：i.Bi+r6：i.Bi+tB：（j→i）[p：i].Bi+1 2tB：（i→j）.Bi2 0 0 2Bir4：i[q：i].Bi+r6：i[q：i].Bi+tB：（i→j）[q：i].Bi2皮皮：皮皮1 1 1Piq：i[y：i].PiPiq：i.Pi+q：i，p：i[X].Pi+p：i[X：i].PvTix：i.TiTiy：i.Ti模型的初始状态由以下模型组件给出（AvDB v）Pv）Tv）D0r5：v，r6：v0p：v，q：v0x：v，y：v0tA：（i→j），tB：（i→j）（（（AsDB s）P s）T s）0r5：s，r6：s0p：s，q：s0x：s，y：s0一A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3141这些过程的图示如图3所示。在这个例子中，我们可以看到钩子是如何被放置在浓度阈值上的，将由分子A和B形成的生化层与更高的层联系起来。较高层42A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31我我可以具有生物学意义，例如代表组织表型的突起Tj可替代地，它们可以是帮助将其他层粘合在一起的中间层，诸如工艺Pj。6相关工作正如我们已经提到的，这项工作与其他进程代数PEPA[10]和Bio-PEPA [6]。实现钩子同步的另一种方法可能是在PEPA中使用动作的优先级。生化动作的优先级最低，而优先级较高的动作可以用来保持更高层次与生化一致。这种方法有两个缺点。首先，具有高优先级的动作将与生化动作或具有甚至更高优先级的动作交织，从而产生额外的中间状态，这些额外的中间状态可以使用钩同步先验地避免。第二，移除这些额外的状态将导致移除除生化行为之外的所有行为。尽管表示更高抽象层的过程是一致的，但我们将失去在模型之间执行基于动作的相等性检查的能力，关于所选择的抽象层在进程代数模型中使用进程来“监听”动作的概念首先在此设置中，进程（探测器）使用正则表达式构造，并用于查询模型。特殊的开始和停止标签被添加到某些操作中，以指示满足查询的进入和离开状态。虽然存在类比，但我们的方法并不旨在查询系统，而是形式化和形式化我们可以从不同的抽象层观察其行为的方式。此外，在某些情况下，正则表达式可能不够强大，无法构建我们需要监听生化作用的过程。7结论和今后的工作一种新的进程代数，PAH，其目的是正式模式形成的模型已经提出。它的主要特点是能够通过自下而上的动作同步来对抽象的不同层进行建模。它还包括几何空间和位置之间的运输的显式表示。在PAH中，最低的抽象层是生物化学，其中过程表示物种的浓度水平更高层的过程表示组织或任何其他抽象层。 在各个层面上，都有明确的位置概念 在几何空间中。语义由一个带标签的转换系统给出，然后过滤以提供一个更简洁的形式，没有钩子，适合给定的抽象层。我们已经通过例子证明了，当浓度阈值被跨越时，或者当两个浓度之间的差异达到阈值时，以及当一组钩子可以顺序或并行地触发行为时，较低层的生化反应如何A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3143在本文中，明确的空间概念的语法有一个有限的功能，如提高模型描述的全面性在PAH的进一步开发中，我们计划在空间改变（如组织生长）的背景下使用该符号。未来的工作还包括定义模型之间的等价关系或其他关系，以便我们可以确定，例如，当两种不同的生物化学导致相同的模式时。确认Andrea Degashte获得格拉斯哥大学的开尔文勋爵/亚当·史密斯奖学金和EPSRC资助的SIGNAL项目的支持。引用[1] Argent-Katwala，A.，J. T. Bradley和N. J. Dingle，使用正则表达式来指定进程代数模型上的随机探针来表达性能要求，第四届软件和性能国际研讨会（2004年），pp.49比58[2] 考 尔 德 ， M. ， S. Gilmore 和 J. Hillston ， 使 用 随 机 过 程 代 数 PEPA 的 影 响 ， 计 算 机 科 学 讲 义 4230（2006），pp.1-23[3]Calder，M.和j.Hillston，生物分子过程的过程代数建模样式，LNCS5750（2009），pp. 1-25[4] 卡尔佐内湖，F. Fages和S. Soliman，Biocham：An environment for modeling biological systems andformalizing experimental knowledge，Bioinformatics22（2006），pp. 1805-1807年。[5] 卡尔代利湖，Brane calculi，Lecture Notes in Bioinformatics3082（2005），pp.257-278.[6] Ciocchetta ， F. 和 J. Hillston ， Bio-PEPA ： 生 物 系 统 建 模 和 分 析 的 框 架 ， 理 论 计 算 机 科 学 410（2009），pp.3065-3084[7] Clark，A.和S.Gilmore，扩展随机探针的状态感知性能分析，LNCS第5261（2008）号来文，第5261（2008）页。125-140[8] 达诺斯，五，J. Feret，W.丰塔纳河Harmer和J. Krivine，细胞信号的基于规则的建模，计算机科学讲义（2007），pp.17比41[9] Degasstrom，A.和M. Calder，关于生物系统梯度扩散模型的形式化，PASTA研讨会2009（2009）。URLhttp://www.dcs.gla.ac.uk/www.example.com~andrea/files/DegasperiCalder_Bio-PASTA2009.pdf[10] Hillston，J.，[11] Meinhardt，H.，裁剪和耦合的反应-微分方程系统，以获得可再现的复杂模式的形成过程中的发展，高等生物，应用数学和计算32（1989年），页。103-135[12] Meinhardt，H.，生物模式形成的模型：从基本步骤到胚胎轴，Curr。Top. Dev. Biol. 81（2008），pp.1比63[13] Meinhardt，H.，梯度的生成和解释模型，冷泉港生物学展望（2009年），pp。1-14号。[14] 普里阿米角和p.Quaglia，用于生物相互作用的β-结合剂，LNCS3082（2005），pp.20-33[15] Priami，C.，A. Regev，E. Shapiro和W.陈晓，随机名字传递演算在分子过程，北京：计算机科学出版社。Lett. 80（2001），pp. 25-31.[16] Regev，A.，E. Panina，W.西尔弗曼湖Cardelli和E. Shapiro，Bioambients：An abstraction for biologicalcompartments，Theoretical Computer Science325（2004），pp.141-16744A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31A BEF1 2[17] Regev，A.，W. Silverman和E. Shapiro，使用pi演算过程代数表示和模拟生化过程，Paci fic Symposiumon Biocomputing（2001），pp. 459-470[18] Turing，A.，形态发生的化学基础，伦敦皇家学会哲学汇刊。Series B，Biological Sciences237（1952），pp.37比72随机语义为了定义PAH的随机版本，我们需要将速率与临时LTS的每次转换相关联。速率是一个正实数，它是一个转变（即一个动作）发生所需时间的指数分布的参数。由于生化反应的速率通常是物种浓度的函数，我们采用函数速率。每一个生化作用a：m∈BioAct都与一个功能速率fa：m相关联。我们定义F为函数率的集合，使得fa：m∈F。如何评价功能性比率的详细信息见附录C。在这里，可以说比率ra：m是从函数比率fa：m∈F计算的，并且环境Γ，它是将变量名与值相关联的函数。我们将其定义为我们现在介绍PAH的随机语义。相对于原始语义，派生规则Prefix、ChoiceLeft和Choice Right不变。以下是修改后的规则：恒定SA[H] CvCvS1如果物种（Cv）∈物种，则1 −−−→2 ，11Cv（A[H]， Γ）CvΓ ={（物种（Cv），水平（Cv）·h）}，否则Γ =1−−−−−→2合作左翼1 1P（A[H]， Γ）1−→P3， A L=PDP（A[H]，Γ）PDP1合作权利L2−→3L2P（A[H]， Γ）2−→P4， A L=PDP（A[H]，Γ）PDP1L定期合作2−→1L4P（A[E]，Γ1）（B[F]， Γ2）1−−→P3P2−→P4， ABL/=P1勾忽略DPL（[]，Γ（Γ）2−−−−−−−−−−−−−−→P3DP4LA. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3145111P（A[H]， Γ）1−→P2， H <$L= HPCv（A[H]，Γ）PCv1L−→2L钩同步P（A[E]，Γ1）v（B[F]， Γ2）v1−−−−−−→P2C1−−−−−→C2 、 B[F]condPCv （A <$B[E <$F]，Γ1<$ Γ2）PCv1L1−−− − −−− − − −→2L2边条件B[F]cond不变。请注意，C v在更高的抽象层上，因此，如果模型是良构的，则species（C v）=且Γ 2=。随机临时LTS被定义为Ls ， u=（ Pm，Act，→s ， u），其中转移关系→s ，u=Pm×Ext×2Species×R×Pm是满足PAH随机语义的最小关系随机临时LTS的过滤用于选择动作 在标签上相对于感兴趣的抽象层，并计算转换的速率。与非随机情况类似，我们使用以下curried函数：过滤器S：2C×R−→（2Act−→（2Pm×Ext×2S物种×R×Pm−→2Pm×2Act×R×Pm））给定一个环境ΓC×R和一组动作T，其中包含与特定抽象层相关的动作，函数滤波器s（Γ）（T）用一个转换（P，B，r，Q）替换每个转换（P，A[H]， ΓJ，Q），其中B是T和A的集合交集，r是转换的速率。假设一个形式良好的PAH模型，A只包含一个生化作用a：m，与相关的功能速率fa：m。 速率r由fa：m和环境Γ和ΓJ的并集计算。如在非随机情况下，如果T和A的交集为空，则B等于{τ}。函数滤波器s在定义B.4中正式定义。定义A.1随机过滤LTS。给定一个随机临时LTSLs，u =（Pm，Act，→s，u），一个环境Γ<$C×R和一组动作T <$Act，对应的随机滤波LTSLs，p =（Pm，Act，→s，p），其中→s，p<$Pm×2Act×R×Pm，由（Pm，Act，filters（Γ）（T）（→s，u））给出.B正式定义定义B.1B[F]cond. 在推导规则“钩子同步”中形式上定义为B[F]condbyy：BELi>|B|Φi（C v）（E<$L）=φ，其中|B|是B和Φk的基数定义为：Φ k（A [H].C v）= λX. {A [H]} 如果|一|= kA XΦ k（S1 + S2）= λX. （Φk（S1）（X）<$Φk（S2）（X））Φ k（nil）= λX。ø定义B.2良好形成的PAH模型。如果满足以下条件，则PAH模型形成良好：• 当定义顺序组件时，包含生物的常规动作集46A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31−−−−→−−−→χ∪ ∪ ∪ ∩∪L∩--⊆11化学作用只能是单态的，即给定 A [H].C v， 如果 a：m ∈BioAct s.t. a：m ∈ A则A ={a：m};• 物种一致性，即如果Cv/=nil，则（Cv）=物种（Cv），其中定义为：（A[H].Cv）={物种（Cv）}，（S1+S2）=• hooks从不包含生化作用，即给定A[H].Cv则HBioAct= H，• 生物化学过程，而不是仅仅是生物化学作用，即如果物种（Cv）∈物种和a：m [H].C va：m [H] C v则a：m ∈BioAct。 此外，如果物种（Cv）=0，A[H].C vA[H] C v则ABioAct =。• 抽象的最低层包含生物化学过程，模型中每个物种只有一个过程，即χ（P）=（A，B，C）和A物种，B= λ和C物种= λ，其中χ定义为：（2）C =（ 种（Cv） ，，），χ（P1DP2）=（AX、BY（A）X）、CZ），其中X（P1）=（A，B，C），并且L（P2）=（X，Y，Z），χ（PC v）=（A，B，{species（C v）}<$C），其中x（P）=（A，B，C）。定义B.3滤波器功能。滤波器：2Act−→（2Pm×Ext×Pm−→2Pm×2Act×Pm）=λY。（λX. （过滤器实验室（Y）（α）|α∈X}）过滤器实验室：2 Act−→（P m× Ext × P m−→ Pm× 2 Act× P m）=λY。（λX. （（P，filterset（Y）（A），Q），其中X=（P，A[H]，Q）滤波器组：2Act−→（2Act−→ 2Act）=λY。（λX. （如果A = π，则τ else A，其中A ={a：m|a：m∈X<$Y}））定义B.4过滤器的功能。给定（P，A[H]， Γ，Q）∈→s，u，我们知道A ∈BioAct={a：m}。这是因为，如果一个PAH模型是良好形成的，那么每个转变都只有一个生化作用。我们在以下curried函数中使用此观察结果，定义为产生随机滤波LTS。过滤器S：2C×R−→（2Act−→（2Pm×Ext×2S物种×R×Pm−→2Pm×2Act×R×Pm））=λZ。（λY. （λX. （{过滤器s，实验室（Z）（Y）（α））|α∈X}）过滤器，实验室：2C×R−→（2Act−→（Pm×Ext×2Species×R×Pm−→Pm×2Act×R×Pm））=A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）3147⎜ ⎜⎜⎜⎛⎛⎜滤波器（P，filterset（Y）（A），eval（fa：m，ΓZ），Q），滤波器滤波器λZ。 λY。 λX。⎝ ⎝⎝其中X=（P，A[H]， Γ，Q），并且{a：m}=A βBioAct⎟⎠⎟⎠⎟⎠函数48A. 德加斯托湾Calder/Electronic Notes in Theoretical Computer Science 268（2010）31δt我δtΔtΔtC功能费率每个生化反应都与速度相关，也称为动力学定律，其确定每时间单位（例如秒）由反应转化的浓度（例如摩尔）的量。可以使用与a：m相关联的反应速度来导出速率ra：m。首先，速度被形式化为一个功能率。第二，当需要时，基于特定状态下的物质在CTMC水平模型中推导利率。给定动作a：m，与a：m相关联的生化反应的速度v，Si（i = 1，.，n）反应中涉及的物质，[Si]表示Si的浓度，Si表示Si的当前浓度水平，ki ∈Z表示它们在反应中的化学计量，h为步长，[Si]的时间变化由下式给出：δ[