生化空间语言（BCSL）：生物化学系统的模型规范和分析

可在www.sciencedirect.com在线获取理论计算机科学电子笔记350（2020）91-116www.elsevier.com/locate/entcs可执行生化空间用于生物化学系统的规范和分析MatejTroja'k，DavidSafra'nek，LubosBrim捷克布尔诺马萨里克大学系统生物学实验室JakubSalagovic，JanCerveny'全球变化研究中心AS CR，v. v. i.，捷克共和国摘要我们提出了第二代的基于规则的语言称为生化空间语言（BCSL），结合了不同的方法的优点，从而使一个e-jourt克服现有的解决方案的几个问题。 该语言的关键方面是它使用的抽象级别，这允许可伸缩性。和生物化学实体的紧凑的等级规范。这种抽象使得独特的分析技术能够在语义和语法级别上对用语言编写的模型的属性进行推理。保留字：基于规则的建模，形式化规范，静态分析1引言在系统生物学中对复杂系统进行建模必须在几个抽象层次上进行，这些抽象层次很好地反映了已知信息[14]。在每一个层次上，系统都必须用一种形式化的语言来严格描述，以避免误解和模糊的解释。系统越复杂，就越难在严格描述它的同时不失去人类可读性和描述的紧凑性。一个现代的生物化学系统规范语言，可以在系统生物学实践中使用，必须是分层的和可执行的。分层描述允许表达联系人：xtrojak@fi.ju.cz或safranek@fi.ju.cz这项工作得到了捷克科学基金会资助18- 00178 S和捷克国家基础设施资助LM 2015055的支持。https://doi.org/10.1016/j.entcs.2020.06.0061571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。92M. Troják等人/理论计算机科学电子笔记350（2020）91不同详细程度的单个系统组件。由于并非所有的生物化学结构都是详细已知的，语言必须支持部分知识的表达。另一方面，可执行性允许自动分配描述与适当的形式（数学或编程）结构，使模拟和详尽的分析所需的属性或揭示错误的描述。用于描述生物化学系统的传统方法是：（i）化学方法，其通过化学反应采用这两种方法的问题是模型描述和执行的可扩展性：即使模型的制定没有遇到可扩展性问题，执行或模拟仍然可能是不可行的。为此，计算机科学提供了一种基于具有各种严格可执行语义的抽象语言的计算方法。这些方法之间的关系已在[4]和[12]中讨论。基于规则的建模[7，9]和过程代数框架[4，5，23]提供了一种有前途的计算方法。基于规则的模型是化学中使用的基于机械反应的模型的自然延伸。基于规则的框架不是操作对象，而是操作类型，这些类型允许避免在直接指定底层对象时发生的组合爆炸。模型的语义是根据给定类型定义的规则给出的。基于规则的方法的一个重要优点是可以自动生成数学模型。特别地，代替依赖于单个数学形式体系，因此可以针对给定模型获得不同的数学模型（例如，常微分方程[3]、偏微分方程[1]、化学主方程或连续时间马尔可夫链[19，25]、反应微分方程系统[26]等）。虽然基于规则的模型是数学模型的一个很好的替代品，但它们在实践中还没有得到充分的应用。原因是现有的形式主义依赖于神秘（符号）语法，并且它们限于相互作用的特定子集或过于抽象：BNGL[9]和Kappa[7]靶向蛋白质-蛋白质 结 合 ; BioSPI[23] 和 SPiM[22] 使 用 非 常 基 本 的 不 对 称 二 进 制 同 步 基 元 ;BioPEPA[5]使过程代数框架适应化学反应，同时放松组合相互作用的紧凑性;Chromar [13]利用函数编程。因此，这些语言可以被理解为允许精确的形式化描述和分析生物过程的低级形式。基于这些形式主义的原则，已经开发了几个高级框架：rxncon[24]专注于监管交互并允许从实验证据构建规则，LBS[21]和LBS-κ[20]通过模块化丰富了基于规则的框架，PySB[17]将Kappa和BNGL嵌入到Python 中 ， MetaKappa[6] 通 过 代 理 站 点 的 分 层 继 承 扩 展 了 Kappa 语 言 ，BioCHAM[2]明确地将规则与其数学语义分离。 没有一这些框架提供了一个succiently通用的解决方案，用于描述和注释在细胞水平上集成的异质生物物理过程。显然，不同的方法需要相应地结合起来，使一个统一的，M. Troják等人/理论计算机科学电子笔记350（2020）9193支持可执行性的分层建模和注释基础。[18]中提出的工作旨在将注释标准引入基于规则的框架中。另一方面，SBML multi[29]将基于规则的描述转换为统一的XML格式，该格式固定了对象的层次结构和规则的模块化。它将基于规则的范式推向描述生物系统的标准技术然而，它并没有直接解决可执行性和高级分析问题，这些问题是基于规则的框架的一个重要方面。我们的长期目标是开发一个通用的建模框架[16，27]。与一般注释格式生化空间[15]一起，它尊重维护现有ODE模型的需要，但允许将它们与生物学家可理解的基于规则的机制描述对齐，尺寸紧凑，在允许基本分析任务方面可执行，确保描述的一致性，并提供现有生物信息学注释数据库的链接。这样一个全面的解决方案允许支持建模者在构建具有明确生物化学意义并且可以容易地集成的数学模型方面取得成功。 此外，机械描述可以在以后用作具有基于规则的建模的所有优点的计算模型。为此，我们开创了一个想法，通过引入一种名为生化空间语言（BCSL）的高级规则语言的第一个原型，将基于规则的建模的优势与化学反应的简单性相结合。语言在Kappa的顶部被定义。BCSL的目标是比Kappa更高级别的抽象，Kappa专注于蛋白质结合位点之间的态射。因此，基于Kappa的BCSL公式具有有限的表达性，并且不适合我们框架的目标。此外，Kappa不提供层次化描述，这是BCSL的关键方面之在本文中，BCSL被重新定义并相对于[ 8 ]中提出的主要原型进行了显着改进：（i）分层和可组合的对象类型和规则被定义，而无需在现有的基于规则的框架中对其进行编码，从而避免了任何信息丢失，（ii）规则的可执行语义直接在语言级别定义，从而为特定于所考虑的抽象级别的独特分析任务奠定了基础，（iii）软件工具可用于维护和分析BCSL规范- BCSGen 1。新版本的BCSL强调了以下几个方面：（i）人类可读性（易于阅读，编写和维护），（ii）可执行性（定义了正式的可执行语义，允许有效的静态分析和一致性检查），（iii）通用性（主要是不同的细胞过程可以在单个规范中充分组合），（iv）可伸缩性（避免描述的组合爆炸），（v）层次结构（分层描述对象类型，允许从更简单的结构组合组装）。此外，我们还提供了几种静态分析技术，这些技术利用了特定抽象级别它们主要用于一致性检验、模型降阶和可达性分析。特别是，规则冗余消除允许检测模型中不必要的规则，基于上下文第1https://github.com/sybila/BCSgen94M. Troják等人/理论计算机科学电子笔记350（2020）91约简和静态不可达性分析在不一定需要的情况下防止昂贵的转换系统枚举方面唯一地处理不可达性这些技术在成纤维细胞生长因子（FGF）信号通路模型上得到了证明，并在静态分析领域显示出实际影响。2生化空间语言在本节中，我们正式定义了生化空间语言。首先，我们定义所有需要的对象（所谓的代理）和它们之间的交互（所谓的规则;例如，见图1），然后我们定义语言的语法和BCSL模型的语义。KaiC蛋白KaiBC二聚体S{u}：：KaiC：： KaiBC：：cytS{p}：： KaiC：： KaiBC：：cyt丝氨酸残基（非磷酸化）丝氨酸残基（磷酸化）细胞溶质Fig. 1.一个规则的例子。该规则描述了丝氨酸（S）氨基酸残基从非磷酸化状态到磷酸化状态的变化。此外，只有当丝氨酸是KaiC蛋白的一部分时，这种磷酸化才会发生，这发生在KaiC和KaiB蛋白的蛋白质复合物内。的整个过程仅允许在胞质溶胶（cyt）隔室内部2.1正式任命在我们继续之前，我们提供一些基本的定义和符号，以建立语言的形式定义。定义2.1（多集）多集Ω是一个对（A，m），其中A是一个集合，m：A→N是从A到自然数集合的函数。集合A称为元素的参考集合。 对于A中的每个元素a，a的重数（即出现的次数）是数m（a）。符号2.2• 设S是一个集合。我 们 用ΩS表示所有可能的有限多重集（A，m）的集合这样，A？• 令O =（o1，...，n）是一个元组。· 我们用Ω（O）表示从元组O构造的多重集。· 我们用σ（O）表示元组O的长度为n的所有可能排列的集合。• 通过|Y|我们表示（i）元组Y的维数 或（ii）（多）集Y的基数。M. Troják等人/理论计算机科学电子笔记350（2020）9195i=1.Σ定义2.3（标记跃迁系统）标记跃迁系统（LTS）L是一个四元组（S，A，T，s0），其中S是一组状态，A是一组标记，T<$S×A×S是一个跃迁关系，s0∈S是一个初始状态。定义2.4（LTS中的路径）设L =（S，A，T，s0）是LTS。我们将路径定义为状态s1s2s3的 序 列 。 . 对a ∈A，有（si，a，si+1）∈T.定义2.5（元组连接）设X =（x1，.，xn），Y =（y1，.，y m）是对某个n，m∈N的两个元组。两个元组的连接，记为X ++ Y，定义为：X ++ Y =（x1，...，x n，y1，.， y m）。定义2.6（级联和）设T =（T1，T2，...，T n）是序列n∈N的元组。 元组序列++n的连接Ti定义为：ni=1T i= T1++ T2++. ++ T n2.2对象定义设NA，NT，Nδ，NC分别是原子名、结构名、状态和区室的互斥有限集合。此外，ε是保留符号，不属于任何这些集合。为了更好的可读性，我们提供了最重要对象的语法示例及其定义。下面给出句法的形式定义以及与宾语的关系（2.3节和2.4节）。2.2.1签名定义2.7（签名）原子签名是一个函数，它将每个原子名与一组状态名相关联。类似地，结构签名是一个函数T：NT→2NA，它将每个结构名称与一组原子名称相关联。签名为原子名定义了一组允许的状态，为st r定义了一组允许的原子名。结构名称。例如，S→{u，p}，Q→{a，i}是2.2.2原子剂定义2.8（原子代理）原子代理A是一个对（η，δ），其中η∈ NA是一个名称，δ∈ Nδε{ε}是一个状态。A的名字和状态通常分别用η（A）和δ（A）表示原子试剂是用于描述生物实体的最简单的对象。每个原子代理都有自己的名称和状态。原子代理的容许状态的允许集合（具有额外的空ε状态）由签名A（η）给出定义2.9（原子主体的平等关系）设A，AJ是原子主体。 一等于AJ，记为A=AJ，i <$η（A）=η（AJ）<$δ（A）=δ（AJ）。++原子签名，KaiC→ {S，Q}，KaiB→{S，Q}是一种结构化签名。96M. Troják等人/理论计算机科学电子笔记350（2020）91直觉上，原子代理上定义的相等是一个等价关系。记法2.10我们用符号A来表示所有可能的原子主体的宇宙。原子试剂通常用于表达可以改变其状态的小生物实体，例如氨基酸、小无机分子等。原子代理的例子是A1=（S，u），记作S{u}，和A2=（Q，ε），记作Q{ε}。注意，ε的含义是状态是未知的，或者在给定的上下文中不重要。定义2.11（原子代理的相容性）设A1，A2为原子代理。如果A1=A2或η（A1）=η（A2）<$δ（A1）=ε，则A1与A2相容，记为A1A2。原子代理的兼容性是代理之间定义的关键属性。一个代理与另一个代理是兼容的，如果他们有相同的名字，并且他们处于相同的状态，或者第一个代理处于未知状态。它提供了一种正式的方法来比较哪个代理更详细，即它的状态更具体。定义2.12（完全指定的原子主体）设A∈A是原子主体。我们假设年龄ntA是完全确定的，设ΔA，i ∈AJ∈A，满足AJA：<$（AJA）。2.2.3构造剂定义2.13（结构主体）我们将结构主体T定义为一对（η，γ），其中η∈ NT是一个名称，γ∈A是一组称为部分合成的原子主体，使得λA，AJ∈γ：η（A）/=η（AJ）。施事T的名称和部分组成通常分别用η（T）和γ（A）表示一个结构剂代表一个生化对象，它是由几个已知的原子剂，而我们知道，一个组成是抽象的，不一定是完整的。为了将这种抽象纳入我们的语言中，结构代理被定义为使用唯一名称和一组原子代理进行标记。根据给定的与结构代理同名的结构签名，此集合受到限制。定义2.14（结构主体的等式关系）设T，TJ为结构主体。T等于TJ，记为T=TJ，i <$η（T）=η（TJ）<$γ（T）=γ（TJ）。直观地说，结构主体上定义的等式是一种等价关系。结构主体的关键构造是部分组成，部分组成被定义为一组原子主体，这些原子主体被认为是结构主体的相关部分。我们允许这个集合是空的，具有生物结构的意义，不知道它的成分。符号2.15我们用符号T表示所有可能的结构主体的论域。M. Troják等人/理论计算机科学电子笔记350（2020）9197结构剂的典型例子是蛋白质，其中原子剂是在特定环境中感兴趣的氨基酸。想象一下，在我们的建模系统中，几百个氨基酸中只有三个能够进行一些翻译后修饰，如磷酸化，甲基化等，只建模这三个氨基酸而不是整个蛋白质的一级结构是合适的。结构剂的实例是T1=（K，{（S，p），（Q，i）}），写作K（S{p}，Q{i}），和T2=（K，{（Q，a）}），写作K（Q{a}）。我们在结构施事的部分成分的水平上定义差异，这对于下面的语义定义是必要的定义2.16（部分合成的区别）设γ，γJ是部分合成。我们定义了部分复合的差γgγJ={A|A∈ γ<$A/∈ γ <$γJ}其中γ<$γJ={A|A∈γ<$AJ∈γJ：η（AJ）= η（A）}。定义2.17（结构剂的相容性）设T1，T2为结构剂.主体T1与主体T2相容，记为T1T2，i <$T1= T2或η（T1）=η（T2）<$$>A1∈γ（T1）<$A2∈γ（T2）：A1A2。如果可以从第一个代理与第二个代理的组成的原子代理创建对，使得这些原子代理都是唯一的，则结构代理是兼容的。对于这样的配对，每对中的代理必须兼容。 它提供了一种形式化的方法来比较哪一个代理更具体，即部分组成中原子代理的特定状态是否给定定义2.18（完全特定结构的智能体）设T∈T是一个复合智能体。我们假设年龄tT是完全确定的，设ΔT，i∈TJ∈T，则TJT：<$（TJT）.2.2.4络合剂一个复杂的代理代表一个非平凡的复合生物化学对象，它是从已知的生物对象诱导构建的。在基于规则的语言中，这通常是通过在单个生化对象之间引入键来定义的。在BCSL中，我们从债券的详细说明中抽象出来，我们宁愿假设一个复杂的作为共存的某些对象在一个特定的群体。此外，一个复杂的代理驻留在一个隔间，这给了它一个空间位置。定义2.19（复杂智能体）我们将复杂智能体X定义为一对（μ，com），其中μ∈（A<$T）n是智能体序列，com∈ Nc是一个隔室，n∈N。试剂X的序列和隔室通常用μ（X）表示，com（X）。复杂主体的关键元素是从现有主体中归纳构造的序列。与结构代理中的部分组合相反，我们允许在序列水平上进行复制（某个名称的代理可以在序列中出现不止一次序列中的顺序对于唯一地标识相等的代理是必要的另一方面，当比较两个序列时，我们不考虑顺序。98M. Troják等人/理论计算机科学电子笔记350（2020）91.Σ定义2.20（复合主体的等式关系）设X，XJ是复合主体。X等于XJ，写作X=XJ，i <$com（X）=com（XJ）<$Ω（μ（X））= Ω（μ（XJ））。直观地说，复杂主体上的定义的等式是一个等价关系。复合剂的示例是X=（（K，{（S，p），（Q，i）}），（S，p）），cell，写作K（S{p}，Q{i}）.S{p}：：cell。记法2.21我们用符号X表示所有可能的复体的论域。复杂代理封装其他代理-原子代理或结构代理不能单独存在（可能发生只有一个项目在其序列中的情况）。这保证了每个原子和结构代理都间接地给出了空间位置– the定义2.22（配位剂的相容性）设X1，X2为配位剂。复施体X1与复施体X2相容，记为X1X2，i <$X1=X2或com（X1）=com（X2）<$$> μJ∈σ（μ（X2））使得<$i∈[1，n]：μi（X）μji，其中n是序列的长度，两个序列的长度相同如果存在第一个施事的序列的置换，使得两个序列中相同位置上的个体施事是相容的，则复合施事是相容的。它提供了一种正式的方法来比较哪个代理更具体。定义2.23（完全指定的复杂主体）设X ∈ X是复杂主体。 设ΔX，i ∈XJ∈X，满足XJ/=X：<$（XJX），则年龄ntX是完全确定的.值得注意的是，配合物没有结合拓扑结构。虽然它提供了许多优点，特别是在组合爆炸方面，但它也有一些缺点。最重要的一点是，我们不能在复合物的水平上表达结构修饰。这些必须使用状态进行编码。2.2.5规则让我们举一个简单的规则例子K（S{u}）.B（u）：：cytK（S{p}）：：cyt+B（u）：：cyt.这个规则将K和B（都是结构剂）的复合物分解为两个独立的剂，而结构剂K将其原子剂S的状态从u改变为p。为了形式化地描述规则，我们需要捕获所谓的左手边（符号前的部分）和右手边（符号后它是通过索引规则中的各个位置并在它们之间创建索引映射来实现的。定义2.24（规则）我们将规则R定义为一个五元组（χ，ω，i，ω，ω），其中：• χ∈Xn是一个复代理序列，• ω∈（A <$T）m是原子和结构代理的序列M. Troják等人/理论计算机科学电子笔记350（2020）9199（（C，⎣⎥·• i ∈ {0，. n}是确定的左手边的末端（LHS）的索引，χ，• 是从ω到χ的指数映射，• <$∈（（ {−}<$N）2）n是从LHS到RHS其中n，m∈N，LHS =（χ1，.，X1）是左手侧，并且RHS =（X1+ 1，...，χn）是右手边。这个特殊定义的原因是有必要捕捉规则的左手边和右手边之间的关系。这是通过从复合剂序列χ中枚举所有原子和结构剂ω来完成的。在ω中的代理之间的索引映射确定来自左手侧和右手侧的彼此对应的代理对。有可能存在没有配对（用−表示）的代理，当规则在从（resp. 出到）系统。另一个索引映射用于将从ω开始的施事关联回复合物的原始序列χ。最后，通过索引i，我们确定规则左侧的结束。请注意，在左侧没有代理的情况下，索引为零。符号2.25我们用符号R来表示所有可能规则的宇宙。规则的示例是R=（x，ω，i，ω，i），其中：·χ=·ω=- 是的（（K，{（S，u）}），（B，）），cyt，.Σ- 是的（（A，ε）），cyt，⎡⎢⎣（K，{（S，u）}），（B，n），（C，n），（D，i），（A，ε），（K，{（S，p）}），（B，ε），（C，ε），（D，a），（A，ε），（H，u）⎤⎥⎦- 是的（（K，{（S，p）}），（B，），（C，）），cyt，• i= 3⎢写为：. （（D，a），（A，ε）），cyt，. （（H，u）），cyt• =（2， 4， 5， 8， 10， 11）[（1， 6）;（2， 7）;（3， 8）;（4，9）;（5， 10）;（−， 11）]K（S{u}）。B（n）：：c yt+C（n）. D{i}：：cyt+A{ε}：：cyt<$K（S{p}）。B（）。C（ε）：：cyt+D{a}.A{ε}：：cyt+H{u}：：cyt不是所有的规则都有意义。例如，一个规则，其中没有一个单一的代理被改变或规则，其中的左手和右手之间的关系将是不清楚的。为了避免这种情况，我们需要指定规则何时是良构的，即它在语义上有意义。100M. Troják等人/理论计算机科学电子笔记350（2020）91定义2.26（良构规则）设R是规则，i，j∈N。我们说规则如果以下所有条件成立，则R=（χ，ω，i，ω，ω）是良构的(i) 至少一个条件成立：(a) <$（i，j）∈<$：ωiωj，(b) |LHS（R）|/= |RHS（R）|、M. Troják等人/理论计算机科学电子笔记350（2020）91101（c）n∈[1，i]：com（xi）com（xi+i）;(ii) n（i，j）∈n：η（ωi）=η（ωj）;(iii) <$（−，i）∈<$：Δωi.如果一条规则满足定义2.26中给出的条件，那么它就是良构的。这些条件基本上要求代理在规则应用期间必须改变。这通过条件（i）来确保，其中存在三个选项：（a）来自规则的LHS和RHS的至少一对代理是不同的;（b）LHS和RHS的长度是不同的，即，要么创建新代理，要么形成/解离复合物（c）舱室被改变。允许这些子条件的任何组合第二个条件（ii）保证规则ω中的结构和原子代理对具有相同的名称。 请注意，条件（i）和（ii）不适用于ω中那些在规则的另一侧没有配对的代理。最后，条件（iii）声称，如果有一个代理人不具有通过索引映射定义一对（用−表示），它需要是一个完全指定的代理（但仅在代理创建的情况下，它不需要代理降级）。2.3语法在本节中，我们定义了语言的语法，即我们通常如何编写它，以使符号易于编写和可读。它对应于上面定义代理和规则时给出的例子。定义2.27（语法）原子表达式结构表达式复杂表达式α：：= η{s}|η{ε}τ：：= η（γ）|η（π）r：：= β1........ β k：：cη：：= n ∈ NAγ：：= α1，.， α kβi：：= α|τs：：=n∈Nδη：：=n∈NTc：：=n∈Nc规则表达式Q：：= Γ 1+. + r n r n+1+. + Γm其中m，n∈N0<$m> n，k∈N.2.4翻译功能一旦我们定义了BCSL代理和语言的规则和语法，我们需要将它们连接起来，以便为语法中编写的模型提供语义意义。为此，我们定义平移函数F（定义2.28）。它是根据作为参数给出的表达式递归定义的。102M. Troják等人/理论计算机科学电子笔记350（2020）91（）（）（）.Σ（Ⅲ）。（1）（Ⅲ）i=1.<$$>）<$）Σ⎧⎪⎨⎪一）定义2.28（平移函数）我们根据双方括号中给出的表达式定义平移函数F。 ）如下：F <$η{ε}） =（η，ε）∈F <$η{s}） =（η，s）∈不F<$η（ ） =（η，η）∈Fη（α1，…， ak）=n，{F a1，...，F ak}∈TFα1。 . . . .α k：：c=（Fα1 ，...，Fα k），c∈XR使得：FΓ 1+... + r n r n+1+. + Γ m=（χ，ω，ι，ω，ω）∈• χ=F1，...，FΓn，Fn+1，.，F'm，• ω= ++|χ|μ（χi），• i=n，• n =（J1，.，其中Jk=·ki=1|、|,{（i，j）|i ∈ [1，i] j∈ [i+1，|ω|][]]|i − j|=}i={（i，−）|i ∈ [k，n i] n k = |ω| − +1 |{\fnMicrosoft YaHei}n{（−，j）|j ∈ [k，|ω|][k]= 2 × [i+1}其中，符号j是与一个排序一起定义的，使得对于每个k∈N，符号J−J> k，并且忽略符号j定义中的所有下降区间。注意，translation函数只对定义2.27中定义的表达式起作用。该函数递归地从给定的表达式创建对象。每个规则表达式首先被分解为LHS和RHS，然后每个代理表达式被转换为一个对象。适当的索引映射是从复合物序列χ和原子和结构剂序列ω创建的。2.5BCSL模型我们继续进行BCSL模型的定义。我们总是考虑一个初始化的模型，这意味着定义包含系统的初始状态（解，定义2.29）。BCSL模型的定义还包含规则和签名。定义2.29（解）解是一个多集S∈ΩX，使得A是S的参考集，且<$X ∈A：ΔX。定义2.30（BCSL模型）我们将BCSL模型M定义为四元组（R，RBA，RBT，S），其中R是一组规则，RBA是原子签名，RBT是结构签名，S是初始解。BCSL模型由一组规则R形成，这些规则定义了该模型初始解S定义了模型开始时的状态一M. Troják等人/理论计算机科学电子笔记350（2020）91103XX(a)ω 我∈A如果ωi=ωjAtomic Signature定义了规则中使用的所有原子代理的允许状态。最后，结构签名RINT定义允许规则中使用的所有结构代理的原子代理2.6匹配在这一点上，我们定义匹配，它将用于定义BCSL模型M的语义。定义2.31（匹配）设R=（χ，ω，i，n，n），r=（χJ，ωJ，iJ，nJ，nJ）是两个规则，S ∈ Ω是一个解，i，j∈N.让|=<$R× Ω ×R是满足一个元组（R，S，r）∈|=，写为R|=rS，i(i)i=ij=j= j（二） |为|χj|∧| ω|为|ωj|、|,(iii) i ∈ [1，|χ|]：χJiχi，(iv) Ω（LHS（r））=S，（v）<$（i，j）∈ <$： .ωi=ωiJ<$ωj=ωjJ如果ωiωj（b）ωi∈T<$γ（ωIJ）gγ（ωi）=γ（ωJJ）gγ（ωj）.注2.32注意来自元组（R，S，r）的规则r∈| =是所谓的反应，其特征在于作为规则R的一个实例。对于模型中的每个规则，可以枚举所有潜在反应，并以这种方式将基于规则的模型转换为基于反应的模型。2.7语义定义2.33（替换）设→ΩX×R× ΩX为替换关系S.T. 一个元组（S，R，SJ）∈→，设S→RSj，i <$$>r∈R<$x<$Ssuch，R|=rx∈ SJ\（S\x）= Ω（RHS（r））。替换关系定义了如何根据给定的规则转换解决方案对于BCSL模型M，规则产生包含边S →RSJ的解之间的标记转移系统LTS（M）。请注意，我们可以实现如果我们首先从规则中生成所有可能的反应，然后用它们来替换（规则只是反应的一般化集合3句法扩展在本节中，我们定义了几个语法扩展，以增加规则表达式的可读性。请注意，每个规则表达式的扩展形式都可以转换为上面定义的基本形式（2.3节）。所有包含以下扩展的规则为了更好地演示，我们提供了一个运行示例，ωiJ=ωjJ104M. Troják等人/理论计算机科学电子笔记350（2020）91它将遍历所有语法扩展（运行示例3.1）。请注意，示例模型没有生物学意义，其唯一目的是有效地演示所有定义的语法扩展。运行示例3.1（示例模型M）(i) KaiC（S{u}，T{ε}）.KaiC（S{ε}，T{ε}）.KaiC（S{ε}，T{ε}）：：cytKaiC（S{p}，T{ε}）.KaiC（S{ε}，T{ε}）.KaiC（S{ε}，T{ε}）：：cyt(ii) KaiC（S{u}， T{ε}）. Kai B（ε）：：cy t<$KaiC（S{p}， T{ε}）. Kai B（）：：c yt(iii) KaiC（S{ε}，T{ε}）：：cyt+KaiC（S{ε}，T{ε}）：：cyt+KaiC（S{ε}，T{ε}）：：cytKaiC（S{ε}，T{ε}）.KaiC（S{ε}，T{ε}）.KaiC（S{ε}，T{ε}）：：cyt(iv) KaiC（S{ε}，T{ε}）.KaiC（S{ε}，T{ε}）.KaiC（S{ε}，T{ε}）：：cytCYTKaiC（S{ε}，T{ε}）：：cyt+KaiC（S{ε}，T{ε}）：：cyt+KaiC（S{ε}，T{ε}）：：A=，S→ {u，p}，T→ {a，i}，我们省略了初始状态定义，只是为了例子的简单，因为所有的扩展只涉及规则表达式。3.1部分组合上下文消除可以从结构剂的部分组合中省略所有具有未指定状态ε的原子表达式（运行示例3.2）。这样的代理表达式不提供任何额外的信息，并且可以从给定的签名中重构整个部分组合运行示例3.2（示例模型M）(i) KaiC（S{u}）. KaiC（）.KaiC（）：：cytKaiC（S{p}）.KaiC（）.KaiC（）：：CYT(ii) KaiC（S{u}）.KaiB（）：：cytKaiC（S{p}）.KaiB（）：：cyt(iii) KaiC（）：：cyt+KaiC（）：：cyt+KaiC（）：：cytKaiC（(iv) KaiC（）.KaiC（）.KaiC（）：：cytKaiC（）：：cyt+KaiC（）：：cyt+KaiC（）：： cyt此外，这个扩展可以通过完全省略结构代理中的（）部分而更进一步（运行示例3.3）。由于我们定义了结构签名RNT，我们可以明确地确定哪些名称属于结构代理，并且可以很容易地重建该句法部分运行示例3.3（示例模型M）(i) KaiC（S{u}）.KaiC.KaiC：：cytKaiC（S{p}）.KaiC.KaiC：：cyt(ii) KaiC（S{u}）.KaiB：：cytKaiC（S{p}）.KaiB：：cyt(iii) KaiC：：cyt+KaiC：：cyt+KaiC：：cytKaiC.KaiC.KaiC：：cytT=KaiC→ {S，T}，KaiB→{S，T}M. Troják等人/理论计算机科学电子笔记350（2020）91105⎩⎭(iv) KaiC.KaiC.KaiC：：cytKaiC：：cyt+KaiC：：cyt+KaiC：：cyt这种语法扩展为语法带来了很大的可读性，同时保留了模型M上下文中的所有信息。3.2复合签名我们通过复签名X扩展了模型定义（运行示例3.4）。在这个签名中，有效的复杂表达式有定义的别名。然后，用别名替换原始复杂表达式运行示例3.4（示例模型M）复杂签名的定义=KaiC3：：cyt→KaiC。KaiC. KaiC：：cyt，KaiBC：：cyt→KaiC.KaiB：：cyt(i) KaiC（S{u}）.KaiC.KaiC：：cytKaiC（S{p}）.KaiC.KaiC：：cyt(ii) KaiC（S{u}）.KaiB：：cytKaiC（S{p}）.KaiB：：cyt(iii) KaiC：：cyt+KaiC：：cyt+KaiC：：cytKaiC3：：cyt(iv) KaiC3：：cytKaiC：：cyt+KaiC：：cyt+KaiC：：cyt复杂签名的使用有其局限性。一旦指定了上下文，就不能使用别名。我们将从以下几个方面来解决这个问题。3.3方向我们允许规则表达式是双向的-它只是两个规则表达式的捷径，它可以转换为基本的规则表达式形式。一个规则表达式Q：l惠r可以写成两个规则表达式Q1：l⇒r和 Q2：rl（运行示例3.5）.运行示例3.5（示例模型M）(i) KaiC（S{u}）.KaiC.KaiC：：cytKaiC（S{p}）.KaiC.KaiC：：cyt(ii) KaiC（S{u}）.KaiB：：cytKaiC（S{p}）.KaiB：：cyt(iii) KaiC：：cyt+KaiC：：cyt+KaiC：：cyt惠KaiC3：：cyt运行例3.4中规则（iii）和（iv）的定义被运行例3.5中的一个双向规则（iii）取代。3.4化学计量对于形式的规则表达式：β1：：c + β2：：c +. + β n：：c β1.β2.. β n：：c我们可以对两边重新排序，这样我们就得到了非交叉划分P = B1/B2/。... /Bk106M. Troják等人/理论计算机科学电子笔记350（2020）91其中k≤n来自其索引[1，...，n]使得：<$B∈ P <$β，βJ∈ B：β=βJ，<$B，BJ∈ P<$β∈B<$βJ∈BJ：ββJ使得BBJ.对于左手边β1：：c + β2：：c +. . + β n：：c可以替换所有规则表达式[βi， .. . ，βj]，其通过符号“k β j”归属于相同的非交叉划分B，其中β是来自β i，.，βj（它们都是等价的）和k是分区B中的表达式的数目（运行实施例3.6）。 请注意，这个过程是完全可逆的运行示例3.6（示例模型M）规则表达式的定义：(i) KaiC（S{u}）.KaiC.KaiC：：cytKaiC（S{p}）.KaiC.KaiC：：cyt(ii) KaiC（S{u}）.KaiB：：cytKaiC（S{p}）.KaiB：：cyt(iii) 3KaiC：：cyt惠KaiC3：：cyt惠来自运行示例3.5的规则表达式（iii）的定义被使用化学计量的新规则表达式替换3.5位置本地化操作符旨在允许表达分层构造的代理表达式的替代方式（运行示例3.8）。其主要思想是允许放大到复杂和结构表达式的各个部分为此，我们使用a：：b表示法，使得a、b是满足定义3.7中给出的条件之一的任意代理。定义3.7（位置条件）(i) 存在AJ∈γ（T）使得A一个J，(ii) A：： X惠存在AJ∈μ（X）使得 AAJ，(iii) 存在TJ∈μ（X）使得TTJ。对于每一对代理（α，β），它们之间允许试剂β的部分）组合物，使得其与试剂α相容。然后，将agentαJ与agentα合并，构造agentβJ运行示例3.8（示例模型M）(i) S{u}：：KaiC：：KaiC3：：cytS{p}：：KaiC：：KaiC3：：cyt(ii) S{u}：：KaiC：：KaiBC：： cytS {p}：：KaiC：：KaiBC：：cyt(iii) 3KaiC：：cyt惠KaiC3：：cyt惠运行示例3.6中的规则表达式（i）和（ii）的定义被替换为位置。本地化操作员允许我们额外使用复杂的签名。M. Troják等人/理论计算机科学电子笔记350（2020）91107≤3.6变量运行示例3.8中的规则表达式（i）和（ii）非常相似，除了它们发生的复杂表达式的上下文。我们可以用一个给定域的变量来在规则表达式中，可以使用变量引用一个代理表达式，作为一组可以替换的规则代理表达式（运行示例3.9）。这样的代理表达式被引用为？X.此外，在这种情况下，当一个？X用于一个位置，它必须满足定义3.7中的条件。与变量相关联的每个规则表达式可以容易地被写为若干规则表达式，其中变量被来自附加到变量的代理表达式集合的代理表达式替换。为简单起见，每个规则表达式只能使用一个变量。运行示例3.9（示例模型M）(i) S {u}：：KaiC：：？X：：cyt S {p}：：KaiC：：？X：：cyt;？X={KaiC3，KaiBC}(ii) 3KaiC：：cyt惠KaiC3：：cyt惠替换了运行示例3.8作为带有变量的单个规则表达式这是最后的语法扩展。与原始模型（运行示例3.1）相比，生成的模型更简洁，可读性更强。4静态分析BCS语言提供了一些有趣的功能，为给定的模型提供了几种静态分析技术。这些技术基于定义的相容性运算符，该运算符为每种类型的代理制定合适的属性定义4.1（代理的排序）设x1，x2是两个任意代理。相容关系导出了主体x1和x2的偏序，记为x1≤x2，i ∈x1x2。记法4.2偏序≤的复个体X的论域是一个偏序集X ≤。相容算子定义了A、T和X集合上的偏序为我们目的，只有偏序集X是相关的。 原因在于，代理实际上封装了所有其他代理类型。然而，偏序的整个宇宙的复杂的代理是不是很有用，因为大多数的代理不能比较的兼容性操作。我们感兴趣的是特定的子集，每两个复杂的代理可以直接比较，或者存在一个代理与他们两个兼容。定义4.3（相容集）有限集X <$X是相容集，如果：(i) <$X1，X2∈ X<$Xj∈ X：X1XJ<$X2XJ，108M. Troják等人/理论计算机科学电子笔记350（2020）91X(ii) 且对于每个有限集XJ<$Xsuch，X<$XJ=<$x成立：<$X∈ X<$Xj∈XJ：（X）XJ<$XJX）。注4.4相容集X继承X≤的偏序，因为它是它的子集。相容集合X包含偏序的复杂主体，使得它们在主体名称方面都具有相同的序列。图2给出了兼容集的示例。图二.一个兼容集的例子。该集合由cyt隔室中的复合物形成，其序列中仅具有一个结构剂K。结构剂K在其部分