可在www.sciencedirect.com在线获取理论计算机科学电子笔记293（2013）35-49www.elsevier.com/locate/entcsBioScape：一种细菌-物质相互作用Adriana Compagnonia Vishakha Sharmaa Yifei BaoaMatthew Liberaa Svetlana Sukhishvilia Philippe BidingerbLivio Bioglioc Eduardo Bonellid史蒂文斯理工学院bVERIMAGc托里诺大学Quilmes国立大学摘要我 们设 计 了 BioScape ， 一 种并 发 语 言， 用 于 在 3D 空 间中 的 反 应环 境 中 随机 模 拟 生物 和 生 物材 料 过 程。BioScape是基于随机Pi演算，它的动机是基于个体的，连续的运动，连续的空间模拟建模复杂的细菌-材料相互作用的需要。我们的主要例子是用于抗感染医疗植入物的生物触发药物输送系统。我们在BioScape中的模型将有助于识别生物靶标和材料策略，以治疗生物材料相关的细菌感染。BioScape的新颖之处包括声明物种可以移动的空间范围、扩散率、形状和反应距离的语法原语，以及处理3D位置、验证反应距离和随机移动的操作语义。我们定义了一个从BioScape到3π的翻译，并证明了它在操作语义上的可靠性关键词：随机模拟，随机Pi演算，细菌-材料相互作用1介绍与现在对组织细胞如何与生物材料表面相互作用的深入和多维理解相反然而，这些互动显然非常重要。生物材料相关感染（BAI）是一个主要的临床问题[1，13，35]。 目前缓解BAI的策略集中在工程抗菌[16，18，20，22]或抗菌[9，14，19，33]涂层用于特定的生物医学器械。虽然这种方法在短期内具有临床价值，但它忽略了一个事实，即许多设备，特别是涉及再生策略的设备，需要必须可控地与组织细胞和细菌相互作用通常，表面1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2013.02.01736A. Compagnoni等人/理论计算机科学电子笔记293（2013）35浮游细菌 吸附（Ap） 弥漫性 流 被AmA杀死（Kp>> Ka） 复制（Rp <$Ra） 代谢（Mp/Ma）介质流结合AmA 保持约束 pH-释放 接触释放吸附菌 解吸 被AmA杀死（Ka Kp） 复制（Ra <$Rp） 代谢（Ma/Mp） 生产ECM优化以促进组织-细胞相互作用也支持不期望的细菌定殖（图1B）。①的人。生物材料相互作用作为围绕普通微分方程（ODE）集构建的模型的替代方案，进程代数是一种形式语言，其中具有不同行为属性的多个对象可以在整个系统开发中动态地相互交互。进程代数正被用来模拟生物系统[30，6，2]，其中，他们特别是在-吸引人的，因为他们的能力，以适应新的对象和新的生物属性，作为复杂的生物系统变得更好地理解。然而，目前，基于并发同步的建模语言要么缺乏空间属性（SPiM [27]，Kappa [12]，Petri Nets [26]）或随机性 （ SpacePi [15] ， Shape Calculus[3]），要么它们只包含有限的空间概念 （ BioAmbients [23] ， BioPepa[10]）。正如生物学实验的发现所揭示的，细胞间和细胞内动力学以及信号传导路径取决于粒子的位置和移动[17]。最近，已经提出了允许明确描述生化过程的时间空间动态的新的空间建模语言（SpacePi [15] ，DCA [36] ，L[34] ，Stochsim [24]）。其他基于代理的平台[21]包括C-Immsim图1喷砂Ti6Al4V在骨科植入物植物促进成骨细胞粘附/扩散（荧光图像），但也增强葡萄球菌集落形成（SEM插图）。继Wu， Libera etal.[37个]图2并发模型灵活地解释了多个对象类型和副本。每种类型都有其特有的属性。一个属性在其他对象中的动态表达以及每个对象下一个可能表达的属性。[32]和PathSim可视化工具[28]。然而，很少有人支持基于个人连续运动和连续空间随机模拟[4]，这些特征是精确模拟生化过程时空动力学的重要特征。为了解决这个问题，我们设计了BioScape，这是一种新的语言，它包含了随机性和3D空间属性。图2说明了模型的一个简单实例的元素。它包括四个对象：嗜热菌;吸附菌;凝胶结合抗菌剂Ama发布 结合 弥漫性 流 杀 水解A. Compagnoni等人/理论计算机科学电子笔记293（2013）3537(AmA)并释放了Ama。每一个都有属性，其中许多是相互关联的。例如，两种细菌都可以代谢，尽管速度不同。 代谢对结合型AmA特别重要，因为酸性产物会降低局部pH值，降低静电AmA-凝胶结合的强度，并使结合型AmA能够在然后，释放的AmA可以扩散和/或流动，并可能杀死结合的或非结合的细菌，同样具有不同的效率，因为生物膜细菌的增强的微生物抗性当为每个对象分配更多属性时，这种模型的复杂性请注意，空间坐标和随机性对于理解不同物体之间以及与基底之间的相互作用至关重要 到目前为止，现有的进程代数建模语言不支持这一点。此外，虽然现在正在开发许多模型来解释生物膜的形成[31，38]，但没有一个模型考虑到基质的可控特性以及这如何影响细菌粘附，增殖和表型变化。1.41.21.00.80.60.40.20.00 5 10 15 2025时间，小时8.07.57.06.56.05.55.04.54.0pH变化图3S.表皮生长图4抗菌剂从pH响应性逐层水凝胶薄膜的生物触发释放。许多实验上可测量的量可用于校准模型的元件。其中包括细菌增殖率、生物膜形态、AmA最小抑制（MIC）和杀菌（MBC）浓度、AmA结合的凝胶能力和pH依赖性以及组分分散性等。例如，Sukhishvili的小组测量了L5抗菌肽的pH依赖性释放及其对S. Epidermidis [25]已被Compagnoni和她的小组用于在BioScape中开发原型实现（图3）。该数据对应于图4中描述的模式。该模型包括在负载L5的水凝胶表面上的非稳态细菌运动、粘附和增殖以及局部代谢pH降低、触发的AmA释放和杀死细菌的计算过程（图1A和1B）。5C/D）。实验图像（图5A/B）的计算结果与我们的计算结果符合得很好。细菌细菌光密度培养基pH值38A. Compagnoni等人/理论计算机科学电子笔记293（2013）35语言设计BioScape的3D方面受到3π [7]和 SpacePi [15] 的 启 发 。 在BioScape中，每个过程都有一个隐式的A图和一个形状（图7）。形状由一组点坐标定义，该点坐标位于进程坐标系的局部虽然BioScape的语法在其隐含的局部框架内描述了过程，但其语义通过为每个过程分配一个局部映射（一个定位的过程），将过程放置在全局3D空间中（图8应用的一个a-logne地图的形状返回的形状定位在全球框架。的图5NJ 9709 S的光学显微照片。在（A）合成后原样和（B）负载L5的（PMAA）10凝胶上培养表皮细胞。使用40种细菌和（C）合成后原样的凝胶膜和（D）负载L5的凝胶膜进行BioScape模拟。活细菌是绿色的，死细菌是红色的，L5分子是小蓝点。一个图是表征过程位置的图运动是一种...通过更新一个进程的进程映射来完成。相反，3π是一种低级语言，它为程序员提供了对空间属性的绝对控制。例如，程序员可以通过检查两个进程是否足够接近来保护交互，并且它还可以为进程分配一个映射例如，3π中的冲突检查必须由程序员执行，检查与系统中每个其他实体的相应距离，并考虑每个进程的形状。相比之下，在BioScape中，程序员指定物种声明反应半径，就像在SpacePi中一样，操作语义强制执行邻近要求。因此，与3π不同，BioScape中的程序员无法使用一个双折射图。虽然3π是空间过程的通用演算，但BioScape旨在对生物和生物材料过程及其相互作用进行编程。BioScape的新功能• 我们为每个过程引入了三个新参数：运动空间，运动步骤和形状，由程序员在定义过程时指定。我们以细菌的定义为例。移动空间限制了细菌可以移动的空间。在图5中，细菌永远无法穿透凝胶膜。因此，我们将薄膜上方的体积定义为细菌的运动空间。我们假设调度程序将随机地将细菌的初始浓度放置在该空间中。移动步长表示细菌在一个时间间隔内可以移动的距离。细菌的形状代表了每个细菌在空间中占据的体积。形状有助于避免碰撞和重叠。B10微米加载肽DC一10微米所合成A. Compagnoni等人/理论计算机科学电子笔记293（2013）3539• 除了标准的反应操作发送，接收和延迟外，BioScape还有一个几何操作移动，可以推广到任何一个Anchorne变换。不同之处在于，虽然反应操作具有随机反应速率，但操作移动总是启用的为了避免反应和几何运算之间的不公平竞争，我们将语义分成两个约简关系，并考虑了具有概率和非确定性分支的异构选择算子直观地说，这就像有两个选择运算符。• 让调度器为每个进程分配初始的一个映射，以及让操作语义强制执行邻近性要求，这些设计决策大大简化了模型BioScape是一个合作工具，帮助我们开发了一个长期的多学科研究计划，以研究表面特性如何与细菌相互作用。2语法BioScape基于随机π-演算[29]，具有3D空间中过程的基元。我们假设一组名字N，其范围为x，y，.. . 和全球三维欧氏空间BioScape的语法定义见Fig. 第六章（νx@r，rad）.P定义在 过 程 P 中 ， 信 道 名 x 具 有 两 个 参 数 r 和rad∈R≥0;r是通过信道x的通信的随机速率，rad是通信半径。半径是进程之间的最大距离，以便通过更改进行通信P，Q：：=（νx @ r，rad）.P|P|Q| X (x)M：：= 0|π.P+Mπ：：=延迟@ r| ! x（x）| ? x（y）|movD：：=| D，X（x）@ ω，ω，σ = M E：：= ω|E ，x @ r，rad图6BioScape ®nelx，反应速率决定了两个足够接近的过程是否P|Q是进程的并行组合。M是异质选择，其中+是结合和交换的。M可以具有反应分支和运动分支。反应分支是概率性的，而移动分支是非确定性的，因为反应受到反应速率的影响，而移动总是被启用的。0是空进程。前缀π表示作用于π的作用。P可以执行。delay@r是单个过程的瞬时单边反应，r是随机速率。！x是输出前缀，？x是输入前缀。 我们添加一个新的几何前缀mov来翻译一个过程。我们使用标准的语法缩写，如π.P表示π.P+0，π表示π。0. X（x）是一个定义调用。D是定义的全局列表。X（x）@ω，ω，σ=M定义了具有自变量x，运动空间ω，步长ω和形状σ的过程X。运动空间是定义体积的全局坐标系中的一组点坐标。直觉上，X可以在X内移动。步长ω∈R≥0，是X在一步中可以移动的距离，它对应于X的位移率;X的形状是σ，空间中的任意体积，定义为局部坐标系中的一组坐标（图7）。空进程0的移动空间是全局空间，40A. Compagnoni等人/理论计算机科学电子笔记293（2013）35我oj►|→|KK图第七章 在它们的局部坐标系（i，j，k）中，原点为o。我OJK我距离OJ KOJOJKK奥伊 伊OJKz图八、 在全局坐标系（x，y，z）-（μ（σ））中的最小值NR.PARNR.移动μ′=translate（ω，μ，r）μ′（σ）X（x）@ω，ω，σ=mov，P+M∈DE<${X（y）}μ→{P[y/x]}μ'SR.DELAYEA→Btranss（B）transs（C）=E A C B CSR. COMX（x）@r，ω，σ=delay@r.P+M∈DE<${X（y）}μ→r{P[y/x]}μX（x）@ω，ω，σ=！z（u）.P+M∈DY（y）@ω，ω，σ=？z（v）.Q+N∈Ddis（μ，μ′）≤radE，z@r，rad<${X（x′）}μ|{Y（y′）}μ′→r{P[x′/x]}μ|{Q[y′/y][u/v]}μ'图第九章随机（SR）和非随机（NR）归约关系（样本规则）其移动步长默认为0X最多可以由D中的一个方程定义。E是通道名称声明的一种形式。 x@r，rad表示具有反应速率r和反应半径rad的通道名称x。频道名称x在E中最多出现一次。考虑下面一个细菌Bac的简单例子，它可以移动或分裂成两个子细胞。一个更复杂的例子可以在五、Bac由移动空间movB、移动步骤stepB和形状shapeB定义。直觉上，细菌可以在movB内移动，具有长度stepB的随机步骤，并且形状shapeB始终包含在movB 内。prefixmov表示长度步长B的随机移动。延迟@1.0。（Bac（）|Bac（））代表有丝分裂，即细菌分裂成两个子细胞：|Bac（），而delay@1.0 prefix用于模拟除法不是瞬时反应的事实。Bac（）@movB，stepB，shapeB =mov.Bac（）+ delay@1.0。（Bac（）|B a c （）3业务 语义BioScape的操作语义基于两个归约关系：一个非确定性关系，EDA→B，用于几何变换，在我们的例子中是movee;一个统计关系，EDA→rB，用于反应，如同步和延迟。我们经常省略D以简化符号。我们用μ来表示一个自映射;μ（s）=M×s+V，其中M是一个矩阵我ojX我我A. Compagnoni等人/理论计算机科学电子笔记293（2013）3541|∪V是一个向量[7]（见图7）。μ（σ）计算进程在全局坐标系中的位置和方向。当一个进程被初始化时，它在全局框架中的运动空间内被分配一个随机μ（μ（σ））。我们定义配置A，B，. . . 作为定位过程的平行组合。一个定位的过程{P}μ，σ是一个用一个图μ和形状σ标注的过程P。A，B ，.. . . ：：={P}μ ，σ|一|B|（νx@r，rad）.A. 为了清楚起见，我们经常省略形状σ。评价背景如下。 我们将上下文C写成C [A]，其中孔·被A：C：：=· 替换。|（νx@r，rad）。C|一|C|C|一我们定义了transm，一个关于配置的函数，它返回位于全局框架中的过程的形状（图1）。 8），使得transs（{P}μ，σ）= μ（σ），transs（（νx@r，rad）.A）=transs（A）andndtranss（AB）=反式（A）反式（B）。我们将全局坐标系中μ的原点与μ j的原点之间的距离记为dis（μ，μJ）（图11）。（八）。 我们将translate（ω，μ，r）表示为使用移动步长ω、旧映射μ和随机数r生成新的局部自适应映射μ j的函数。通常，fn是返回进程或配置的自由名称集的函数，bn是函数（S.Loc）P<$Q蕴含{P}μ<${Q}μ（S.Loc.N u）（νx @ r，rad）. {P}μ {（νx @ r，rad）.P}μ（S.Loc.μ1（形状（P））μ2（形状（Q））=μ（形状（P|Q））{P|Q} μm {P} μ1|{Q} μ2图10结构等效性（示例规则）返回进程或配置的绑定名称集，=α等于两个过程或配置，只在它们的绑定名称上不同。我们归纳地定义过程的形状如下：shape（0）=shape（X（a））= σ如果X（x）@ ω，ω，σ = M∈D shape（（νx @ r，rad）.P）= shape（P）shape（P|Q）=形状（P）形状（Q）其中给出通过并置组合两个形状而获得的形状对于不同的应用，我们可以选择合适的函数来实现，我们只需要是一个交换的结合算子，即σ1σ2=σ2σ1和（σ1σ2）σ3=σ1（σ2σ3）。 μ（shape（P））计算一个 在全局坐标系中处理P结构等价关系是包含图10中的规则的最小等价关系，并且使得并行组合是可交换的、关联的、并且对于任何μ具有中性元素{0}μ。规则S.LOC使用标准结构-在过程的理论等价性上，S.LOC.NU规则允许通道定义移动通过定位的过程，和规则S.LOC.PAR允许从配置移动通过创建一个从旧的和过程的形状派生的新的过程映射，将过程映射到单个位置的过程（反之亦然）图9给出了BioScape的非统计（EA→B）和统计（EA→rB）归约关系的样本规则。NR.Move的条件μJ（σ）≠ 0，保证了新的局部过程{P[y/x]}μ′在它的运动空间μ内.NR.MOVE可以很容易地推广到任何一个简单的地图应用程序。NR.PAR条件transs（B）transs（C）=表示还原不会引起碰撞42A. Compagnoni等人/理论计算机科学电子笔记293（2013）35或者是OVerlaps。 关于统计约化关系，E_（？）A→r_B中的r是同步或延迟的速率。SR. COM中的条件dis（μ，μJ）≤rad确保定位的进程{X（xJ）}μ和{Y（yJ）}μ′足够接近以通过通道x通信。其余的规则是标准的。4仿真仿真算法分为反应和运动两个阶段。反应阶段基于SPiM中实现的Gillespie算法，它不仅保留了每个试剂种类的浓度，还保留了每个实例的3D信息（x，y，z）。Gillespie的算法在每次迭代中产生两个输出：接下来要执行的反应和更新模拟时间的时间间隔。如果所选择的反应是两个代理之间的交互（发送/接收），则算法使用3D位置信息来识别足够接近以进行交互的两个个体代理，并且如操作语义（SR-COM）中所描述的那样进行。 如果没有两个这样的代理，则进入移动阶段。 如果所选反应是一阶反应（延迟），则算法按照操作语义（SR-D延迟）中所述传播3D信息。移动阶段使用由Gillespie算法生成的时间间隔移动阶段考虑了操作语义（NR-PAR）中描述过度拥挤超出了本文的范围然而，有几种方法可以解决这个问题。细胞有外部调节器，允许它们对邻近细胞外部的分子做出反应，这些外部调节器发出信号，在过度拥挤的条件下抑制有丝分裂。因此，如果它与正在建模的系统相关，那么解决过度拥挤的最自然的方法就是将其编程到模型中。或者，建模语言可以以不同的方式解决过度拥挤问题。例如，如果在一次迭代中在给定的移动区域内有足够的移动步骤失败，则可以禁用加剧过度拥挤的反应这种选择将具有模拟细胞中休眠的效果，例如生物膜形成的成熟I或成熟II阶段的细菌5例如在本节中，我们介绍了来自图1和图2的生物触发药物递送系统的BioScape模型4和5.我们首先用反应速率和反应半径定义了释放、杀伤和绑定的通信渠道通道释放用于水合氢离子和嵌入的药物分子之间的通信，通道杀伤用于释放的药物分子和细菌之间的通信，通道结合用于溶液中的细菌和水凝胶膜基质上的结合位点之间的通信BacF（）表示溶液中的游离细菌游离的细菌可以移动，结合到水凝胶上薄膜，生长，通过产生水合氢离子酸化环境，并被杀死A. Compagnoni等人/理论计算机科学电子笔记293（2013）3543药物分子BacB（）代表与水凝胶膜结合的细菌结合的细菌不能移动，但它们可以生长，通过产生水合氢离子酸化环境，并被药物分子杀死BindSite（）表示水凝胶膜上的结合位点。DeadBac（）表示死细菌。死细菌可以移动和降解。MolB（）代表嵌入水凝胶膜中的药物分子。药物分子可以随着水凝胶离子的产生而释放MolF（）表示释放的药物分子。它们可以移动和杀死细菌。HIon（）表示水合氢离子，其决定环境的pH值。 氢离子可以移动并释放嵌入的药物分子。resX、stepX和shapeX表示物种X的ω、ω和σ。以下是BioScape代码。release@0.004，2.0@0.001，0.5 HIon（）@resIon，stepIon，shapeIonbind@3.0， 0.2 = mov.HIon（）+！release.Hion（）BacF（）@resBF，stepBF，shapeBF = BindSite（）@resBS，stepBS，shapeBSmov.BacF（）+=？bind.BindSite（）！bind.BacB（）+延迟@0.2。（BacF（）|BacF（））+DeadBac（）@stepDB，stepDB，shapeDB delay@0.005.（BacF（）|HIon（））+=延迟@0.1？kill.DeadBac（）MolB（）@resMB，stepMB，shapeMBBacB（）@resBB，stepBB，shapeBB ==？release.MolF（）delay@0.1.（BacB（）|BacF（））+delay@0.005.（BacB（）|Hion（））+MolF（）@resMF，stepMF，shapeMF？kill.DeadBac（）= mov.MolF（）+！杀为了模拟该模型，程序员决定游离细菌（BacF（））和AmA的结合分子（MolB（））的初始浓度。图5C的模拟结果示出了仅假设初始浓度的游离细菌而没有抗菌剂的对照实验。相反，图5D图图5A和B显示了与我们的结果一致的实验图像。我们现在考虑说明随机和非随机规则的交错的示例，其从一个游离细菌、一个水合氢离子和一个AmA的结合分子开始：{BacF（）}μ1|{HIon（）}μ2|{MolB（）}μ3，以展示移动步骤与反应步骤（通信或延迟）的交错。为了使我们的例子更容易理解，我们将这三个定义展开如下：{mov.BacF（）+！bind.BacB（）+delay@1.5.（BacF（）|BacF（））+延迟@0.5。（BacF（）|HIon（））+？kill.DeadBac（）}μ1| {mov.HIon() +! release.HIon（）}μ2|{？释放.MolF（）}μ3该过 程具 有可 用的 运动 步骤 和反 应我 们首 先减 少所 有移 动步 骤。 我们 从mov.BacF（）开始。假设一个随机映射μJ1，使得：1）对于某个随机数r，μ j1 = translate（stepBF，μ 1，r）; 2）自由细菌shapeBF的平移形状在自由细菌resBF的移动空间内：μJ1（shapeBF）translateresBF，以及3）自由细菌的新形状不与空间中的其他形状重叠：transs（{BacF（）}μ′1）反transs（{HIon（）}μ2|{MolB（）}μ3）=μ。如果没有设置，则配置保持未挂起，并且可以减少下一个移动步骤。使用非随机归约规则NR.MOVE和NR.PAR，我们有：44A. Compagnoni等人/理论计算机科学电子笔记293（2013）35≺{mov.BacF（）+！bind.BacB（）+delay@1.5.（BacF（）|BacF（））+延迟@0.5。（BacF（）|Hion（）+ ？kill.DeadBac（）}μ1 | {mov.HIon() + ! release.HIon（）}μ2 |{?释放.MolF（）}μ3→{BacF（）}μ'1|{mov.HIon（）+！release.HIon（）}μ2|{？释放.MolF（）}μ3接下来，我们使用NR.MOVE和NR.PAR来减少mov.Hion（）：{BacF（）}μ'1|{mov.HIon（）+！release.HIon（）}μ2|{？释放.MolF（）}μ3→{BacF（）}μ'1|{HIon（）}μ'2|{？释放.MolF（）}μ3为了清楚起见，展开{BacF（）}μ′1和{HIon（）}μ′2{mov.BacF（）+！bind.BacB（）+delay@1.5.（BacF（）|BacF（））+延迟@0.5。（BacF（）|Hion（）+吗？kill.DeadBac（）}μ'1|{mov.HIon（）+！释放.HIon（）}μ'2|{？释放.MolF（）}μ3有三个可用的反应，一个关于通道释放的通信和两个延迟。下一个反应将使用相应的反应速率来确定。 假设下一个反应是HIon（）和MolB（）之间通过通道释放的通信。利用随机规则SR. CM和SR. PAR，若过程间距离在释放反应半径（dis（μ j 2，μ 3）≤ 2. 0）则最后一个过程简化为：{mov.BacF（）+！bind.BacB（）+delay@1.5.（BacF（）|BacF（））+延迟@0.5。（BacF（）|Hion（）+吗？kill.DeadBac（）}μ'1|{HIon（）}μ'2|{MolF（）}μ3否则，配置保持不变。下一个减少是移动步骤，我们减少所有可用的mov前缀。这包括减少mov.BacF（）、mov.HIon（）和mov.MolF（），以及随后交错随机（反应）和非随机（运动）减少。6从BioScape到3π的我们定义了一个从BioScape到Cardelli-Gardner的3 π的变体的翻译，用6.1）。由于3π不包括随机性，我们只将BioScape的空间方面转化为3π。为了使这篇论文自包含，我们包括在本节的材料，从过程中的空间[7]。“3 3π的语法如表1所示 。 每 个 数 据 项 和 值 都 有 一 个 排 序σ∈ {c，a，p，v，m}，表示通道、标量、点、向量和映射关系。一个几何数据可以是一个值或一个变量，或者是一个函数。Δ：：= xc|......这是什么？ | μ[Δ]π：：=？σx（x′）|！σx（Δ）|Δ=σΔP：：= 0 |π.P |P + P ′|P |P ′|（νx）P |μ [P]D：：=| D，X（x）= P（红色通讯）ΔA›→意味着！σx（Δ）.P + P′|？σx（y）.Q+Q′A→P|Q{y/}（红Cmp）ΔAΔ′表示Δ=σΔ′。PA→P（红Par）PA→Q表示P|RA→Q|R（Red Res）PA→ Q蕴含（νx）PA→（νx）Q（RedRes）P′<$P，PA→Q，Q<$Q′隐含P′A→Q′表13π语法和约简用户和变量，或者帧移位。一个作用项π可以是一个输入？σx（xJ），一个输出！σx（Δ），或数据比较Δ =σ Δ。输入和输出操作是A. Compagnoni等人/理论计算机科学电子笔记293（2013）3545≺X;E;D;rProProX;，E;D;rProX;，E;D;rPro（X（x）=M类似于π演算动作，而如果Δ和ΔJ的值相同，则数据比较的值为P动作受到排序约束的限制：通道必须有排序c;输入中的xJ必须有排序σ;输出中的Δ必须有排序σ;数据比较中的Δ和ΔJ必须有排序σ。过程项是标准的π演算项，加上移帧过程μ[P]：这意味着在全局框架A中运行过程P，该框架A被通过评估映射μ而获得的a-映射移动。还原关系AA，见表1。，它将两个过程与全局框架相约简规则是具有数据项Δ的按值π演算的规则，但Red Comm和Red Cmp规则依赖于求值关系A<$→，该求值关系在全局框架A中将数据Δ求值为值Δ。数据比较需要数据评估Δ AΔ J，这意味着存在一个数据值Δ j，使得Δ A›→Δ j和Δ JA Δj。”我们定义了三个函数，分别是：P-SPA、P-PRO和P-DEF，用来转换空间坐标。图，过程和定义，分别。在ASPA中，A是一个空间X是一个包含运动空间、形状和步骤的三元组。当前定义，E是一组通道声明，D是一组定义，以及r是实数。我们将滥用符号，并考虑E和D集合或列表。类似地，对于PUPPRO和PUPDEF′也是如此。X;E;D;r[过程翻译]X;E;D;rPro ProR（v x@r，rad）.P<$X;E;D;r=<$P<$X;，E;D;rP.ResProProProProCUP|Q<$X;E;D;r=<$P<$X;E;D;r |P.Par;E;D;r<$X（y）<$X;E;，D;r=X（y）P.Def0ProProProπ。P+M<$X;E;D;r={ππ. PX;E;D;r} MX;E;D;rP.ChoPro Pro在r.P<$X;E;D;r=（νm）（！cm|？cm（）。（英文）m/∈fn（P）P.Del快！x（y）.P<$X;< x@r，rad>，E;D;r=？ccx（o k）。？co k（pos）. ？ppos（p）.abs（p-H）≤ rad =a 1。！c可以。公司简介cx，ok，pos， p∈/fn（P）P.Out你说呢？x（z）.Q<$X;< x@r，rad>，E;D;r=（νok，pos）（！ccx（ok）。！cok（pos）.！ppos（H）。？cok（z）. 公司简介）cx∈/fn（Q） P.InP.P.M<，σ，ω>;E;D;r= into（T（↑（r，ω））[H]，σ，ω）=a 1.Pro<，σ，ω>;E;D;r[P.Mov.【空间形态翻译】SPA PRO{P}μSPASPASPAA.A.|BX; E; D;r =AX; E; D;r |A.B. C.X; E; D;rS. ParSPA水疗（νx@r，rad）.A<$X;E;D;r=<$A<$X ;，E;D;rS.Res[De翻译]<$X（x）@<$，σ，ω=M，D′<$DEFDEFX;E;D;r =D.无=X;E;，D;rPRO;E;，D;rDEFX;E;D;rD.Def），'DA. Compagnoni等人/理论计算机科学电子笔记293（2013）3547ǁ ǁ≡ ǁ ǁBioScape选择过程的平移是其分支的平移集合，因为3π不允许在其选择算子下进行约简否则，通过翻译这些分支而获得的削减将被冻结。因此，我们将3π最棘手的规则是用于翻译通信的规则，P.In用于输入，P.Out用于输出。 首先，输入端向输出端发送两个私有通道ok和pos，然后通过通道pos发送其位置（H）。输出计算其自身与输入发送的位置之间的距离，函数abs（p-H），即进程位置之间的差异的绝对值。如果这个距离小于反应半径（rad），那么输出端在成功的通道上发送一个通信，并执行过程P：当输入端在ok通道上接收到一个通信时，它执行过程Q。对于规则P.Mov中的移动的转换，我们假设一个函数到（p，sh，sp）中，该函数检查以点p为中心的形状s是否包含在空间sp中。 T（v）是向量为v的平移映射，而↑（r，ω）是长度为ω且方向为r的向量。该平移检查是否进入对应于NR中的条件μJ（σ）的（T（↑（r，ω））[H]，σ，）。最后，由于延迟不是3π中的前缀，因此它被转换为通道上的通信定理6.1（合理性）如果E<$DA→B或E<$DA→rB，则存在S使得水疗E;D;rA→AS和S BSPAE;D;r 对于某个数r。在我们的翻译中，整体框架A是单位元。虽然声音，这种翻译是不完整的，在这个意义上，不是所有的减少，翻译代码产生的相应减少，在源代码。实现完整性更加复杂，需要冲突检测和更精细的机制来检查接近度。7结论设S和T是集合(i)S|T={（P|Q）|P∈S，Q∈ T}(ii)μ[{}] =，μ[{P} <$S]={μ[P]} <$μ[S](iii)π.S ={π.P|P∈ S}(iv)（νm）.S ={（νm）.P|P∈ S}（Set.Par） SA→S'蕴涵S|TA→S'|T（设置红色）PA → P ′imp. {P} QA→ {P ′} Q（S.Set.Par）SS' imp. S|TS'|T（S.Set.Red）PP ′imp. {P} Q {P ′} Q表2集合上的运算、归约和同余我们将BioScape定义为复杂细菌-材料相互作用的建模和模拟。BioScape建立在3π[7]和SpacePi [15]的基础上，合并了一个α-π空间几何，反应半径1和反应边界。 正如所描述的，这种特征的组合是由我们所捕获的模型的性质严格驱动的在导言中：随机性、运动、单个过程位置（与体积中均匀混合的反应物相反）、邻近的相互作用和运动确认。我们为BioScape制定了一个约简语义，[1]虽然这个概念可以从3π中推导出来，但在实践中把它作为本原是方便的。48A. Compagnoni等人/理论计算机科学电子笔记293（2013）35在细菌感染存在下pH触发药物释放的实例中证明了这一点此外，我们验证了BioScape的翻译到Cardelli- Gardner完整的技术细节可参见配套技术报告[11]。与BioScape最相似的过程演算是Shape Calculus [3]，这是一种类似CCS的时间演算，带有模拟工具BioShape [5]。这些是一些不同的。BioScape是随机的，但Shape Calculus不是。Shape Calculus不允许动态创建通道，但BioScape允许。BioScape中的智能体可以通过一种可用于建模现象（如细胞生长）的线性变换进行修改，但Shape Calculus只允许使用速度矢量指定的运动。Shape Calculus有一个时间原语来描述延迟，而BioScape有一个随机延迟。BioScape中对一个代理的指定描述了一个允许它存在的区域，但Shape Calculus没有。这一领域有助于描述生物材料，如抗菌表面，并防止细菌穿透表面，同时允许抗菌分子这样做。另一方面，这种行为必须在形状演算中对代理我们开发了一个基于SPiM的BioScape的实现，并显示初步的模拟结果与湿实验室实验一致。我们目前正在研究一个在CUDA中实现的并行仿真算法，我们的原型实现可以在3D空间中处理100万个代理我们的长期建模目标是确定最显著抑制细菌定植和促进组织整合的底物变量组合。确认我们感谢：Mariangiola Dezani和Paola Giannini对早期草案的评论和启发性讨论;Andrew Phillips提供了BioScape实现所基于的SPiM实现; Svetlana V. Pavlukhina提供了图3中的实验数据; Justin Sousa实现了图5C和D的3D渲染，以及匿名裁判的建议。该研究项目得到了美国国家科学基金会（National Science Foundation）的部分支持，资助号为CBET-0708379，史蒂文斯研究企业基金（Stevens引用[1] C. R.阿西奥拉植入物感染的新概念和新武器。国际人工器官杂志，32（9）：533[2] Y. Bao、黑腹拟步行虫A. B. Compagnoni、J. Glavy和T.白. G蛋白偶联受体对G蛋白激活周期的计算建模 在2010年第 四 届 膜 计 算 和 生 物 启 发 过 程 微 积 分 研 讨 会 上 。 （ MeCBIC ） ， 在Electronic Proceedings inTheoretical Computer Science，第39-53页，2010中的第40号。[3] E. Bartocci，F. Corradini，M. R. D. Berardini，E. Merelli和L.铁清形状演算。三维形状的空间移动演算S c i . Ann. Comp. Sci. ，20：1A. Compagnoni等人/理论计算机科学电子笔记293（2013）3549[4] A. T. Bittig和A. M.乌马赫多层次细胞生物学空间建模。在冬季模拟会议，第608-619页[5] F. Buti，D. Cacciagrano，F. Corradini，E. Merelli和L.铁清Bioshape：一个基于空间形状的生物系统尺度无关仿真环境。Procedia Computer Science，1（1）：827[6] L. Cardelli，E. Caron，P. Gardner，O. Kahramanogullari和A.菲利浦rho gtp结合蛋白的过程模型。Theor. Comput. Sci. ，410（33-34）：3166[7] L. Cardelli和P.迦纳太空中的进程载于CiE，第78[8] F. Castiglione和M.伯纳斯基C-immsim：
我的内容管理
展开
