Sufficient conditions for reachability in automata networks with priorities
Sufficient conditions for reachability in automata networks with priorities
复制标题
DOI：
10.1016/j.tcs.2015.08.040
复制
发表时间：
2015-12-10
影响因子：
1.1
通讯作者：
Roux, Olivier
中科院分区：
文献类型：
--
作者：
Folschette, Maxime;Pauleve, Loic;Roux, Olivier
在这篇文章中，我们开发了一个有效的下近似的异步自动机网络(AANS)的动力学框架。AAN是自动机之间具有同步转换的自动机网络，其中每个转换恰好改变一个自动机的局部状态(但允许任意数量的同步局部状态)。我们提出的工作是基于抽象解释的静态分析，它允许证明到达具有给定性质的状态是可能的，而不需要像通常的模型检验器那样计算：复杂性与局部状态的总数是多项式的，与单个自动机内的局部状态的数目是指数的。此外，我们对AANS进行了优先级分类，并将其编码为无优先级的AANS，从而扩展了我们的欠近似的应用范围。最后，给出了大规模生物网络模型检测的方法。(C)2015爱思唯尔B.V.保留所有权利。
In this paper, we develop a framework for an efficient under-approximation of the dynamics of Asynchronous Automata Networks (AANs). AAN is an Automata Network with synchronised transitions between automata, where each transition changes the local state of exactly one automaton (but any number of synchronising local states are allowed). The work we propose here is based on static analysis by abstract interpretation, which allows to prove that reaching a state with a given property is possible, without the same computational cost of usual model checkers: the complexity is polynomial with the total number of local states and exponential with the number of local states within a single automaton. Furthermore, we address AANs with classes of priorities, and give an encoding into AANs without priorities, thus extending the application range of our under-approximation. Finally, we illustrate our method for the model checking of large-scale biological networks. (C) 2015 Elsevier B.V. All rights reserved.