Reachability Analysis Using Message Passing over Tree Decompositions

Reachability Analysis Using Message Passing over Tree Decompositions
复制标题

DOI:
10.1007/978-3-030-53288-8_30
复制
发表时间:
2020-06-13
期刊:
Computer Aided Verification
影响因子:
--
通讯作者:
Sankaranarayanan S
Sankaranarayanan S
中科院分区:
其他
文献类型:
--
作者:
Sankaranarayanan S

文献摘要

参考文献

相似文献

本文研究了离散时间非线性动力系统在变量之间的相关性具有低树宽时的可达性分析的有效方法。非线性动态系统的可达性分析是指从一组初始状态开始,是否可以达到一组给定的目标状态。这是通过使用抽象域来表示可达集合的近似来计算可达集合的近似的保守性来解决的。然而,大多数方法必须权衡保守性的程度和执行分析的成本,特别是当系统变量的数量增加时。这给具有大量状态变量的非线性系统的可达性分析带来了挑战。我们的方法通过构建系统变量之间的依赖图来工作。该图的树分解构建了树,其中树的每个节点用系统的状态变量的子集进行标记。此外,树分解还满足重要的结构性质。使用树分解,我们的方法将高维系统的一组状态抽象为该状态的低维投影集的树。我们得到了这个抽象域的各种性质,包括从低维投影完全恢复原始高维集的条件。接下来,我们使用最初为贝叶斯网络上的信任传播而开发的消息传递的思想,以高效的方式在整个状态空间上执行可达性分析。我们在一些有趣的低树宽的非线性系统上演示了我们的方法,以展示我们方法的优点。
In this paper, we study efficient approaches to reachability analysis for discrete-time nonlinear dynamical systems when the dependencies among the variables of the system have low treewidth. Reachability analysis over nonlinear dynamical systems asks if a given set of target states can be reached, starting from an initial set of states. This is solved by computing conservative over approximations of the reachable set using abstract domains to represent these approximations. However, most approaches must tradeoff the level of conservatism against the cost of performing analysis, especially when the number of system variables increases. This makes reachability analysis challenging for nonlinear systems with a large number of state variables. Our approach works by constructing a dependency graph among the variables of the system. The tree decomposition of this graph builds a tree wherein each node of the tree is labeled with subsets of the state variables of the system. Furthermore, the tree decomposition satisfies important structural properties. Using the tree decomposition, our approach abstracts a set of states of the high dimensional system into a tree of sets of lower dimensional projections of this state. We derive various properties of this abstract domain, including conditions under which the original high dimensional set can be fully recovered from its low dimensional projections. Next, we use ideas from message passing developed originally for belief propagation over Bayesian networks to perform reachability analysis over the full state space in an efficient manner. We illustrate our approach on some interesting nonlinear systems with low treewidth to demonstrate the advantages of our approach.
DOI: 10.1137/s0097539793251219
发表时间: 1996-12-01
影响因子: 1.6
作者:
Bodlaender, HL
通讯作者: Bodlaender, HL
DOI: 10.1137/s0036139996312703
发表时间: 1998-12-08
影响因子: 1.9
作者:
Cahn, JW;Mallet-Paret, J;Van Vleck, ES
通讯作者: Van Vleck, ES
DOI: 10.1145/1190215.1190258
发表时间: 2007-01-01
影响因子: --
作者:
Gulwani, Sumit;Jojic, Nebojsa
通讯作者: Jojic, Nebojsa
DOI: 10.1145/3210257
发表时间: 2018-08-01
影响因子: 1.3
作者:
Chatterjee, Krishnendu;Ibsen-Jensen, Rasmus;Pavlogiannis, Andreas
通讯作者: Pavlogiannis, Andreas
DOI: 10.1098/rspb.2002.2001
发表时间: 2002-07-07
影响因子: 4.7
作者:
Britton, NF;Franks, NR;Seeley, TD
通讯作者: Seeley, TD