形式化方法进行模型选择在动力系统领域的应用与评价

可在www.sciencedirect.com在线获取理论计算机科学电子笔记350（2020）57-71www.elsevier.com/locate/entcs用形式化方法进行模型选择Matej Hajnal1 and Samuel Pastva2，3捷克布尔诺马萨里克大学信息学院摘要我们解决的问题，选择一个模型从列表中的潜在模型在动力系统领域。选择基于时序逻辑而不是时间序列中指定的模型行为。这为系统动态提供了更多的全局约束。 不仅要选择一种模式，创建一个有序的结构，我们提出了模型排序问题。我们建议并应用几个排序关系比较模型给定的属性规格。为了提供一个正式的方法与全球的结果，我们采用和适应模型检查和参数合成方法。 评价的方法，我们将所提出的方法应用到几个监管网络的定性模型关键词：模型检验，参数综合，模型选择，FFL1引言试图揭示潜在生物机制的模型在复杂性、规模和数量上都在增加因此，回答哪个模型更好地代表感兴趣的系统的问题成为一项具有挑战性的任务，因为模型通常是不完整的（仅描述系统的一部分），异构的（在物质或性质上不同）或相互不一致的（在网络或演绎假设中矛盾）。为了解决这个问题，通常使用两种方法：模型鉴别，排除不合适的模型;和模型选择，选择最有潜力的模型的对应方法。结果模型作为一个完美的候选列表，供进一步使用，预测和湿实验室实验测试，完成标准工作流程的全周期。减少潜在模型的集合节省了实验生物学家的宝贵时间和成本在1电子邮件地址：xhajnal@fi.muni.cz2电子邮件：xpastva@fi.muni.cz3这 项 工 作 得 到 了 捷 克 科 学 基 金 会 资 助 号 18- 00178 S 和 捷 克 国家基 础 设施资 助 号LM 2015055 的 支 持 。Theauthorsa cn oL ocPaule v′e e tal. 为了完成一个使用过的库- minibn 。https://doi.org/10.1016/j.entcs.2020.06.0041571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。58M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57因此，可以更快和更便宜地实现对系统的正确理解和发现可能的改变，以便治愈不期望的行为。在这项工作中，我们提出了模型排序，一种能够通过创建模型的有序结构来解决区分和选择的方法。此外，我们提出了一种方法模型排序比较行为方面的模型，因为它是最有价值的资源，了解生物机制。与模型选择的标准方法[17，18，11]相比，系统行为是使用时序逻辑的属性来指定的，与时间序列数据相比，允许更一般的分类。只要特定逻辑能够提供关于系统行为的充分推理和足够有效的参数综合程序，那么特定逻辑的选择并不严格在这项工作中，我们采用计算树逻辑（CTL）-为了验证模型的行为和估计满意的参数，我们采用模型检测技术，侧重于参数合成。模型检查技术提供了全局保证和时间无界结果，克服了近似、采样[9]和模拟方法的局限性。为了计算模型集合上的排序，基于模型排序关系的给定指定来比较模型对。我们提出了几种关系选项，包括适合分为两组的定性测量和定量鲁棒性测量[16]。在这项工作中，我们专注于模型的一个元素例如，可以通过满足参数空间的体积或比例来比较模型类似的排序可以应用于状态空间。模型排序关系适用于任何类别的规范和建模形式主义，强调了该方法的通用性。我们通过将模型排序应用于具有已知行为[1]-所需的排序，各自的网络结构的质量 的 评 估 ， 与 现 实 生 活 中 的 发 病 率 进 行 比 较 。 为 保 证 重 现 性 ， 分 析 可 在www.example.com上http://biodivine.fi.muni.cz/paper/SASB2018/FFLs。html或在http://biodivine.fi.muni.cz/paper/SASB 2018/FFLs.ipynb 上 编 辑 并 作 为jupyter notebook运行。总之，模型排序是一种适用于许多模型形式、规范形式和分析框架的方法。我们相信这种方法可以大大简化模型推理工作，同时提供了一个可靠的方法来评估模型的形式主义。我们热衷于扩大所提出的方法的可用性，因为它的重现性。2预赛为了区分、选择或排序一组模型M，基于规格S来比较模型。为了在给定模型上创建有序结构，使用比较一对模型的关系M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57592.1模型序关系设M是一组模型，S是一个特例。模型序关系≤S是M上自反传递的二元关系4.如果一个二元关系也是自反的和传递的，那么它是一个预序。如果一个预序关系也是反对称的，那么它是偏序的。偏序允许创建格的可能性。例2.1考虑两个任意模型--M1和M2. 设specification，#var，表示模型的变量数设≤#var，是一个模型序关系，它偏好具有更多变量的模型-M1 ≤ # var M2 i <$M2至少具有与M1一样多的变量。2.2问题定义我们考虑以下三个问题，根据模型排序的结果定义模型选择和• 模型排序问题如下：给定一组任意模型M，一个指定S，以及一个模型排序关系≤S，关于≤S对模型进行排序。• 模型选择问题：给定按≤S排序的模型，选择关于≤S的最大模型。• 模型判别问题：给定按≤S排序的模型，排除低于阈值的模型-排序关系中的由于我们关注的是采用模型检查技术使用时间属性进行行为比较，因此在以下小节中讨论了适用于所提出方法的模型类型、规格和排序关系。2.3建模形式为了利用模型检查方法的优点，模型由转换系统（TS）表示为了达到这一目的，布尔网、Petri网和托马斯网等离散动态系统的形式化都可以通过生成状态转移图来表示。对于连续模型，状态空间的有限离散抽象是必要的。例如，一类重要的ODE（普通微分方程）模型可以通过矩形抽象来离散化[4]。抽象的主要缺点是，它通常会导致过近似或欠近似（或4可能对的子集60M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57∈两者的混合）的原系统的动力学。表示动态系统并采用模型检查的标准TS是Kripke结构。定义2.2给定AP，一组原子命题，Kripke结构是元组K=（S，S0，→，L），其中• S是状态的有限集合，• S0是一组初始状态，• →S×S是一个过渡关系，• L：S→2AP是一个标记函数。观察真实系统是一项具有挑战性的任务，通常包含不确定性– 例如其动力学。这种不确定性在模型中由一个参数表示，该参数可以通过参数化Kripke结构应用于转换图[3]。定义2.3给定AP，一组原子命题，参数化Kripke结构是元组K=（S，S0，P，→，L），其中• S是状态的有限集合，• S0是一组初始状态，• P是参数化的有限集合，• →S×P×S是一个过渡关系，• L：S→2AP是一个标记函数。固定参数化p P将参数化Kripke结构K简化为p标准（非参数化）Kripke结构Kp=（S，→，L）。这项工作假设每个参数化都是作为模型参数的估值给出的，因此每个参数都是使用参数索引来识别的。该指数在所有考虑的模型中唯一识别参数这些指数是用罗马数字写的。在例3.1中，我们考虑了三个模型，三个参数分别为I、II和III。这里，第一个模型只包含参数I和III，第二个模型包含参数I和II，第三个模型包含参数II和III。2.4质量标准在这项工作中，我们比较模型的基础上，他们的行为使用时间属性。为了表达系统动力学的性质，我们考虑由以下抽象语法定义的计算树逻辑（CTL）[8]公式：：：= Q |¬ϕ |ϕ1∧ ϕ2|AX系列|EX-2000|A（101U 102）|E（1U），其中Q的范围是从集合AP中获取的原子命题。标准缩写EF代表E（真U），AG表示<$EF<$。一些典型的CTL公式的例子是[10]：M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）5761• 表示条件成立的状态的可达性• AG_n表示稳定，其中_n持续为真，• EFAG<$1和EFAG<$2表示一个开关（可以达到两个不同的稳定状态<$1和<$2为了比较模型的性质，我们首先必须确定哪些模型满足该性质。 在参数化模型的情况下，也要从参数空间中找到最大集合，该属性对其保持。形式上，Kripke结构的模型检测问题如下：给定参数化的Kripke结构K和时态属性k，检查K是否满足属性-K| = 0。 参数综合则是指一个问题：给定参数化Kripke结构K和时间性质为了计算出令人满意的参数空间，好的 在CTL支持的情况下，Synth（K，n）={p∈P|s0∈S0s.t.Kp，s0|{\ f n黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.注2.4在本文中，我们考虑模型排序问题的一个特殊变体：给定一组参数化的Kripke结构，K，CTL公式和模型排序关系≤ <$，关于≤<$对模型进行排序。3方法在这一节中，我们提出了一种方法，用于参数化Kripke结构的时序特性和排序关系的模型排序 作为输入，我们的方法假设由参数化Kripke结构K ={Km=（Sm，Im，Pm，→m，Lm）表示的模型的有限集合。|m∈{1. n}}和一个属性。然后通过参数合成过程分析这些结构，该过程返回每个c h结构Km的满意参数子空间P′m。 最后，应用选定的排序关系≤k，以便比较关于参数合成结果的模型，参见图1。在第5节中讨论了所提出的方法的变化和扩展。3.1质量标准如第2.4节所介绍的，我们使用CTL[8]，计算吸引力的时间逻辑充分描述了真实动力系统的非确定性行为。此外，有大量的工具为CTL提供模型检查和参数合成[7，13，6，2]。然而，选择特定逻辑并不严格，只要它提供了关于系统行为的充分推理和足够有效的参数综合过程。62M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57ϕϕ模型排序法参数合成模型Kripke结构Kripke结构Model 3Kripke结构模型2财产Kripke结构有序结构序关系模型1Fig. 1.方法的工作流程。输入模型由参数化Kripke结构（虚线）表示。运行特性曲线的参数合成。给定序关系≤n，结构是有序的。3.2流量计的订购根据给定的规格将模型相互比较的内在方法是对它们进行排序。在这项工作中，我们提供了几个选项的模型排序关系给定规格的形式CTL公式，，在模型表示的Kripke结构，K≤KJ，这意味着KJ尊重至少一样好的K。所提出的排序考虑了时间特性，集中在满足单个结构– 好的3.2.1模型鉴别模式识别只需要定性比较。我们给出了以下模型排序，通过满足给定标准来分离模型。采用这种划分的排序产生两个等价类。(i) 模型满足以下性质：Km|= 0。这种幼稚的标准是行为歧视的基石。如果模型不满足该属性，则将其简单地排除。随着参数化的引入，需要更具体的表示。(ii) 这是一个参数化：P？m？让我们说我们观察一个系统的一个属性因此，系统必须包含满足该属性的参数化。系统的模型必须满足至少一个参数化的这个属性。因此，没有任何参数化的模型，满足λ是不合适的。(iii) 对于所有参数化：P<$m=P m。假设我们观察到一个性质，它是系统的一个必要条件。系统的模型必须满足每个参数化的这个属性因此，任何参数化不满足最小值的模型都是不合适的。M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）5763ϕϕϕϕϕϕϕϕϕϕϕϕϕϕ3.2.2型号选择。在这里，我们提供了几个定量的模型排序关系划分模型到更多的组适合模型选择。基于属性或模型，一个模型排序关系可能比另一个更合适。在本节中，我们提出了关注各个模型的参数空间的模型排序关系，而类似的排序可以应用于模型的状态空间或结构属性。模型主要通过满足参数空间的体积或比例进行比较。然而，不同的模型通常包含不同的参数，这使得比较具有挑战性。为了比较这样的参数空间，我们建议使用投影πcom将参数化限制为所有模型中共有的参数。这个函数接受一个任意的集合并将每个参数化限制为公共参数。或者，也可以对两个模型Km;Km′∈ K进行成对投影-π com（m，m ′）. 注意，在模型之间的非平凡关系的情况下，参数，可能需要更复杂的过程来有意义地统一参数。提供的订单列表不完整。对于特定的应用，可以提出新的、更合适的排序。比较各个模型排序关系的适用性是一个困难的任务，我们计划在我们未来的工作中解决。(i) 符合要求的常用参数数量Km≤1Km′惠|πco m（P<$m）| ≤|πco m（P<$m′）|.具有更令人满意的参数化的模型提供更高的鲁棒性，意味着该性质对于更多的参数扰动成立。(ii) 满足参数化是公共参数的子集：Km≤2Km′惠πco m（P<$m）惠πco m（P<$m′）。≤2是≤ 1 -Km ≤ 2 Km ′ <$Km ≤ 1 Km ′的更严格版本。它还提供与前面的排序≤1类似的鲁棒性概念。 令人满意的是，较大结构的参数化集合还包含较小结构的所有参数化，这意味着该属性对于至少同样多的参数扰动成立成对公共参数不能用于创建订单，因为排序关系不会传递-参见下面的例3.1关于模型序≤1和≤2的变分的传递性的反例，其中两两公共参数在以下三个上ϕ ϕ模型（图2）：Km≤1′Km′惠|πcom（m，m′）（P<$m）| ≤|πcom（m，m′）（P<$m′）|.不传递：K1和K2的两两公共满足空间是1参数化-（1），对于两个模型，因此（K1，K2）是相关的。在K2和K3的情况下，它是参数化（2），因此（K1，K2）也是相关的。但（K1，K3）不存在这种关系，因为（K1，K3）的公共参数空间64M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57ϕϕϕϕϕϕϕϕϕϕpϕpR¯K（一、三）第1页ϕ{p1=（1，4），K（一、二）第二阶段ϕ{p1=（1，K（二、三）第3页ϕ{p1=（2，K（一、二）第1页ϕ{p1=（1，2），K（二）第二阶段ϕ{p1=（2）}（K1，K3）在K1的情况下由两个参数化（4）;（5）组成，而在K3-（3）的情况下只有一个参数化。不是反对称的：（K1，K2）是相关的，但也是（K2，K1）和K1/=K2。Km≤2′Km′惠πcom（m，m′）（P<$m）惠πcom（m，m′）（P<$m′）不传递：（K1，K2）和（K2，K3）是相关的，但（K1，K3）是没有不是反对称的：（K1，K2）是相关的，但也是（K2，K1）和K1/=K2。图二、三种模型的满意参数子空间。P<$m表示模型的满足参数空间M. pi指示参数空间中的参数化，并且k指示相应参数的索引– 具有相同索引的参数是常见的。(iii) 令人满意的参数化数量：Km≤3Km′惠|彭| ≤|普米|.类似地，如在≤1中，具有更令人满意的参数化的模型提供更高的鲁棒性意味着该属性对于每个更多的参数保持不变，扰动由于≤3不适用于公共参数，因此在模型参数不均匀，排序可能不公平（图3）。图三.满足两个模型K1，K2的参数子空间和一个性质.根据满足的参数化个数K1≤3K2.这仅仅是因为第一个模型的参数空间包含维度I和两个额外的令人满意的元素。(iv) 满意度：Km≤4Km′R惠sd（Km，） ≤sd（Km′，λ）， 其中，sd（Kp，k））是满意度”[9]这句话的意思是：满意度通过描述模型如何很好地保持给定参数化的属性来模仿评价函数D[12]。 该选项可以扩展到整个参数空间-例如，通过参数空间的最小或平均满意度(v) 满意参数化的比例Km≤5Km′惠R（Km，λ）≤ R（Km′，λ），其中R（K，λ）= |P|.ϕ|P|M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）5765≤Kϕ具有更大比例的满意状态空间的模型提供更高的全局鲁棒性，其中结果由整个参数空间的体积而不是[11]中的参数数量进行归一化。标准化还使得能够针对不同维度进行比较。(vi) 最小参数化扰动m6m′普尔惠R（Km，p，n） ≤R（Km′，r，n）， 其中R（K，p，n）=min（{dist（p，pJ）|pJ∈P∈K<$Kp′ $<$}）。与不满足的参数空间具有更大（最小）距离的参数化提供更高的局部鲁棒性。此外，该选项可以扩展到整个参数空间-例如，通过最小或平均距离参数空间 注意，在≤4中，是在状态空间这里是参数空间。所提出的模型序关系不是反对称的，因此不创建偏序集。这是因为两个模型可以通过排序关系来实现相同的特性，例如，一组令人满意的参数化，同时具有不同的过渡系统。偏序集可以通过合并等价模型得到。4为例为了检验该方法的适用性，我们将模型排序应用于具有已知行为的模型[1]-有13种可能的方式来连接三个节点与有向边。FFL是13种可能的三节点模式中唯一的网络基序。从FFL基序的八个符号组合（如图4所示）中，只有两个是重要的。在相干群的情况下，它是类型1 - C1-FFL。对于非相干群，它也是1 - I1-FFL型。其他六种FFL类型似乎比C1-FFL和I1-FLL出现的频率要低得多。[1]为了理解这两种类型的优势，我们研究了[1]中研究的蛋白质Z的两个动力学性质：• 信号敏感延迟。蛋白Z在开启信号时激活有延迟，但在开启信号时没有延迟，反之亦然。• 脉冲发生器。在脉冲中，Z电平首先上升，然后下降到低电平。为了评估竞争FFL类型的质量，计算每个属性的排序。结果排序与现实生活中的发病率进行了比较。4.1模型和时间属性首先，我们展示了布尔网络模型的方法每个模型包含五个变量8个FFL子类型中的每一个都是用两个连接两个规则的K66M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57DE类型1类型2类型3类型4相干非相干见图4。前馈环路的八种符号组合（类型）。 连贯组具有与直接路径整体符号相同的间接路径，而不连贯组具有与直接路径整体符号相反的间接路径，箭头符号表示激活，符号表示抑制。蛋白质Z和/或，创建了16个模型。其次，我们使用多值网络模型，这些模型分别用多值蛋白质X和蛋白质Y和Z，xy和xz的调节阈值进行增强，创建了48个模型。5为了评价该方法，我们将[1]的结果与我们的方法的结果进行了在分析中，我们使用[5]进行模型检查，以逐个合成以下三个属性的参数（图5中的相应行为示例）：仅在接通时发生的延迟是两个特性的结合：s0=（sx = 1，sy = 1，X = 0，Y = 0，Z = 0），延迟开启=A（Z= 0UY = 1）无延迟o AF =AF（sx=0sy= 1Z =1Y= 1）EX（Y= 0））=EX（Y=0Z= 0））- 从初始状态s0开始的延迟，其表示在信号出现之后接通蛋白质Z的延迟，并且没有延迟o-接通蛋白质Z的s0=（sx = 0，sy = 1，X = 1，Y = 1，Z = 1），delay o =A（z= 1Uy = 0）无延迟开启=AF（sx =1sy= 1Z = 0Y = 0）EX（Y= 1））=EX（Y= 1Z= 1））仅发生在开关o的延迟是两个性质的结合：从初始状态s0开始的延迟o，其表示在信号消失后打开蛋白质Z的延迟，以及没有打开延迟我们考虑3种情况，xy xz，xy > xz，xy=xzM. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）5767图五.蛋白质Z符号敏感延迟的两种行为的示例，延迟打开（左）和无延迟打开（中）以及脉冲发生器（右）。T_ON表示延迟的长度，k_yz表示调节Z的浓度Y的阈值。和C1C2C3C4I1I2I3I4xy=xz133313XYXZ<13331,2xy> xz133313或C1C2C3C4I1I2I3I4xy=xz2332XYXZ<232,32xy> xz2332见图6。枚举相应逻辑的多值模型的满足属性s0=（sx= 1，sy = 1，X = 0，Y = 0，Z = 0），峰gen =AF（Z= 1<$AF（AGZ=0））脉冲发生器用峰值产生特性表示。4.2结果前面的分析[1]揭示了C1-AND类型满足第一个属性，C1-OR满足第二个属性，I1-AND满足第三个属性。我们的分析揭示了BN模型的以下结果• 在第一个属性的情况下，只有C1-AND和I3-AND子类型的属性才有效。• 第二个属性适用于C1-OR和I3-OR子类型。• 最后一个属性适用于I1-AND、C3 both、I4-AND、C2-OR和I2- AND。此外，我们还利用相同的性质分析了多值网络68M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57和初始状态，结果如图6所示。 结果符合要求 分析总结在[1]中，因为所有三个研究的模型都表现出各自的性质。同样在第三性质的情况下，可以容易地区分模型I2-AND和I4-AND，因为蛋白质Z的稳定状态对蛋白质Y-sy上的信号不敏感通过静态分析验证了这一特性。然而，也可以将其表示为时间属性。由于剩余的模型满足给定的属性，它们可以作为进一步研究的候选模型利用这些结果，我们可以很容易地区分和选择几个模型，例如，删除模型没有令人满意的参数化。此外，与其他模型相比，具有令人满意的参数化超集的模型可以被选择为更鲁棒的。由于所有模型共享相同的参数空间，因此可以使用满意结果的数量推导出相同的结论。由于我们模型的简单性质（小状态和参数空间），更高级的排序是徒劳的。要 查 看 案 例 研 究 分 析 和 结 果 ， 请 访 问 http://biodivine.fi.muni 。cz/paper/SASB2018/FFLs.html 。 该 分 析 也 可 以 在 www.example.com 上 以jupyter笔记本的形式获得http://biodivine.fi.muni.cz/paper/SASB2018/FFL.ipynb 。 笔 记 本 可 以 使 用CoLoMoTodocker编辑和运行[14]在https://hub.docker.com/r/colomoto/colomoto-docker/ 上 安 装 。 它 使 用 可 用 的python库来建模，编辑和分析网络- minibn，ginsim和biolqm。可执行笔记本的优点是模型是在计算机上创建的，因此可以很容易地编辑和调整分析也可以只选择其中的一部分来进行，而且整个工作流程包括结果都可以以统一的形式呈现。4.3使用的框架-Docker，Docker和CoLoMoTo-docker在分析中，我们使用了以下框架：Example yter（http://jupyter.org）提供了一个交互式Web界面，用于创建名为notebook的文档，其中包含代码、公式和格式化文本。笔记本通常描述分析的完整工作流程，包括文本解释以及再现结果的完整代码和参数。笔记本是一个单一的文件，可以很容易地修改，共享，重新执行，并在线可视化。Docker（https://www.docker.com/）是一种计算机软件，它执行操作系统级虚拟化，也称为容器化。容器是相互隔离的软件包，使用自己的工具和库;它们可以通过定义良好的通道进行通信。所有容器都由单个操作系统内核运行，因此比虚拟机更轻量级。CoLoMoTo-docker（https://hub.docker.com/r/colomoto/colomoto-docker/）是一个docker镜像，它提供了一个交互式的web，M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）5769使用Python的即时可用环境。 它包含旨在创建、编辑、模拟和分析逻辑网络的库。它是几个逻辑建模软件工具的联合发行版，简化了互补分析的链接。[第十五条]5讨论我们已经提出了模型排序作为比较模型的一般概念。在这项工作中，我们倾向于行为比较静态属性和系统属性的数据。在本节中，我们将讨论三个层次上不同的方面5.1当前方法的增强和扩展该方法的计算瓶颈是由于状态空间爆炸的模型检查和参数综合过程。此外，必须为每个模型计算过渡系统。我们提出了一种方法来减少这种计算时间。• 由于模型在状态空间和参数空间上通常非常相似，因此通过计算一个联合参数化转移图可以优化单个模型的状态转移图的计算• 在某些情况下，使用符号数据结构可以大大减少转换系统的大小。• 并行计算-本文提出的实施重点是布尔和多值网络和CTL中给出的属性。下一个自然的步骤将是扩展可能的应用程序与新的：• 建模形式主义，如Petri网或普通微分方程;• 时间逻辑，如LTL或STL;• 使用更复杂的参数统一或特定于域的属性来建模排序关系。5.2使用时间属性的方法的变体• 当呈现多个属性时，可以使用不同的排序方法· 分别为每个属性应用选定的排序关系，并创建一个这些关系的交集。· 根据满意属性的数量对模型进行排序，可能会对属性进行优先级排序或加权。70M. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）57·在单独的模型排序上应用新的特定排序关系。• 模型的排序关系集中在状态空间，而不是参数空间。5.3基于系统特性的其他方法存在用于基于系统的动态方面的模型选择/排序的方法，其不需要精确的时间属性，因此不需要与系统的变量绑定。其中一种方法使用动力学的一般属性，第二种方法将动力学与其他系统进行比较，而不是属性本身。• 一般行为特性· 吸引子/稳定状态的数量等。· 振荡、平台、峰值产生、活性等。• 系统等同性· 互模拟· 拓扑等价（轨道上的· 同构（Isomorphism）6结论为了揭示生物机制，我们提出了模型排序方法，以减少候选模型的集合。在2.2节中，我们从三个问题的问题定义开始--模型判别、选择和排序。此外，在第三节中提出了一种基于行为比较的模型排序方法，重点关注满意的参数空间。第3.2节提供了与给定规范相关的订购关系列表。基于此结果，可以选择最大模型。最后，该方法被应用到一个案例研究的FFL图案与已知的行为使用布尔和多值网络的作品在第4节。所获得的排序与现实生活中的发病率进行比较。整个分析可使用CoLoMoTo交互式笔记本[15]复制。我们讨论了第5节中方法的可能扩展、调整和变化，我们将从以下方面着手• 通过使用参数化模型和包括多个模型的结构来优化该方法• 通过添加其他时态逻辑来扩展符合条件的规范。• 扩展、分析和创建方法来计算可用的排序关系。• 作为最重要的部分，我们将研究该方法的适用性引用[1] 阿隆大学，“An Introduction to Systems Biology: Design Principles of Biological Circuits,” ChapmanM. Hajnal，S.Pastva/理论计算机科学电子笔记350（2020）5771[2] 本 · 埃克斯， N. ， L. Brim ， M.Dem ko ， S.Pastva 和 D.Safranek ， Pithya ： Apar alleltoolforparalsynthesisofpiecewisemulti-a-n-dichroic systems ， in ： R. 我 是 一 个 巨 人 和 V 。 Ku nKubercak， editors ， CAV2017，LNCS 10426（2017），pp. 591-598.[3] 布里姆湖M. Dem ko，M. Ce s ka，S. Pastva和D. Safranek，基于并行计算的CTL模型检测的并行综合，在：O. Roux和J. Bourdon，编辑，CMSB 2015，LNBI9308（2015），第100页。251- 263。[4] 布里姆湖M. Dem ko，S. Pastva和D. Safranek，Pie-ewise-a-dynamic系统的高性能圆盘迭代分析，在：A.Abate和D. Safranek，editors，HybridSystemsBiol ogy2015，LNBI 9271（2015），pp. 58比74[5] Cimatti，A.， E. Clarke，E. Giunchiglia，F. Giunchiglia，M. Pistore，M. 罗韦里河 阿扎尼亚尼和A. Tacchella，NuSMV版本2：用于符号模型检查的开源工具，在：Proc. International Conference onComputer-Aided Verification（CAV），LNCS2404（2002）。[6] Cimatti，A.，E. Clarke，F.Giunchiglia和M.Roveri，Nusmv：一个新的符号模型验证器，在：计算机辅助验证国际会议，Springer，1999，pp。495-499[7] Clarke ， E. M. 和 E. A. Emerson ， Design and synthesis of synchronization skeletons using branchingtime temporal logic，in：Workshop on Logic of Programs，Springer，1981，pp. 52-71.[8] Clarke，E. M.，E. A. Emerson和A. P. Sistla，使用时序逻辑规范，ACM Trans.程序. 浪系统8（1986），pp.244-263。[9] Fages ， F. 和 A. Rizk ， From model-checking to temporal logic constraint solving ， in ： InternationalConference on Principles and Practice of Constraint Programming，Springer，2009，pp.319-334[10] Fages，F.和S. Soliman，Formal cell biology in biocham，in：SFM，LNCS5016（2008），pp. 54比80[11] Hafner，M.，H. Koeppl，M. Hasler和A. Wagner，e1000534。[12] Kitano，H.，Towards a theory of biological robustness，Molecular systems biology3（2007），p. 137.[13] McMillan，K. L.，Symbolic Model Checking，in：Symbolic Model Checking，Springer，1993. 25比60[14] Naldi，A.，C. Hernandez，N.Levy，G.斯托尔山口T. 蒙泰罗角Chaouiya，T.Helikar，A.季诺维耶夫，L. Calzone，S. Cohen-Boulakia，D. ThieBerryandL. Paulev′e，Co LoMo ToInte ractiveNote book：定性生物网络的可解释性和可再现性计算分析，bioRxiv（2018）。[15] Naldi，A.， P. T. Mo nteiro，C. Müssel角 用于逻辑模型、T〇ols、H. A. Kestler，D. 蒂耶雷岛Xenarios，J. Saez-Rodriguez，T. Helikar和C. Chaouiya，与colomoto合作开发逻辑建模标准和工具，生物信息学31（2015），pp. 1154-1159.[16] Rizk， A.， G. Batt，F. Fages和S. Soliman ，A general computational method for robustness analysiswith applications to synthetic gene networks，Bioinformatics25（2009）.[17] Silk，D.，P. D.柯克角P. Barnes，T.托尼和M. P. Stumpf，系统生物学中的模型选择取决于实验设计，PLoS计算生物学10（2014），p.e1003650。[18] Toni ， T. 和 M. P. Stumpf ， 基 于 模 拟 的 模 型 选 择 系 统 和 种 群 生 物 学 中 的 动 态 系 统 ， 生 物 信 息 学 26（2009），pp. 104-110