大规模生物动力学模型的可达性分析方法的新发展 - 来自www.sciencedirect.com

可在www.sciencedirect.com在线获取理论计算机科学电子笔记350（2020）139-158www.elsevier.com/locate/entcs可达性问题的静态分析与随机搜索Xinwei Chai，Tony Ribeiro，Morgan Magnin，Olivier Roux1，2Laboratoire desSciencesduNum'eriquedeNantes1RuedelaNoé，44300Nantes，FRance井上胜美3国立信息学邮编101-8430东京都千代田区一桥2-1-2摘要本文主要研究大规模生物动力学模型可达性分析的一个重要改进。 为了处理这样的模型，经典的模型检查器由于状态空间爆炸而失败由详尽的搜索引导。 已经提出了替代的静态分析方法，但它们也可能失败在某些情况下，由于非穷举搜索。在本文中，我们介绍了一种混合方法ASPReach，它结合了静态分析和随机搜索，打破了这两种方法的限制。我们在我们最近引入的建模框架上解决了这个问题，异步二进制自动机网络（ABAN）。我们表明，ASPReach能够有效地分析一些现有方法无法解决的可达性属性。我们还研究了生物学文献中的各种案例，强调了我们的方法在结论性和性能方面关键词：模型检测，可达性问题，异步二进制自动机网络，局部因果图，启发式，答案集编程。1介绍随着新技术提供的可用数据数量的增加，例如DNA微阵列[22]，对表达建模及其相关的高性能分析工具的需求日益增长。其中，并发系统的工作已经在系统生物学的兴趣超过十年[4，5，35]。如果模型验证是一个主要问题，那么现在的主要挑战之一就是预测这些系统的行为。1由国家留学基金管理委员会资助2电子邮件：{xinwei.chai，tony.ribeiro，morgan.magnin，olivier.roux}@ ls2n.fr3电子邮件：inoue@nii.ac.jphttps://doi.org/10.1016/j.entcs.2020.06.0081571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。140X. Chai等人/理论计算机科学电子笔记350（2020）139形式模型的可达性问题是一个关键的挑战，其中验证问题（模型是否满足先验知识）和预测问题（待发现的属性）都从形式化的观点看，计算模型中的大量生物学性质可以转化为可达性性质。例如，a的状态0/1的可达性可以表示某些基因的激活/抑制或蛋白质的合成，而初始状态可以表示实验中的初始观察。如果某一状态的可达性与先验知识相矛盾，则可以修改模型和/或设计新的实验来验证先验知识或先前观察是否存在错误。此外，可达性分析有助于药物设计：例如，如果想要防止细胞（目标状态）的致癌，一种可能的解决方案是找到通往目标状态的关键途径，并设计一种药物来切断它们，以保持细胞健康。在模型检测领域，可达性已经引起了30多年的极大兴趣[10，11]。生物信息学中的各种建模框架和语义已被研究：布尔网络[2]，Petri网[23，14]，时间自动机[12，36]。这些方法依赖于全局搜索，因此面临状态爆炸问题，因为状态空间随变量的数量呈指数增长。在[28]中，已经证明了Petri网的可达性问题是指数时间困难和指数空间困难的，即使在某些特定条件下，这个结论也不会改变[14]。对于1-安全Petri网，可达性分析的复杂性通常是PSPACE-完全的[8]。Li et al.[20，21]从理论上研究了切换布尔网络的稳定性，可控性和可达性，但他们的方法仍然计算昂贵;Saadatpour et al. [30]只研究固定点的可达性。为了解决复杂性问题，基于有序二元决策图（OBDDs）和SAT求解器（满意度）的符号模型检查[6]已经研究了多年，但仍然无法分析具有超过1000个变量的大型生物系统。有界模型检验（BMC）[9]是一种有效的方法，但通常不完整，因为其搜索深度限于给定的整数k。除了这些方法之外，抽象是处理大规模模型的有效策略。它的目的是近似的模型，同时保持最重要的部分，以确保可达性。抽象方法通常具有更好的时间记忆性能，但会丢失信息。它们通常解决原始模型的简化版本，即这些方法的结果不一定与原始模型的所有属性兼容。在研究可达性问题时，将系统动力学抽象为状态和变迁之间的静态因果关系。我们设计了一个新的并发系统离散建模框架[7]：异步二进制自动机网络（ABAN）。在ABAN中，我们应用了由Paule v'e等人开发的方法。 [25，15，26]到一个dressrea chabili typrob-lem.这种方法是指可达性的静态抽象（具有真实动态的过近似和欠近似它基于一个抽象的解释：局部因果图（LCG）。这一解释的戏剧性-X. Chai等人/理论计算机科学电子笔记350（2020）139141cally减少了搜索状态空间，从而避免了昂贵的全局搜索[27]。然而，这种纯静态的分析是不完整的，因为存在着无法确定可达与否的不确定情况。许多生物网络以布尔风格编码，例如[2，18]，因为BN是一种简单的形式主义，但具有很强的适用性：BN中的离散化是处理模型上先验知识不精确的一种方法。然而，国阵可能表达不够。关于动态行为的建模在时刻t+ 1如果在时刻t“ba总是跟随b的演变，但具有潜在的不希望的行为ABAN将这种动态建模为通过{b1}→a1，而没有这种冗余。此外，BN可转化为ABAN，这一性质使我们的方法适用于更广泛的领域（附录A）。我们的工作有类似的关注，但我们结合静态分析和有界模型检查。我们已经开发了一种启发式方法PermReach来攻击可达性问题[7]，该方法比纯静态分析更有结论性，但耗时，并且在某些条件下仍然无法解决可达性问题在本文中，我们提出了一种混合方法ASPReach的基础上，以前的LCG推理和非穷举搜索的LCG获得更确凿的解决方案的可达性问题。ASPReach允许解决其他静态方法失败的情况。 此外，它还可以解决一组状态的可达性，据我们所知，这在静态方式中从未做过。 我们评估我们的贡献的价值使用基准生物学的例子从文献。本文的组织如下：第2节介绍了正式的背景和必要的工作的理解形式化;第3节提出了具体的方法和算法组成的整个方法;第4节显示的基准评估我们的方法和其他替代品;第5节总结本文。2形式化符号：ai表示自动机a取值i;x：：y是实体x和y的顺序连接符，其中x刚好出现在y;a.next是a的直接继承者;a.pred是的直接前身a.布尔网络是一种传统而有效的建模框架，BN中编码的生物网络[18]。为了更精确地描述动力学性质，引入了自动机网络[7，29]。它可以被认为是通信有限状态机或安全Petri网的子集。异步二进制自动机网络（ABAN）是自动机网络的一个特例。“Asynchronous”implies the update scheme that no more than one au- tomaton 异步更新方案使142X. Chai等人/理论计算机科学电子笔记350（2020）139生物现实和复杂性之间的权衡。从一个给定的状态，生物系统可以进化到多个未来的状态（例如细胞分化），但它 是昂贵的，以模拟广义AN的任意子集的自动机可以同时更新。“Binary” implies that every automaton has exactly two possible 在附录A中，我们展示了如何将布尔网络转换为ABAN。定义2.1[ABAN] ABAN是一个三元组AB=（λ，L，T），其中：• {a，b，.. . }是自动机的有限集合，每个组件都有一个布尔状态;• LSa∈N{a0，a1}是所有局部状态的集合，La∈×N′{a0，a1}是连接状态的集合，其中N J∈ N.特别地，如果J=，则L是全局状态的集合。• T{A→bi|b∈A∈L}是转移的集合，其中A（称为head）是转移tr=A→bi所需的状态的集合，其中所 有 的 路径都 是 从 b1−i 到 bi （称为 b ody ） 。 在 其他文 字 中 ，transitiontr被称为可触发的i/s，其中s是当前的全局状态。局部状态表示一个自动机的状态，例如a1，而全局状态表示网络中所有自动机的联合状态，例如a0，b1，c0，其中L={a，b，c}。定义2.2 [异步动力学]从当前全局状态s出发，触发转换tr=A→bi之后的全局状态记为s·tr=s\{b1−i}<${bi}，其中eb1−i∈s。某个自动机a的状态记为（s·t r）[a]。具体地，如果不存在可触发的转变，则下一状态保持与当前状态相同。为了描述ABAN中的演化，我们使用轨迹的概念定义2.3[轨迹]给定一个ABANAB =（λ，L，T）和一个全局初始状态α∈L，从α出发的轨迹t是一个转移序列t=tr1：：···：：tri：：···：：tr n，其中tr i∈T，并且每个tr i在（s·tr1·... ·tri−1）。从α开始，触发t的所有转换后的全局状态是（s·tr1·. ·trn），表示为s·t。定义2.4[状态序列]给定一个ABANAB =（λ，L，T）和一个全局初始状态α∈L和轨迹t，状态序列seq=s1：：···：：si：：··：：sn，其中si∈LS由轨迹t期间更新的局部状态形成。例2.5Fig. 图1示出了初始状态α=a0，b0，c0，d0，e0的ABAN，并且可能的轨迹是t={d0} →b1：：{b1} →d1：：{d1} →c1：：{b1，c1} →a1。在触发轨迹t中的转换之后，状态变为Ω =s·t=a1，b1，c1，d1，e0，并且ω=a1=（α·t）[a]。状态序列为seq=b1：：d1：：c1：：a1。对于可达性问题，给定一个ABANAB =（α，L，T），将联合可达性REACH（α，Ω）形式化为：如果存在一条轨迹ts.t.α·t= Ω。类似地定义部分可达到达（α，ω）：局部状态ω=ai是可达的i如果存在轨迹ts. t。（α·t）[a] =ai. REACH（α，Ω）和reach（α，ω）取布尔值True、False或InconclusiveX. Chai等人/理论计算机科学电子笔记350（2020）13914310Fig. 1. 以ABAN如果不能决定。图1，Ω =ωa1，b1，c1，d1，e0或ω=a1是从初始状态α经由轨迹t可达的，即reach（a1）=True且REACH（α，Ω）=True。事实上，联合状态甚至全局状态的可达性等价于一个局部状态的可达性。给定一组目标状态{ai，.z j}，通过将新的自动机x添加到x1，将其初始状态设置为x0，并将转换{a i，. z j}→x1到T，REACH（α，{ai，. z j}）因此等价于reach（α，x1）。为了方便起见，本文研究了部分可达性。Paulev'eetal.[26]提出了局部因果图（LCG）来静态分析可达性问题。LCG通过一个过近似（必要条件）和一个欠近似（充分条件）对原问题进行抽象。这是一个非常有效的工具，因为没有全局搜索，所有的操作都是有界的多项式复杂度。然而LCG并不保证得到一个结果，即一些不确定的实例满足必要条件，而不满足充分条件。在本文中，我们利用LCG通过删除一些只需要在多值网络中的元素，然后我们试图更深入地分析它来解决不确定的情况下，二值系统。 事实上，Didier et al. 表明一种将多值网络转换为布尔网络的技术[13]，它为我们提供了多值情况的适用性定义2.6[LCG]给定一个ABANAB =（V，L，T），一个初始状态α和一个目标状 态 ω ， LCGl = （ Vstate ， Vsolution ， E ） 是 最 小 的 递 归 结 构 ， 其 中E<$（Vstate×Vsolution）<$（Vsolution×Vstate）满足：ω∈V态a i∈ V状态惠{（a i，sol ai）|a i∈α}<$E sol ai ∈ Vsolution惠{（sol ai，Va（sol ai）}<$E其中，V状态是局部状态的集合，V解是解的集合，Va是solai的所需局部状态的集合。例2.7图2显示了图1中用于分析到达（a1）的LCG。∅图二. LCG的可视化，正方形代表局部状态，小圆圈代表解决方案节点。 这意味着不需要连接一个ny转换，即前一个状态d0处于初始状态。算法1描述了如何从ABANAB =（A，L，T）构造LCG一B1 1{b1，c1}{e1}{d0}0 0C1{d1}0D1{b1}0ee1或的B1d0和C1D1144X. Chai等人/理论计算机科学电子笔记350（2020）139从一个给定的目标状态Ls=ω开始，我们可以找到所有到达ω的跃迁Ts<$T，并添加边ω→Ts。然后我们找到Ts的所有头A，并添加边Ts→A，并用A替换Ls（递归）。最后，我们更新结构，直到Ls<$α或在Ls中没有与体的跃迁。输入：一个ABANAB =（λ，L，T），一个初始状态α，一个目标状态ω输出：LCG1 =（V状态，V溶液，E）L：Ls<${ω}，V状态<$，V溶液<$，E<$而L.S.多Ls=Ls\V状态对于i∈Ls，Ls←Ls\{ai}如果ai∈α，则E←E{（ai，）}其他//选择到达i的转换，即体a1−i对于sol=A→a1−i∈TdoVsolution←V solution{sol}E<$E <${（ai，sol）}Vstate<$Vstate<$Aforbj∈AdoE←E<${（sol，bj）}Ls←Ls<$AVstate←V state触发器V solution ←Vsolutioni. 下return（Vstate，Vsolution，E）算法1. LCG的构建直觉上，当递归构造完成时，SLCG实际上是一个有向图，其状态节点为Vstate，解节点为Vsolution。E由局部状态节点和解节点之间的边组成。要访问某些局部状态，至少需要触发它的一个后继解（从解节点的相应转换）;要使一个解节点可触发，需要满足它的所有后继局部状态。可达性的递归推理从表示目标局部状态的状态节点开始，经过ai→solai→bj·· ·，并以初始状态（可能可达）或没有解后继的局部状态（不可达）结束利用LCG可以很容易地验证它们是否是从目标状态ω到初始状态α的潜在路径。如果不存在这样的路径，则可以确保ω不能从α到达。[27]这是一种逻辑推理。定义2.8[伪可达性]给定LCGl =（V状态，V解，E），X. Chai等人/理论计算机科学电子笔记350（2020）139145⎩J假如果v/∈α和/ε（s，sol）∈E如果v∈α，则True全局初始状态α，节点v∈V状态的伪可达性定义为⎪（1）A=（（sol，s）∈E到达J（α，s））否则然而，伪可达性被命名为它揭示了可达性的必要条件例2.9在图2.1中，3、reachJ（l，c1）=reachJ（l，a1）reachJ（l，b1）=reachJ（l，a0）reach（l，b0）=True。a1和b1都是可达的，但都无法到达同步在这样的LCG中，存在两个分支，一个1b0和b1A0，自动机a和b涉及不同的分支，a1的可达性阻碍B1的可达性，反之亦然。∅∅图3.第三章。T={a，b，c}，T={{b0} →a1，{a0} →b1，{a1，b1} →c1}， ω=c1而且，如果LCG中存在循环，则递归推理不会终止。在计算伪可达性时，自相关形式达到J（l，ai）=... =reachJ（l，ai）将出现。应对周期是不可避免的。定义2.10[循环]在LCG中，循环由如下连接的节点序列形成：ai→ b i →·· ·→ b i →ai为了识别圈，我们搜索大于1的强连通分量（SCC）。因为循环可能会交错，而SCC中没有这种问题。换句话说，一个SCC可以包含几个相互连接的嵌套循环。[33]显示SCC的检测可以在O（|V|+的|E|）时间，与|V|顶点的基数，|E|边的基数 LCG通常是一个稀疏图，因为在生物系统中，组件主要只与系统的一部分相互作用，因此可以认为出度为O（1），并且可以在O（|V|），即 线性时间定理2.11给定LCG中的循环x→ n →· · · → n →x，如果至多有一个进入循环的边缘，则可以去除循环。证据如果没有进入边沿，则目标状态y必须在循环中。可以移除边y.pred→ y →y，因为y.pred的可达性需要y，但是y是目标状态，其在图1中的其它局部状态之前从未被到达4Python 3实现https://github.com/alviano/python/blob/master/rewrite_aggregates/scc.py一1{b0}0BC1 1{a0}{a1，b1}0 0的1b0的C1和B1a0级reachJ（α，v）=146X. Chai等人/理论计算机科学电子笔记350（2020）139一XzyLCG已经到达。因此，对应于该边缘的过渡永远不会被触发，并且该边缘可以被移除。类似地，如果存在外部进入边缘a→ p →x，则a必须是目标状态y的后继者或目标本身，因此可以移除pred→ p →xQ···见图4。含圈x→ n →y→ n →z→ n →x的LCGl例2.12在图4中，a的伪可达性是reachJ（l，a）=reachJ（l，x）=reachJ（l，y）=reachJ（l，z）=reachJ（l，x）为了到达x，我们需要到达z，但是z不能依赖于x，因为x已经被到达了。 自相关出现：如果x是可达的，则x是可达的。 因此边z→ x →x被删除（虚线）。不幸的是，不是所有的圈都可以通过定理2.11去除。例2.13解释了这个问题。图五、x、y、z都有外部链接，因此没有一个链接可以被丢弃例2.13根据定理2.11，圈x→ n →y→ n →z→ n →x是不可破的，它有3条引入边。但是对于定理2.14，如果去掉或门，就可以处理这个循环。或门的移除将在下一节中说明。定理2.14给定一个循环，如果它不包含或门，则循环中的所有局部状态都不可达。是的 。当h → LCG中的一条边时，存在一个任意的 循环C =ai→···bj→···→ai.NtethatreachJ（α，ai）=reachJ（α，bj）=reachJ（α，bj.next）=r···=reachJ（α，ai）.根据reachJ的定义，reachJ（α，a）=True仅当<$ck∈C且ck∈α.如果存在这样的ck，那么C就不应该存在，因为推理止于ck，不形成循环、矛盾。达到J（α，ai）= r，每个J（α，bj）=·· ·=False。Q一XzWyX. Chai等人/理论计算机科学电子笔记350（2020）1391473ASPReach算法在本节中，我们介绍了本文的主要贡献，我们的分析器AS-PReach：一种用于检查给定ABAN中目标局部状态ω从全局初始状态α（也可以是部分）可达性的算法。然而，主动搜索导致大量的计算和巨大的内存需求。下面提出的算法试图通过将静态分析和随机搜索结合到下面的混合方法中来克服这些缺点。ASPReach：• 输入：ABANAB、初始状态α、目标状态ω和最大迭代次数k• 输出：reach（ω）∈ {False，True，Inconclusive}(i) 构造LCGl =LCG（AB，α，ω）(ii) 尝试删除所有周期和修剪无用的边缘从l(iii) 尝试使用伪可达性reachJ（l，ω）证明ω在l中不可达，如果reachJ（l，ω）=False，则返回False(iv) 最多尝试k次• lJ←l• 对每个或门进行计数，使得lJ是仅具有与门的LCG• 如果仍有循环：· 返回步骤（iv）• 使用ASP生成在lJ中以α开始的所有轨迹· 如果找到以ω结尾的轨迹t，则返回True(v) returnInconclusiveLCG说明了为达到目标状态而触发的必要转换之间的因果关系;删除循环的尝试简化了LCG并保持可达性不变;伪可达性允许人们基于LCG的拓扑结构过滤一些不可达的情况。启发式方法是我们算法的核心。随机选择避免了不同OR门的组合爆炸。ASP部分彻底搜索结果，但不遍历整个状态空间（ASP求解器从约束开始，找到一个一致的顺序并终止搜索）。算法2提供了采用LCG的算法的详细伪代码 l作为输入，其详细构造在算法1中给出。 删除第4-8 所有周期最多具有一个输入边沿。在移除循环之后，LCG可以包含没有后继者的节点。 这样的节点可以被修剪，因为它们不会导致初始状态（第9-18行）。 这种预处理减少了在步骤4中执行的随机搜索。现在我被修剪了，可能没有周期了。l的静态分析可以被用作检验伪可达性（定义2.8）的算法，以检测一些可能在搜索之前结束的不可达情况（第19-21行）LCG显示了本地状态之间的依赖关系，148X. Chai等人/理论计算机科学电子笔记350（2020）139一曰： 输入：LCG1 =（V状态，V解，E），整数k第二章： 输出：可达性r和轨迹t3：计算SCC，将它们分类为具有至多1个进入边缘的SCC 1（l）和否则的SCC 2（l四： // 1）打破所有循环，修剪无用的分支5：对于每个（VsJ状态<$V状态，Vsj解<$V解）∈SCC 1（l），6：对于每个v∈VsJ状态，7：如果n（v，vJ）∈E，vJ∈（V解\Vs解），则8：E←E\{（v，vJJ）|vJJ∈VsJ解，（v，vJJ）∈ E}9：// 2）删除无用的节点/边10：修剪=真11：whilepruneddo12：pruned =False13：forv∈Vstatedo14：如果/（v，vJ）∈E，则15：V状态←V状态\{v};E←E\{（vJJ，v）∈E}16：E ← E\{（vJJ，sol）∈ E|sol ∈ {sol =（A → a）∈V解|v ∈ A17：V解← V解\{sol =（A → a）∈ V解|v ∈ A}18：修剪=真19：// 3）检查伪可达性20：如果pseudoReach（l）=False，则21：return（False，False）二十二： // 4）主搜索循环二十三： 对于每一个i在1…凯多24：lJ=（VsJtate，VsJsolution，EJ）←（Vstate，Vsolution，E）25：对于v∈VsJtatedo //处理每个或门26：选取一个随机元素（v，vJ）∈EJ27：EJ←EJ\{（v，vJJ）∈EJ|vJ J/= vJ}，其中$i∈ SCC 2（l）且i∈ EJ28：（r，t）←ASPsolve（lJ）29：如果r=True，则返回（True，t）三十： return（Inconclusive，null）算法2. ASPReach过渡。LCG中的路径暗示了达到目标状态的可能轨迹。如果pseudoReach（l，ω）=False，我们可以确保ω是不可达的，因为pseudo-reachability检查可达性的必要条件。如果reachJ（l，ω）=True，静态分析对于可达性分析是不够的。当静态分析失败时，最多执行k次随机搜索（第22-29行），以找到从初始状态α到目标状态ω的状态序列。如果存在具有多个引入边的圈，根据定理2.14，ω是不可达的。k的值将在后面的评估部分中讨论。随机选择为LCG的每个或门固定一个值，允许通过使用ASP生成所有可能的变量分配顺序来执行可达性检查。请记住，每个状态节点都是一个或门，我们必须选择它的后继解决方案之一X. Chai等人/理论计算机科学电子笔记350（2020）139149节点访问状态。一组或门选择称为赋值。3.1随机搜索由于每个OR门都有多个选择，为了避免组合爆炸，我们使用一个简单的启发式算法：每次试验随机选择一个分配。这样我们就可以构造一个新的无或门的LCG，每个状态节点只有一个后继解节点。在应用逻辑学删除或门之后，我们使用ASP（Answer Set Programming）[3]来分析新获得的仅具有与门的LCG。ASP是一个类似于Prolog的声明式编程范例。它使用问题的描述和约束（称为规则），而不是命令式命令。ASP求解器通过生成约束条件的所有可能性来我们使用Clingo[16]，这是一个组合的地面Gringo和求解器扣。给定一个带有一阶变量的输入程序，grounder为ASP程序计算一个等价的基础（无变量）程序，而solver在基础上选择可接受的解决方案规则的形式如下：a0级 ← a1，.，是m，不是m+1，...，不是n。其中箭头左边的元素称为head，右边的元素称为body。0是真的，如果1，...，a m为真，且a m+1，...，n是假的。一些特殊的规则值得注意。m=n= 0的规则被称为事实，并且对于表示数据很有用，因为左边的原子a0总是True。它通常没有中心箭头。另一方面，一个规则，其中n >0，一个0=0称为一个约束。由于约束永远不会变为True，因此如果约束的右侧为True，则整个解决方案将无效因此，约束对于过滤掉不需要的解决方案很在约束中通常省略符号“”程序可以不产生答案集、产生一个答案集或产生多个答案集。例如，程序b：-不是c。C：不是B。生成两个答案集：{b}和{c}。事实上，c的不存在使b为真，反之，b的不存在使c为真。基数约束是获得多个答案集的另一种方法的使用基数的最常用方式是代替0：l {q1，...，q k} u ← a1，.，是m，不是m+1，...，不是n。其中k≥ 0，l是整数，u是整数或∞。 这种基数意味着 在满足物体的条件下，答案集合X必须包含集合{q1，...， q m}，或者换 句话说：|{q1,..., q m}X| ≤ u。ASP编码在删除或门之后，为了在ASP中对可达性问题进行编码，我们首先描述以下事实：150X. Chai等人/理论计算机科学电子笔记350（2020）139谓词init（a，i）表示自动机a处于初始状态i。谓词节点（a，i，n）表示LCG中的节点ai编号为n，而父节点（n1，n2）表示节点No。n1是No. n2.图3中的LCG编码如下：init（a，0）. init（b，0）. init（c，0）.node（a，1，1）. node（b，1，2）. node（c，1，3）. node（b，0，4）. node（c，0，5）.parent（1，2）. parent（1，3）.parent（2，5）. 父（3，4）。在事实之后，我们希望节点以一种顺序出现，通过这种顺序，我们可以顺序地触发从初始状态到目标状态的所有转换粗略的想法是：如果一个自动机a出现不同的状态，例如0和1。 其中一个必须处于初始状态（假设为0）。 头部的过渡必须在0返回到1之前触发0，否则LCG中没有允许1返回到0的解决方案节点。换句话说，0的前导必须出现在1之前。核心规则描述了这种约束。Predicateprior（N1，N2）表示节点 N1在结果状态序列中出现早于N2seq（O，a，i）表示状态节点ai出现在轨迹中的第Oreachable/unreachable是程序的最终结果%规则1，一个节点总是比它的前一个节点出现得早（N1，N2）：-parent（N2，N1）。%规则2，传递性prior（N1，N3）：- prior（N1，N2），prior（N2，N3）.%规则3，核心规则prior（N1，N2）：- node（P1，S1，N1），node（P2，S2，N2），node（P2，S3，N3），parent（N1，N3），init（P2，S3），S2！= S3，P1！=P2.%目标不可达，如果不可达的顺序存在冲突：-prior（N1，N2），prior（N2，N1），N1< N2。%一个节点出现一次，并且在序列1seq（1.. O，P，S）1：- O=节点（P1，S1，N1）：节点（P1，S1，N1），节点（P，S，N），不可达。序列中的%节点：-prior（N1，N2），node（P1，S1，N1），node（P2，S2，N2），seq（O1，P1，S1），seq（O2，P2，S2），O1>O2。%序列中的一个位置不能被多个节点占用：-seq（O1，P1，S1），seq（O2，P2，S2），P1！= P2，O1=O2。：-seq（O1，P1，S1），seq（O2，P2，S2），S1！= S2，O1=O2。%--输出格式，首先显示初始状态：-seq（O1，P1，S1），seq（O2，P2，S2），init（P1，S1），X. Chai等人/理论计算机科学电子笔记350（2020）139151不是init（P2，S2），O1>O2。：-seq（O1，P1，S1），seq（O2，P2，S2），init（P1，S1），init（P2，S2），152X. Chai等人/理论计算机科学电子笔记350（2020）139e0级D1和或的B1了c0和d0e1C1b0的P1 P2，O1>O2。可达：-不可达。记法：aDb表示a出现在b之前。当分析图3中的LCG时，规则1给出b0Da1，a1Dc1，a0Db1，b1Dc1;规则2给出a0Dc1和b0Dc1;规则3给出a1Db1和b1Da1，这是不可能的，因此不存在从初始状态到达c1C1不可达。如果我们找到一个与所有序约束一致的状态序列，我们就可以得到它对应的轨迹，从而确定目标状态是可达的。∅ ∅∅ ∅见图6。如果LCG包含这种结构，结果可能是不确定的。然而，这种不确定性需要一个不放弃其他可实现的品牌的努力。然而，ASPReach并不完整。图6中示出了一个反例，当一个或门的多个分支导致不可达时，结果可能是不确定的。有一个棘手的方法来处理这个问题时，|ORgates|并不大：我们设置一个限制n，如果|ORgates| 0是整数。调用ASPReach（l，k）终止。ASPReach（l，k）=（False，k）仅当$t是l中从α到ω的轨迹。ASPReach（l，k）=（True，t），仅当在l中从α到ω的轨迹为t时。证明见附录B。定理3.2（ASPReach复杂度）设l =（ Vstate，Vsolution，E）为初始状态为α的LCG，k > 0为整数。设s = |V溶液|是l的目标状态的数目。设v = |V状态|是l的顶点数。设e = |E|是l 的边数。 ASPReach（l，k）的复杂度为O（v + e + v/2 ×v×e×s + v2×e + v×e + k×（v×e2 + 2v）），其有界性为O（k×2v）.证据见附录B。4评价在本节中，我们通过各种实验来评估我们的方法。所有测试均在Intel Core i7-3770CPU，3.4GHz，8 Gb RAM计算机上运行为了验证我们的方法，我们首先测试了一个小模型，λ-噬菌体模型[34]，以与单独实现的替代可达性分析器Pint[27]进行X. Chai等人/理论计算机科学电子笔记350（2020）139153使用LCG分析[25，15，26]。在这个有4个自动机和12个转换的模型中（不考虑自我调节），我们的结果显示了完全的结论性，而Pint不能（图7）。PermReach[7]也不能处理某些特殊情况，即一个自动机的多个状态出现在不同的分支中（图8）。这些情况都可以通过ASPReach解决。整个方法在Python 3 5中实现。ASP的调用是通过pyasp 6包完成的。∅见图7。λ-噬菌体模型中的一个LCG，自动机cl出现在与门的两个分支中。静态分析器Pi nt不能决定在这种情况下c ro1是否可实现，因为它不考虑状态序列e v e n中的顺序，尽管存在长度为3的解：c ll0：：cl0：：c ro1对应于映射{cl1} →c ll0：：{c ll0} →cl0：：{c ll0，cl0} →c ro1。∅见图8。这个反例表明，如果一个自动机的多个状态出现在一个与门的分支中，那么以前的PermReach是不确定的 （本例中为d0和d1）。然而，存在一致的状态序列：D1 **B1 ** C1 ** a1对应于记录{c0} →d1：：{d0，a0} →b1：：{d1，e0} →c1：：{b1，c1} →a1，这可以通过ASPRea ch找到。为了评估计算机网络的可扩展性，我们以T细胞受体模型（TCR）[31]和表皮生长因子受体模型（EGFR）[32]为例，前者包含95个自动机和206个转换，后者分别包含104个自动机和389个转换这些模型最初是布尔网络。根据附录A中的方法，BN被转换为ABAN。在这里，我们运行了与[15]中相同的测试。在TCR模型中，我们取3个自动机作为输入（cd 4cd 28tcrlig），穷尽地改变它们的初始状态组合（2 -3），取5个自动机（sreap 1nfkbnfat sigumab）的状态可达性作为输出。 同样，我们对EGFR模型进行了更大的测试，输入为13个自动机，输出为12个自动机。我们首先测试了传统模型检查器Mole7和NuSMV8的性能，其中Mole在12个输出中有6个输出是内存输出，所有输出都是内存输出。用于模型EGFR中的NuSMV。由于状态空间很大，传统的模型检测器已不适用。在TCR测试中， 我们的方法给出 了与 Pint完全相同 的结果。至于 EGFR 测试，ASPReach没有返回不确定的输出。5代码和测试数据可在https://github.com/XinweiChai/LCG-in-ASP6https://pypi.python.org/pypi/pyasp7http://www.lsv.fr/~ schwoon/tools/mole8http://nusmv.fbk.eu和CL0cro1CLL0CL1d0和∅B1和a0级∅的1C1和D1了c0e0级∅154X. Chai等人/理论计算机科学电子笔记350（2020）139模型λ噬菌体TCREGFR输入4313输出4512试验总数24× 4 = 6423× 5 = 40213× 12 = 98，304分析仪品脱ASPReach品脱ASPReach品脱ASPReach可达36人（56%）38人（59%）16人（40%）64 282人（65.4%）74 268人（75.5%）不确定2人（3%）0（0%）0（0%）9 986人（10.1%）0（0%）不可达26人（41%）24名（60%）24 036人（24.5%）24 036人（24.5%）总时间<1s<1s7s40s9小时50分钟3小时46分钟表1来自生物学文献的小（λ-噬菌体）和大（TCR，EGFR）样本的测试结果。使用全局搜索的模型检查器的结果是内存输出的，因此未在表中列出。“可达”、“不确定”和“不可达”分别给出可达性的不同结果的数目。值得注意的是，Pint中的不确定案例是由超时引起的[15]。如表1所示，对于ABAN，我们的方法比Pint更有说服力。在逻辑配置中，我们为OR门设置了一个阈值。如果预处理后的OR门少于10个，则计算将从启发式转换为枚举所有OR门组合。下面是这三个基准的情况。实验表明，ASPReach的能力在“简单”的情况下已经比Pint更具决定性为了测试ASPReach的全局适用性，我们对如下生成的随机模型进行了两组测试：给定转换数量，对于每个转换tr，头部ah从LS中随机选择，主体的第一个元素A1是其中LS1=LS\{ah，a1−h}。对于i>1，如果Ai−1=bx存在，则生成Ai以80%的概率，从LSi=LSi−1\{bx，b1−x}中选择。图9（a）显示了ASPReach在随机生成的ABAN上的平均运行时间。在这个实验中，我们固定了转换的数量，|Σ |× 3，每个转换具有从1到|Σ − 1|，其中k为生