Cargando…

Reachability Analysis Using Message Passing over Tree Decompositions

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,...

Descripción completa

Detalles Bibliográficos
Autor principal: Sankaranarayanan, Sriram
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363237/
http://dx.doi.org/10.1007/978-3-030-53288-8_30
_version_ 1783559629803880448
author Sankaranarayanan, Sriram
author_facet Sankaranarayanan, Sriram
author_sort Sankaranarayanan, Sriram
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7363237
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73632372020-07-16 Reachability Analysis Using Message Passing over Tree Decompositions Sankaranarayanan, Sriram Computer Aided Verification Article 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. 2020-06-13 /pmc/articles/PMC7363237/ http://dx.doi.org/10.1007/978-3-030-53288-8_30 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Sankaranarayanan, Sriram
Reachability Analysis Using Message Passing over Tree Decompositions
title Reachability Analysis Using Message Passing over Tree Decompositions
title_full Reachability Analysis Using Message Passing over Tree Decompositions
title_fullStr Reachability Analysis Using Message Passing over Tree Decompositions
title_full_unstemmed Reachability Analysis Using Message Passing over Tree Decompositions
title_short Reachability Analysis Using Message Passing over Tree Decompositions
title_sort reachability analysis using message passing over tree decompositions
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363237/
http://dx.doi.org/10.1007/978-3-030-53288-8_30
work_keys_str_mv AT sankaranarayanansriram reachabilityanalysisusingmessagepassingovertreedecompositions