Fitime Louis Fippo, Roux Olivier, Guziolowski Carito, Paulevé Loïc
LS2N, UMR CNRS 6004, Ecole Centrale de Nantes, Nantes, France.
Laboratoire d'Informatique de Paris Nord (LIPN), UMR 7030, Université Paris 13, 99 avenue Jean-Baptiste Clément, 93430 Villetaneuse, France.
Algorithms Mol Biol. 2017 Jul 20;12:19. doi: 10.1186/s13015-017-0110-3. eCollection 2017.
Numerous cellular differentiation processes can be captured using discrete qualitative models of biological regulatory networks. These models describe the temporal evolution of the state of the network subject to different competing transitions, potentially leading the system to different attractors. This paper focusses on the formal identification of states and transitions that are crucial for preserving or pre-empting the reachability of a given behaviour.
In the context of non-deterministic automata networks, we propose a static identification of so-called bifurcations, i.e., transitions after which a given goal is no longer reachable. Such transitions are naturally good candidates for controlling the occurrence of the goal, notably by modulating their propensity. Our method combines Answer-Set Programming with static analysis of reachability properties to provide an under-approximation of all the existing bifurcations.
We illustrate our discrete bifurcation analysis on several models of biological systems, for which we identify transitions which impact the reachability of given long-term behaviour. In particular, we apply our implementation on a regulatory network among hundreds of biological species, supporting the scalability of our approach.
Our method allows a formal and scalable identification of transitions which are responsible for the lost of capability to reach a given state. It can be applied to any asynchronous automata networks, which encompass Boolean and multi-valued models. An implementation is provided as part of the Pint software, available at http://loicpauleve.name/pint.
使用生物调控网络的离散定性模型可以捕捉众多细胞分化过程。这些模型描述了网络状态在不同竞争转换下的时间演化,可能会使系统趋向于不同的吸引子。本文聚焦于对对于保持或预先阻止给定行为可达性至关重要的状态和转换进行形式化识别。
在非确定性自动机网络的背景下,我们提出对所谓的分岔进行静态识别,即给定目标不再可达的转换。此类转换自然是控制目标出现的良好候选对象,特别是通过调节它们的倾向。我们的方法将回答集编程与可达性属性的静态分析相结合,以提供对所有现有分岔的欠近似。
我们在几个生物系统模型上展示了我们的离散分岔分析,为此我们识别了影响给定长期行为可达性的转换。特别是,我们将我们的实现应用于数百个生物物种之间的调控网络,证明了我们方法的可扩展性。
我们的方法允许对导致失去到达给定状态能力的转换进行形式化且可扩展的识别。它可以应用于任何异步自动机网络,包括布尔模型和多值模型。作为Pint软件的一部分提供了一个实现,可在http://loicpauleve.name/pint获取。