Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant

To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research i...

Full description

Saved in:
Bibliographic Details
Published in:Tsinghua science and technology 2014-04, Vol.19 (2), p.211-222
Main Authors: Kong, Hui, He, Fei, Song, Xiaoyu, Gu, Ming, Tan, Hongyan, Sun, Jiaguang
Format: Article
Language:English
Subjects:
半代数
安全性
安全验证
感应
计算复杂性
诱导条件
量词消去
非线性动力系统
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c345t-56444c82a07fe331fca476694e0d08b29dd6ea1cb9dd91bc7833491bfa3b54c33
cites
container_end_page 222
container_issue 2
container_start_page 211
container_title Tsinghua science and technology
container_volume 19
creator Kong, Hui
He, Fei
Song, Xiaoyu
Gu, Ming
Tan, Hongyan
Sun, Jiaguang
description To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.
doi_str_mv 10.1109/TST.2014.6787375
format article
fullrecord <record><control><sourceid>wanfang_jour_cross</sourceid><recordid>TN_cdi_wanfang_journals_qhdxxb_e201402012</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><cqvip_id>49435176</cqvip_id><wanfj_id>qhdxxb_e201402012</wanfj_id><sourcerecordid>qhdxxb_e201402012</sourcerecordid><originalsourceid>FETCH-LOGICAL-c345t-56444c82a07fe331fca476694e0d08b29dd6ea1cb9dd91bc7833491bfa3b54c33</originalsourceid><addsrcrecordid>eNo1kL1vwjAQxa2qlUpp947p2CHUjh07GRH9QkJiSNrVujg2GBGnOIGS_75G0OXuJ91796SH0CPBE0Jw_lIW5STBhE24yAQV6RUakUxkseCYXwfGWMQ4IewW3XXdBmPKU0FHaFmA0f0QfWtvjVXQ29ZFrYkK3dh4ul3pyoNV0evgoAnnbVQMXa-bLjpYiOau3qveHnSgA3gLrr9HNwa2nX647DH6en8rZ5_xYvkxn00XsaIs7eOUM8ZUlgAWRlNKjAImOM-ZxjXOqiSva66BqCpATiolMkpZAAO0SpmidIyez39_wRlwK7lp996FRLlb18djJfWpDBxGErT4rFW-7TqvjfzxtgE_SILlqTwZypMnvbyUFyxPF8u6daudDQH_HpYzmhLB6R9X1W2t</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant</title><source>IEEE Xplore All Journals</source><creator>Kong, Hui ; He, Fei ; Song, Xiaoyu ; Gu, Ming ; Tan, Hongyan ; Sun, Jiaguang</creator><creatorcontrib>Kong, Hui ; He, Fei ; Song, Xiaoyu ; Gu, Ming ; Tan, Hongyan ; Sun, Jiaguang</creatorcontrib><description>To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.</description><identifier>ISSN: 1007-0214</identifier><identifier>EISSN: 1878-7606</identifier><identifier>EISSN: 1007-0214</identifier><identifier>DOI: 10.1109/TST.2014.6787375</identifier><language>eng</language><publisher>School of Software, Tsinghua University, Beijing 100084,China%Department of ECE, Portland State University, OR 97207, USA%Institute of Acoustics, Chinese Academy of Sciences, Beijing 100190, China</publisher><subject>半代数 ; 安全性 ; 安全验证 ; 感应 ; 计算复杂性 ; 诱导条件 ; 量词消去 ; 非线性动力系统</subject><ispartof>Tsinghua science and technology, 2014-04, Vol.19 (2), p.211-222</ispartof><rights>Copyright © Wanfang Data Co. Ltd. All Rights Reserved.</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c345t-56444c82a07fe331fca476694e0d08b29dd6ea1cb9dd91bc7833491bfa3b54c33</citedby></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Uhttp://image.cqvip.com/vip1000/qk/85782X/85782X.jpg</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Kong, Hui</creatorcontrib><creatorcontrib>He, Fei</creatorcontrib><creatorcontrib>Song, Xiaoyu</creatorcontrib><creatorcontrib>Gu, Ming</creatorcontrib><creatorcontrib>Tan, Hongyan</creatorcontrib><creatorcontrib>Sun, Jiaguang</creatorcontrib><title>Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant</title><title>Tsinghua science and technology</title><addtitle>Tsinghua Science and Technology</addtitle><description>To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.</description><subject>半代数</subject><subject>安全性</subject><subject>安全验证</subject><subject>感应</subject><subject>计算复杂性</subject><subject>诱导条件</subject><subject>量词消去</subject><subject>非线性动力系统</subject><issn>1007-0214</issn><issn>1878-7606</issn><issn>1007-0214</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2014</creationdate><recordtype>article</recordtype><recordid>eNo1kL1vwjAQxa2qlUpp947p2CHUjh07GRH9QkJiSNrVujg2GBGnOIGS_75G0OXuJ91796SH0CPBE0Jw_lIW5STBhE24yAQV6RUakUxkseCYXwfGWMQ4IewW3XXdBmPKU0FHaFmA0f0QfWtvjVXQ29ZFrYkK3dh4ul3pyoNV0evgoAnnbVQMXa-bLjpYiOau3qveHnSgA3gLrr9HNwa2nX647DH6en8rZ5_xYvkxn00XsaIs7eOUM8ZUlgAWRlNKjAImOM-ZxjXOqiSva66BqCpATiolMkpZAAO0SpmidIyez39_wRlwK7lp996FRLlb18djJfWpDBxGErT4rFW-7TqvjfzxtgE_SILlqTwZypMnvbyUFyxPF8u6daudDQH_HpYzmhLB6R9X1W2t</recordid><startdate>20140401</startdate><enddate>20140401</enddate><creator>Kong, Hui</creator><creator>He, Fei</creator><creator>Song, Xiaoyu</creator><creator>Gu, Ming</creator><creator>Tan, Hongyan</creator><creator>Sun, Jiaguang</creator><general>School of Software, Tsinghua University, Beijing 100084,China%Department of ECE, Portland State University, OR 97207, USA%Institute of Acoustics, Chinese Academy of Sciences, Beijing 100190, China</general><scope>2RA</scope><scope>92L</scope><scope>CQIGP</scope><scope>~WA</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>2B.</scope><scope>4A8</scope><scope>92I</scope><scope>93N</scope><scope>PSX</scope><scope>TCJ</scope></search><sort><creationdate>20140401</creationdate><title>Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant</title><author>Kong, Hui ; He, Fei ; Song, Xiaoyu ; Gu, Ming ; Tan, Hongyan ; Sun, Jiaguang</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c345t-56444c82a07fe331fca476694e0d08b29dd6ea1cb9dd91bc7833491bfa3b54c33</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2014</creationdate><topic>半代数</topic><topic>安全性</topic><topic>安全验证</topic><topic>感应</topic><topic>计算复杂性</topic><topic>诱导条件</topic><topic>量词消去</topic><topic>非线性动力系统</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Kong, Hui</creatorcontrib><creatorcontrib>He, Fei</creatorcontrib><creatorcontrib>Song, Xiaoyu</creatorcontrib><creatorcontrib>Gu, Ming</creatorcontrib><creatorcontrib>Tan, Hongyan</creatorcontrib><creatorcontrib>Sun, Jiaguang</creatorcontrib><collection>维普_期刊</collection><collection>中文科技期刊数据库-CALIS站点</collection><collection>维普中文期刊数据库</collection><collection>中文科技期刊数据库- 镜像站点</collection><collection>CrossRef</collection><collection>Wanfang Data Journals - Hong Kong</collection><collection>WANFANG Data Centre</collection><collection>Wanfang Data Journals</collection><collection>万方数据期刊 - 香港版</collection><collection>China Online Journals (COJ)</collection><collection>China Online Journals (COJ)</collection><jtitle>Tsinghua science and technology</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Kong, Hui</au><au>He, Fei</au><au>Song, Xiaoyu</au><au>Gu, Ming</au><au>Tan, Hongyan</au><au>Sun, Jiaguang</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant</atitle><jtitle>Tsinghua science and technology</jtitle><addtitle>Tsinghua Science and Technology</addtitle><date>2014-04-01</date><risdate>2014</risdate><volume>19</volume><issue>2</issue><spage>211</spage><epage>222</epage><pages>211-222</pages><issn>1007-0214</issn><eissn>1878-7606</eissn><eissn>1007-0214</eissn><abstract>To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.</abstract><pub>School of Software, Tsinghua University, Beijing 100084,China%Department of ECE, Portland State University, OR 97207, USA%Institute of Acoustics, Chinese Academy of Sciences, Beijing 100190, China</pub><doi>10.1109/TST.2014.6787375</doi><tpages>12</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 1007-0214
ispartof Tsinghua science and technology, 2014-04, Vol.19 (2), p.211-222
issn 1007-0214
1878-7606
1007-0214
language eng
recordid cdi_wanfang_journals_qhdxxb_e201402012
source IEEE Xplore All Journals
subjects 半代数
安全性
安全验证
感应
计算复杂性
诱导条件
量词消去
非线性动力系统
title Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-27T06%3A28%3A26IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-wanfang_jour_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Safety%20Verification%20of%20Semi-Algebraic%20Dynamical%20Systems%20via%20Inductive%20Invariant&rft.jtitle=Tsinghua%20science%20and%20technology&rft.au=Kong,%20Hui&rft.date=2014-04-01&rft.volume=19&rft.issue=2&rft.spage=211&rft.epage=222&rft.pages=211-222&rft.issn=1007-0214&rft.eissn=1878-7606&rft_id=info:doi/10.1109/TST.2014.6787375&rft_dat=%3Cwanfang_jour_cross%3Eqhdxxb_e201402012%3C/wanfang_jour_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c345t-56444c82a07fe331fca476694e0d08b29dd6ea1cb9dd91bc7833491bfa3b54c33%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_cqvip_id=49435176&rft_wanfj_id=qhdxxb_e201402012&rfr_iscdi=true