理论计算机科学电子笔记180（2007）65-79www.elsevier.com/locate/entcsBioAmbients1的控制流分析弗莱明·尼尔森和汉娜·里斯·尼尔森2丹麦技术大学Corrado Priami和Debora Rosa3特伦托大学摘要本文提出了一种静态分析，用于研究BioAmbients中指定的生物系统的特性。我们利用控制流分析来解码通信引起的变量的绑定，并建立一个可以相互作用的环境的关系。 我们最终将我们的分析一个正反馈基因调控的例子。保留字：控制流分析，BioAmbients，基因调控1介绍和动机生物系统的建模是计算机科学的一个挑战[27]。事实上，这些系统的复杂性比有史以来建造的计算机系统要大一些。此外，生物系统的动力学行为建模正成为生物学家的迫切需要，他们正试图连贯地组织后基因组时代的大量数据。本文是朝着生物学家建模环境的定义迈出的一步，可以帮助他们定义和分析复杂系统。基于进程代数的有前途的方法允许建模和仿真 分子系统的动力学行为。用微积分对生化系统建模的开创性工作是[10]，其中使用了λ-微积分的一个版本。[28]通过微积分提出了一种更好的途径描述1本研究部分由欧盟资助的DEGAS项目（编号IST-2001-32072）和丹麦自然科学研究委员会资助的LoST项目（编号21-02-0507）资助。2电子邮件：nielson@imm.dtu.dk，riis@imm.dtu.dk3电邮地址：priami@dit.unitn.it，schuch@dit.unitn.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.01.04166F. Nielson等人理论计算机科学电子笔记180（2007）65对于移动性，其中进程代表化合物，通信代表交互。然后，[24]用定量方面丰富了这个模型。沿着同样的路线，我们也提到了[16]中提出的生物演算。最近在[7]中提出了称为核心形式分子生物学的过程代数。新的演算建立在π演算的基本原语之上。与上面提到的其他基于语言的模型一样，过程表示复合，过程集表示解决方案，它们的行为由一组重写规则给出，适当的附加条件。所提出的规则与生物领域有关，并模仿生化网络中发生的典型反应，例如。G. 最近，Regev提出了BioAmbients[25]，这是Ambient Calculus [6]的变体，其中隔室被描述为层次结构边界环境。这种层次结构可以通过具有直接生物学解释的适当操作来修改。例如，enter原语将一个环境移动到一个（同级）环境中，它对一个隔间条目进行建模。环境中含有通过通信相互作用的化合物。只有当所涉及的进程遵守某些约束时，通信才是可能的。 G. 它们或者在同一隔间中（本地通信），或者它们属于两个并行隔间（兄弟通信），或者它们属于一个在另一个内的两个环境（父子通信）。BioAmbients的原始介绍已在[26，5]中进行了细化。所有上述工作描述的行为的分子系统依赖于一个过渡系统的表示，可以探索调查的利益性质。这种方法的主要限制是表示的巨大尺寸。 事实上，过渡系统的大小是指数级的，代表行为的程序的一部分。换句话说，上述所有建议都实现了系统的动态分析。当表示的尺寸太大时，动态分析的经典替代方案是静态分析[17]。它只需要程序的文本，就可以推断出所建模系统的行为的适当属性。该技术更加有效，但必须在检查的属性的精度方面付出损失。从历史上看，静态分析技术是在优化编译器的背景下发展起来的，只是在过去的几年里，它们才成功地用于验证进程演算中的程序。在经典的应用领域中，通常完整的程序可用于分析，因此技术集中在封闭程序上。以前的工作表明，静态分析方法可以处理各种各样的必要的构造包括移动性和通信原语，如π演算[3]，移动环境[20，18]和盒装环境[20]。我们在这里介绍一种静态方法，用于分析BioAmbients中指定的分子过程。据我们所知，这是在生物应用领域利用静态分析的第一次尝试。 分析的目的是跟踪环境的内容以及在通信发生时可能变化的名称的绑定。 在BioAmbients中，环境是无名的，为了讨论环境的内容，我们需要一种引用它的方式;因此，我们将注释程序，以便我们可以区分各种环境。F. Nielson等人理论计算机科学电子笔记180（2007）6567环境语的句法出现。使用这些信息，我们建立两个关系描述绑定的名称和环境的内容在扫描规范和分析可能改变名称绑定的潜在通信以及可能改变环境内容的能力的潜在执行时，更新关系我们通过在BioAmbients中建模来展示分析是如何工作的，这个例子已经在[24]中发表并在π演算中指定在生物学背景下利用我们的分析结果是立即的。例如，我们可以使用我们的分析来确定两个环境是否例如，在一个实施例中，蛋白质与降解因子或与另一种蛋白质）或是否存在从一个分子到另一个分子的信息流由于分析约束的求解器的效率，我们能够处理比动态分析更大的分子网络，尽管我们的方法仅表明潜在的相互作用。这可能是分析复杂途径的一个突破：我们可以建立描述生物系统动态行为的模型，并且使用我们的分析技术，我们可以（1）通过验证模型与公共数据库中已经记录的属性的关系来信任模型，以及（2）通过建立公共数据库中可用表示中不直接相关的元素之间的关系来提供进一步的生物学见解。例如，在一个实施例中，[ 12]、EcoCyc[12 ]、WIT [30]、KEGG [22]、CSNDB [11]、aMAZE [31]、GeNet[13]、Transfac [32]、INTERACT [9]、DIP [33]、BIND [2]、SPAD [1]和Flynets [29]）。本文的结构如下。在下一节中，我们将回顾BioAmbients的基础知识。第3节介绍了分析技术，第4节然后将其应用于文献中的一个例子我们最终得出了一些结论。2生物环境BioAmbients [25，26，5]在两个主要方面与Mobile Ambients [6]不同• 环境是无名的实体，尽管它们的角色可以通过注释来指示。为了区分环境语的各种句法出现，我们将像[P]μ中那样注释环境语，我们将说μ是恒等式。环境[P]。• 这些能力基于没有内部结构的纯名称n。反应是同步的，客体和主体必须在反应上达成一致以使其发生;后者是通过使成对的能力相互反应来实现的。此外，流程的控制结构集比 传统上是为移动环境研究的，因为它包括非确定性选择以及CCS方式的一般递归构造[15]。 进程P和能力M的语法在表1中给出。 这一举动- BioAmbients的移动能力是基于主体和客体的，主体和客体包含具有相同名称的能力;这与Mobile Ambients不同，Mobile Ambients的移动能力是基于身份（称为环境名称）的，实际68F. Nielson等人理论计算机科学电子笔记180（2007）65p►►P►►ppppppWFWFWFwf wfPWFPWFWFWFWFP：：=0非活动进程|（n）名称n的P绑定框|[P]μambientPwith identity μ| M.Pprefixing with capability M|P|P J并行过程|P+PJ非确定性选择|recX. P递归过程（X=P）|X过程变量M：：=输入n|接受，进入|出口;出口|排出运动|合并+n|合并- n合并运动|你好！{m}|n？{p}本地通信|你好！{m}|嗯？{p}儿童沟通|不！{m}|n？{p}家长沟通|n#！{m}|n#？{p}兄弟姐妹之间的交流表1BioAmbients公司► s0► wfPs s swf wf wfSwfsX世界粮食计划署WFM.Ps（n）PsP+PJsrec X. PWF► SPPPpPJP► wfP►WF (n) P► WF表2P|P Jp► WFS[P]μ格式良好的谓词：wfP和wfP。更接近于沟通的治疗。忽略这种差异，进入/接受和退出/排出能力类似于移动环境及其变体安全环境[14]和自由环境[20]的进入/进入和离开/离开能力。没有类似的open/open功能，而是有一个merge+/mergeBioAmbients的通信原语与Mobile Ambients的通信原语有些不同，因为它们使用名称作为通道，并且只有名称可以作为通信的结果进行交换。与移动环境一样，如果两个进程在同一环境中并行运行，则它们可以进行通信;这称为本地通信。 但是，两个进程也可以通信 如果它们属于兄弟姐妹的环境。当一个环境是另一个环境的子环境时，还可能发生另一种通信：子环境中的进程 可以与父环境中的进程通信。 与Boxed Ambients一样 [4]，这实际上产生了两种沟通，这取决于信息是从孩子向父母传播，还是从父母向孩子传播。与π演算[15]相比，通道的名称以局部化的方式使用。 语法受格式良好性条件的约束，该条件确保顶级流程具有没有自由的过程变量，它基本上是一个数字的并行组合 每个过程都是过程的总和。后一个条件是形式化的由谓语动词P在表2中定义;它使用辅助谓词SP保持在有保护过程的和上。格式良好的条件是►►►p►PJF. Nielson等人理论计算机科学电子笔记180（2007）6569→≡→WFWF绑定名和绑定变量的α-重命名（n）P（m）P[m/n]n？{p}.P你是谁？{q}.P[ q/p]n？{p}.P你是谁？{q}.P[q/p]嗯？{p}.P你好吗？{q}.P[ q/p]n #？{p}.P你是谁？{q}.P[ q/p]recX. P. P [Y/X]ifm∈/fn（P）ifq∈/fn（P）ifq∈/fn（P）ifq∈/fn（P）ifq∈/fn（P）ifY∈/fv（P）并行过程的重新排序：求和过程的重新排序：P|P J P J|P（P|PJ）|PJJP|（PJ|PJJ）P| 0元名称绑定的作用域规则：（n）0（n1）（n2）P（n2）（n1）PP+PJPJ+P（P+PJ）+PJJ<$P+（PJ+PJJ）P+0 P（n）（P|PJ）（（n）P）|PJifn∈/f n（PJ）（n）（[P]μ）[（n）P]μ表3结构同余关系：P<$PJ。环境的移动[（entern. P+PJ）|P[J] μ1|接受;接受;接受Q+QJ）|QJJ] μ2→ [ [P| P[J] μ1|Q|Q[J] μ2出口，出口，出口 P + P J）|P[J]μ1|驱逐，开除 Q + QJ）|QJJ]μ2 → [P |P[J]μ1 |[Q |Q[J]μ2[（merge+n. P+PJ）|P [J]μ1| [（merge- n. Q+QJ）|QJJ]μ2→ [P|PJJ|Q|QJJ]μ1环境之间的沟通（n！{m}.P+PJ）|（n？{p}.Q+QJ）→P|Q[m/p]（n！{m}.P+PJ）|[（n？{p}.Q+QJ）|QJJ]μ→P|[Q[m/p]|QJJ]μ[（n！{m}.P+PJ）|P[J]μ|（n？{p}.Q+QJ）→[P|P[J]μ|Q[m/p][（n#！{m}.P+PJ）|P [J]μ1| [（n#？{p}.Q+QJ）|QJJ]μ2→[P| P [J]μ1|[Q[m/p]|Q[J]μ2在上下文中执行：P →Q（n）P →（n）QP→Q[P]μ→[Q]μP→QP|R→Q|RP[rec] X. P/X]→Qrec X. P →QP<$PjPJ→QJQJ<$Q P →Q表4跃迁关系：P→PJ。比[26]中提出的和和前缀的语法规则更自由一些。语义给出了在经典的方式使用的同余关系和过渡关系。全等关系在表3中定义;这里我们分别写fn（P）。fn（M），对于P中的自由名集合，分别为M，我们把过程P[m/n]写成P，除了n的所有自由出现都被m代替（服从于绑定名的α-重命名类似的符号用于自由过程变量fv（P）和自由过程变量的替换P[Y/X]。转换关系在表4中定义。以下结果表明，转换关系（直到结构同余）保持了良构性：命题2.1如果P→P且P→Q，则存在QJ，使得P→P且QJQ。Q70F. Nielson等人理论计算机科学电子笔记180（2007）65[]IR[][2014-05-23]∈I∈I∈R3分析分析的目的是跟踪环境的内容和名称的绑定;它相当于[20]中提出的想法的改编。我们将通过过程的句法注释所指定的身份来指代环境。在例子中，我们将小心地引入唯一的身份，但这对我们的方法来说并不重要：如果两个句法上不同的环境得到相同的身份，这只意味着分析将无法区分它们，因此将不会像它可能的那样精确。在这里开发的相当简单的分析中，我们将为环境恒等式的集合编写环境，并假设它是有限的。由于这些名称会被α重命名，因此它们不能用于在分析中携带信息。规避这个问题的通常方法是假设每个名字n都有一个写为n的规范名，然后假设规范名在α-重命名下被保留，即。e. n=m。resp. p=q，对于表3的α-重命名子句成立。 我们将把规范名的集合写成Name，并再次假设它是有限的。规范功能是使用规范名称而不是名称的功能;我们为这些功能编写Cap分析将跟踪以下信息：• 环境的内容的近似IAmbient×（Ambient电容）所以，（μ）（代表（μ，u）））意味着μ可以包含u。 环境可以包含其他环境以及能力。这一部分的分析是以运动能力为前提的。• 类似于相关名称绑定：注册名×姓名所以（v）（代表（v，vJ）））意味着ν可以取值νJ。这里，VJ通常是在通信中传输的名称的规范名称。这一部分的分析是由通信能力所决定的。分析的判断具有以下形式：（I，R）|=P并且表示当P被包围在具有标识 * ∈ Ambient的环境中时，则I和R正确地捕获P的行为，这意味着如果Peves in到PJ在n个步骤中，即， e. P→···→ PJ，则N为0（I，R）|=PJ.分析分为两个阶段。 首先我们要确保 描述 初始过程;这是针对表5中的过程和表6中的能力进行的。表5的子句简单地相当于过程的直接结构遍历;每当引入名称时，它必须在R-分量中被反映，如由条件[n∈R（[n∈ R）]表示的，并且当引入任何名称时，F. Nielson等人理论计算机科学电子笔记180（2007）6571I∈IRI R|I R|（I，R）|=s0（I，R）|=s（n）P我的我的真[n <$∈R（[n<$）<$（I，R）|=sP（I，R）|=s[P]μ我的μ∈I（I）<$（I，R）|=μP（I，R）|=sM. P我的（I，R）|=sM（I，R）|=sP（I，R）|=sP|PJ我的（I，R）|=sP（I，R）|=sPJ（I，R）|=sP+PJ我的（I，R）|=sP（I，R）|=sPJ（I，R）|=srecX.P我的（I，R）|=sP（I，R）|=sX我的真表5过程分析：（I，R）|=sP.（I，R）|=senter ni<$$>vn：vn∈R（[n <$]<$entervn∈I（n）（I，R）|=sacceptni<$$>νn：νn∈R（[n <$]）<$acceptνn∈I（<$）（I，R）|=sexitniνn：νn∈R（[n）exitνn∈I（）（I，R）|=sex pelni<$$>νn：νn∈R（[n <$]）<$ex pelνn∈I（n）（I，R）|=smerge+niνn：νn∈R（[n）merge+νn∈I（）（I，R）|=s合并-niνn：νn∈R（[n）merge（I，R）|=sn！{m} i<$$>νn，νm：νn∈R（[n <$]）<$νm∈R（[m <$]）<$νn！{νm} ∈I（π）（I，R）|=sn？{p} i∈N：N∈R（[n <$]）N？{[p<$}∈I（n）（I，R）|=sn！{m} i<$$>νn，νm：νn∈R（[n <$]）<$νm∈R（[m <$]）<$νn！{νm} ∈I（π）（I，R）|=sn？{p}i∈N：N∈R（[n <$]）N∈N？{[p<$}∈I（n）（I，R）|=sn！{m} i<$$>νn，νm：νn∈R（[n <$]）<$νm∈R（[m <$]）<$νn<$！{νm} ∈I（π）（I，R）|=sn？{p} i∈N：N∈R（[n <$]）N？{[p<$}∈I（n）（I，R）|=sn#！{m}i<$$>vn，vm：vn∈R（[n <$]）<$vm∈R（[m<$]）<$vn#！{νm} ∈I（π）（I，R）|=sn#？{p}i∈N：N∈R（[n∈]）N∈N#？{[p<$}∈I（n）表6能力分析：（I，R）|=sM.它必须在-分量中被反映，如μ（*）所表示的-注意，当我们检查环境的内容时，我们确保记录封闭环境是μ，如子句（，）=μP所反映的。对于能力，我们使用表6中定义的判断（，）=M，并在下面解释。并行过程和过程之和的子句是相等的，从而证明了分析的简单性;在递归的分析中遵循相同的趋势为了理解能力的分析，重要的是要注意到，由（n）P引入的名称是常量，而在输入能力中引入的名称（上面称为p）是可以绑定到其他名称的变量（即，e.（1）由于通信。进程的子句已经确保常量代表它们自己;最初， 输入能力的变量的绑定，当我们研究如何模仿过程的动态时，它们将被强加。表6的子句仅仅要求对于在能力中自由出现的名称的每个可能绑定（在上面称为n和m），在分析的I72F. Nielson等人理论计算机科学电子笔记180（2007）65我IRRR关于我们En ter/accept： μ，μ1，μ2，νn：enterνn∈I（μ1）<$μ1∈I（μ）<$accept νn∈I（μ2） <$μ2∈I（μ）μ1∈I（μ2）出口/出口pel：μ，μ1，μ2，νn：exitνn∈I（μ1）μ1∈I（μ2）μ驱逐νn∈I（μ2） <$μ2∈I（μ）μ1∈I（μ）Merge：μ，μ1，μ2，νn：merge+νn∈I（μ1）merge⇒∀μJ:μJ ∈I(μ2)⇒μJ ∈I(μ1)电话：μ，νm，νp，νn：νn！{νm} ∈I（μ）文？{νp} ∈I（μ）n∈R（vp）到时候，我会说：μ，μc，νm，νp，νn：νn！{νm} ∈I（μ）是吗{νp} ∈I（μc）<$μc∈I（μ）n∈R（vp）Toparnt：μ，μc，νm，νp，νn：νn！{νm} ∈I（μc）<$μc∈I（μ）<$文？{νp} ∈I（μ）n∈R（vp）给兄弟姐妹们：μ，μ1，μ2，νm，νp，νn：νn#！{νm} ∈I（μ1）<$μ1∈I（μ）<$文#？{νp}∈ I（μ2）<$μ2∈I（μ）n∈R（vp）表7I和R的关闭条件。最后，我们确保并考虑了工艺的动力学;这是由表7中的封闭条件制定的。前三个条款涉及移动能力和最后四个通信能力。在每种情况下，前提条件都表示语义中可能存在redex，结论则对模仿语义所需的I和R提出了额外的要求。让我们解释一下enter/accept的子句;其他移动功能的子句遵循相同的模式。从表4中可以清楚地看出，为了使转换发生，必须使输入和接受功能是在兄弟环境中，这正是表7的前提条件所表达的：输入νn在μ1内，接受νn在μ2内，μ1和μ2是兄弟环境，因为它们都在μ内。从语义中，我们可以看到，作为转换的结果，具有enter能力的环境将移动在我们的分析中，这是由子句的结论表示的，即μ1在μ2内。关于通信能力的条款，我们将解释本地通信的条款;其他条款遵循相同的总体模式。前提条件表示，νn！ νm和νn？ νp必须与表4中的语义完全相同。通信的结果是在输入功能的延续中执行绑定;这是通过在 （νp）。 的信息是全球性的，因此它在任何地方都可用特别是在输入能力的延续方面分析的语义正确性表示为：定理3.1假设P→ Q，（I，R）|=<$Pandd<$n∈fn（P）：[n <$∈R（[n <$]）. ThenF. Nielson等人理论计算机科学电子笔记180（2007）6573IR[2011年12月21日][2004年12月21日]我（I，R）|=Q。Q这就是说，分析结果描述了对过程的实际行为的过度近似：它考虑了过程的所有实际过渡步骤。然而，由于分析的简单性，还将存在分析信息指示可能发生转变但实际上永远不会发生转变的情况。 定理的证明是通过P→Q上的归纳法，它使用了以下可以通过P<$Q上的归纳法证明的标准引理：Lemma3. 2如果P≠Q，则（I，R）|当且仅当（I，R）|=Q。Q该分析使用简洁求解器[19]实现。该求解器在有限（但不一定有界）的宇宙上工作，并接受ALFP（Alternation-Free Least Fixed Point Logic）中指定为子句的静态分析作为输入，然后计算它们的最小解。实际上，表5、表6和表7中的子句已经用ALFP编写，因此实现非常简单。Succinct Solver是在标准ML中实现的，它利用了许多巧妙的算法和数据结构，不仅可以获得良好的性能，而且可以获得形式上可预测的时间复杂度。与其他解算器相比，简洁解算器针对处理稀疏关系进行了优化，因为我们相信它们经常出现在上下文相关的静态分析中。在上述分析的具体说明中，我们根本没有涉及这些问题，我们的实际实验也没有表明需要这样做;作为一个例子，在分析下一节将要介绍的过程时，求解器将在一个只有89个原子的宇宙上运行，它将构建一个有75个元素的关系和一个有33个元素的关系;这些关系的计算需要不到一秒钟。然而，对于更复杂的示例，重写分析以更好地利用关系的表示可能是值得的为了说明可以做些什么，考虑例如对表6中的能力输入n的分析：对于n的每个可能值νn，它将产生一对（输入νn，*）in另一种规范将只包括（输入n，*），然后检查表7的闭包条件中是否存在redex。4示例：通过正反馈的转录调节我们现在将使用BioAmbients对[24]中指定的相同示例进行建模，依赖于随机π演算的变体[23]。图1所示和表8所示的系统通过正反馈调节基因表达。它包括两个基因（环境基因A和基因TF）、它们的转录mRNA（环境RNAA和RNATF）、相应的翻译蛋白（环境蛋白A和蛋白TF）以及RNA和蛋白质分子的降解这些事件通过与细胞机制的相互作用介导，用于DNA转录（ambientTranscr）、RNA翻译（ambientTransl）以及RNA和蛋白质降解74F. Nielson等人理论计算机科学电子笔记180（2007）65ATF普泰尔乌比乌德蛋白D3GRADATFOKdegp2酶绑定TF巴克布埃degp2酶结合比乌德TF代姆RKAUTRTRAKSLATFOKUTR代姆D3GRADATFOKpATRAKSCRFPTFOKpA图1.一、通过正反馈进行转录调节的图示[24]。（环境RNA 度和蛋白质度）。这些相互作用中的每一种都涉及不同的分子基序（名称为basal、utr、degm和degp）。在生物环境中驱动生物过程编码的主要思想是利用能力将相互作用的分子移动到可以发生通信的位置此外，由于我们模仿了同一系统的π-演算规范，我们通过通信触发功能执行。在Transcr与GeneA和GeneTF之间关于名称basal的两次同级通信之后，并且在由能力exita/exita和exitc/exitc引起的环境的移动之后，环境RNAA和RNATF都处于顶层。现在，翻译机制通过Transl与RNAA和RNATF之间的通 道 utr 上 的 两 个 兄 弟 通 信 将 蛋 白 A 和 蛋 白 TF 移 动 到 顶 层 ， 然 后 是 由 能 力excludeb/exitb和excludee/exite产生的移动。在所得到的配置中，蛋白A通过使用接受tf/输入tf功能接受自身内部的活性TF来结合蛋白TF然后，蛋白质TF通过驱逐环境结合TF变得活跃，具有驱逐atf/退出atf的能力。对于绑定TF，现在有三种选择：(i) 使用通道bb 2上的同胞通信，它首先与蛋白A的激酶同步，然后与通道bb 1上的母体蛋白A同步，最后它排出具有排出f/退出f能力的周围活性TF。现在，通过排出g/出口g的能力，将环境活性TF从蛋白A中排出。然后，主动TF可以与F. Nielson等人理论计算机科学电子笔记180（2007）6575我（a）（b）（c）（d）（e）（f）（g）（bb1）（bb2）（bb3）（basal）（pa）（utr）（degm）（degp）（tf）（atf）（ptail）[rec X1.（基础编号？{x 2}。 开除;开除 X 1+ pa#？{x 1}。 开除;开除 X 1）| [rec X2. A出口。 （utr #？{x 4}。 驱逐湾X 2+ degm#？{x 3}。 0个）| [ exit b. recX3. 接受TF。（bb1！{d}。（驱逐g. X3+ X3）+degp#？{x 6}。bb3！{d}。bb3！{d}。 0+degp#？{x 7}。bb3！{d}。 0个）| [recX4. （bb2#！{d}。X 4+bb3？{x 5}。0）]激酶]蛋白A]RNAA]基因A| [recX5. （基础编号？{y 2}。驱逐C. X 5+页码？{y 1}。驱逐C. X5）| [rec X6. 出口C。 （utr #？{y 4}。 驱逐出境X 6+ degm#？{y 3}。 0个）| [出口E。输入TF。开除ATF 接受ATF。 0| [退出ATF。 （bb1？{y 9}。输入ATF。 0+bb3？{y 8}。0+bb2#？{y 7}。 （bb1？{y 6}。驱逐;开除 0 + bb3？{y 5}。（0））| [f出口] G出口。 第七章. （ptail#！{d}。X7+degp#？{y10}。0）]活性TF]结合TF]蛋白TF]RNATF]基因TF| [recX8. basal#！{d}。 X8+ptail #？{z1}。 pa#！{d}。X8]Transcr| [recX9. utr#！{d}。X9]Transl| [10. history of life degm#！{d}。 X10]RNA度| [rec X11. degp#！{d}。 X 11]蛋白质度表8正反馈转录调控的生物环境表征转录因子Transcr通过通道ptail上的同胞通讯，或降解因子Proteindeg通过通道degp上的同胞通讯。注意，如果蛋白A通过沿着通道degp与蛋白deg的同胞相互作用开始降解，则结合的TF可以在任何时间溶解。(ii) 它可以在通道bb3上与亲本蛋白A通信后溶解，因为蛋白A已经开始了与通道degp上的同级通信的降解步骤。(iii) 它可以在沿着通道bb1从母体通信后再次进入蛋白TF。该系统的质量标准见表8。请注意，为了避免大量使用括号，我们将求和以及并行复合运算符写在第一个被加数的开头。为了帮助分析，我们把约束变量分开α-重命名，并确保环境变量的恒等式是不同的。分析系统的结果如表9所示。该成分的大多数条目说明了该过程的句法结构;系统的动态性导致添加下划线对。 这些条目清楚地证实了上述系统的行为• 对 （ GeneA ， ProteinA ） 、 （ * ， ProteinA ） 、 （ * ， RNAA ） 、 （ GeneTF ，ProteinTF）、（*，ProteinTF）和（*，RNATF）反映环境蛋白A、ProteinTF、RNAA和RNATF向最高水平的移动。• 这对（蛋白A，蛋白TF）见证了蛋白TF进入蛋白A，然后蛋白A内结合的TF的激活被这对的存在所反映76F. Nielson等人理论计算机科学电子笔记180（2007）65我我·····IRI：（蛋白质度，degp#！{d}），（RNAdeg，degm#！{d}），（翻译，utr#！{d}），（Transcr，pa#！{d}），（Transcr，ptail#？{z1}），（Transcr，基础#！{d}），（活动TF，degp#？{y10}），（ActiveTF，ptail#！{d}）、（活动TF，退出g）、（活动TF，退出f）、（绑定TF，活动TF）、（绑定TF，bb 3？{y5}），（BoundTF，excludef），（BoundTF，bb1？{y6}），（绑定TF，bb2#？{y7}），（约束TF，bb 3？{y8}），（绑定TF，驱逐atf），（绑定TF，bb1？{y9}），（绑定TF，退出atf），（ProteinTF，ActiveTF），（ProteinTF，BoundTF），（ProteinTF，acceptatf），（ProteinTF，excludeatf），（ProteinTF，entertf），（ProteinTF，exite），（RNATF，活性TF），（RNATF，结合TF），（RNATF，蛋白TF），（RNATF，degm#？{y3}），（RNATF，excludee），（RNATF，utr#？{y4}），（RNATF，出口c），（基因TF，活性TF），（基因TF，结合TF），（基因TF，蛋白TF），（基因TF，RNATF），（基因TF，pa#？{y 1}）、（基因TF，排除c）、（基因TF，基础#？{y2}），（激酶，bb3激酶？{x5}），（激酶，bb 2#！{d}），（蛋白A，活性TF），（蛋白A，结合TF），（蛋白A，蛋白TF），（蛋白A，激酶），（蛋白质A，bb 3！{d}）、（蛋白A，degp#？{x 7}），（蛋白A，degp#？{x6}），（蛋白质A，排除g），（蛋白质A，bb 1！{d}），（蛋白A，接受tf），（蛋白A，退出b），（RNA A，活性TF），（RNA A，蛋白A），（RNA A，degm#？{x3}），（RNAA，排除b），（RNAA，utr#？{x4}），（RNAA，退出a），（基因A，活性TF），（基因A，蛋白A），（基因A，RNA A），（基因A，pa#？{x1}），（基因A，排除a），（基因A，基础#？{x2}），（α，蛋白A），（β，RNAA），（β，活性TF），（β，结合TF），（β，蛋白TF），（β，RNATF），（α，蛋白deg），（β，RNAdeg），（β，Transl），（β，transr），（β，基因TF），（β，基因A）：（x1，d），（x2，d），（x3，d），（x4，d），（x5，d），（x6，d），（x7，d），（y1，d），（y2，d），（y3，d），（y4，d），（y5，d），（y6，d），（y7，d），（y8，d），（y9，d），（y10，d），（z1，d），（ptail，ptail）、（atf，atf）、（tf，tf）、（degp，degp）、（degm，degm）、（utr，utr）、（pa，pa）、（basal，basal）、（bb3，bb3），（bb2，bb2），（bb1，bb1），（g，g），（f，f），（e，e），（d，d），（c，c），（b，b），（a，a）表9分析结果。（蛋白A，结合TF）。• 活性TF从蛋白A中的排出通过存在对（*，活性TF）来反映。由于分析指定了对环境的精确内容的过度近似，实际上更有趣的是观察不包括在内的信息，因为这确认了什么绝对没有发生。作为一个例子，我们可以看到，周围的激酶根本不移动-只有一对（蛋白质A，激酶） 因此，即使系统中可能有几个蛋白质A的拷贝，它们也保证不会将它们的激酶组分混合在一起;完整的参数包括检查没有（蛋白质A，蛋白质A），（蛋白质A，合并+）或（蛋白质A，合并 -component近似于名称的绑定，由于示例中的所有通信都是同步的，因此我们观察到所有变量最终都可能绑定到虚拟名称d。我们还看到，所有变量最终RF. Nielson等人理论计算机科学电子笔记180（2007）6577都可能绑定到一个值。78F. Nielson等人理论计算机科学电子笔记180（2007）655结论和进一步工作该论文提出了一种新的BioAmbients控制流程分析，这是一种基于Mobile Ambients的演算，专门用于模拟生物系统。我们的计划是首次尝试将静态分析技术应用于分析分子相互作用。我们通过[24]中的案例研究建立了该方法的可行性，其中通过正反馈进行的基因调控在π演算中建模这里介绍的分析是一个非常简单的分析，因为它既不对上下文敏感，也不对数据流敏感。尽管如此，它已被证明对调试我们规范的初步版本非常有用。 事实上，在模拟二聚体时，环境结石和类π结石的基本机制是完全不同的。在BioAmbients中，我们可以简单地决定一个组件进入同一环境中的另一个组件，或者两个环境合并以生成一个新的环境，包括 两个合并的内容。在π演算中，我们通过让二聚体的组成部分通过作用域扩展和随后关闭扩大的作用域来共享新的私有通道来模拟这种情况。这种差异阻止了[24]中规范中的每个π演算过程与相应的环境相匹配，因此不容易检查两个系统的整体行为是等价的。 我们使用我们的分析来检查相互作用的实体是在两个规范中相同，并且由新绑定表示的信息流在两个规范中相同。我们重复了指定系统并分析它的过程多次，然后才达到与π演算规范具有相同行为这个实际的实验表明，静态分析在生物系统的建模阶段是多么重要，当我们必须编写一个规范，以匹配从生物数据中获得的实验知识时。我们目前正在研究一种方法来编码BioAmbients中的生物系统，以促进我们机器的使用。实际上，细胞内发生的生物反应可以被分类，这些生物反应可以被编译成环境宏。那么系统规范就是这些宏的组成此外，生物系统建模的一个主要问题是参数的选择，这些参数在不同的出版物之间，甚至在同一个实验的不同数据库之间都有很大的差异。为了在这个方向上更准确，我们正在努力扩展语义和分析，以考虑随机信息。一种合适的方法可以是依赖于增强的操作语义[8]，其中随机信息由重新标记函数导出，并且它是语义模型的参数[21]。这种关注点的分离应该允许轻松扩展此处提供的分析，并且还应该允许使用不同的定量参数在相同的规格上多次运行分析求解器，从而比较不同的实验。引用[1] 信号通路数据库。 两千F. Nielson等人理论计算机科学电子笔记180（2007）6579[2] G. D.贝德岛唐纳森角沃尔廷湾F.韦莱特，T. Pawson和C. W.霍格生物分子相互作用网络数据库。核酸研究，29（1）：242[3] C. Bodei，P. Degano，F. Nielson和H.里斯·尼尔森π演算的静态分析及其在安全中的应用。信息与计算，168：68[4] M. Bugliesi湾Castagna和S.克拉法盒装的氛围。在计算机科学理论方面（TACS 2001），计算机科学讲义第2215卷，第37Springer，2001年。[5] L.卡德利Bioware语言在计算机系统中-罗杰·李约瑟的论文。2003年。[6] L. Cardelli和A. D.戈登移动环境。软件科学和计算结构的基础（FoSSaCS 1998），计算机科学讲义第1378卷，第140-155页。Springer，1998年。[7] Danos和C. Laneve.核心正规分子生物学。《欧洲方案编制专题讨论会》（ESOP 03），待发表，2003年。[8] P. Degano和C.普拉米增强的操作语义：描述和分析并发系统的工具。ACM计算调查，33，2：135[9] K. Eilbeck，A. Brass， N. Paton ，和C.霍奇曼Interact：一个面向对象的蛋白质相互作用数据库。在Intelligent Systems for Molecular Biology，第7卷，第87-94页，Palo Alto，1999中。Press.[10] W. Fontana和L.W. 巴斯最适合的到来：走向生物组织理论布尔.数学.生物，56：1-64，1994.[11] T. Igarashi和T. 神沼 开发细胞信号网络数据库。 In R. B. 阿尔特曼，A. K. 邓克湖 Hunter和T. E.Klein，editors，Proccedure of the Paci fic Symposium of Biocomputing中国科学出版社.[12] P. D.卡普，M. Krummenacker，S. Paley和J. Wagg. 整合途径/基因组数据库及其在药物发现中的作用Trends in Biotechnology，17（7）：275[13] F. A
我的内容管理
展开
