主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
甘庭,夏壁灿.运用栅栏函数验证连续系统的有界时间安全性.软件学报,2016,27(3):645-654
运用栅栏函数验证连续系统的有界时间安全性
Barrier Certificate Generation for Safety Verification of Continuous Systems for a Bounded Time
投稿时间:2015-07-16  修订日期:2015-10-20
DOI:10.13328/j.cnki.jos.004986
中文关键词:  连续系统  安全性验证  栅栏函数  半定规划  平方和
英文关键词:continuous system  safety verification  barrier certificate  SDP(semi-definite programming)  SOS(sum of squares)
基金项目:国家自然科学基金(11271034,11290141)
作者单位E-mail
甘庭 北京大学数学科学学院, 北京 100871 gant@pku.edu.cn,xbc@math.pku.edu.cn 
夏壁灿 北京大学数学科学学院, 北京 100871  
摘要点击次数: 2046
全文下载次数: 1322
中文摘要:
      栅栏函数在连续系统验证方面有着广泛的应用,其主要想法在于:在可达集和非安全集之间寻找一个栅栏,从初始区域出发的路径不会越过这个栅栏,而非安全区域在栅栏的另外一端.这样,就可以通过寻找栅栏函数来验证一个系统的安全性.近年来,已有一些工作讨论连续系统在界时间情况下的栅栏函数生成.但是对于有些系统,人们可能只关心其在有界时间内的安全性.因为在界时间内不安全并不能说明在给定时间内也是不安全的,所以对于这类问题,界时间栅栏函数方法并不适用.受界时间栅栏函数方法的启发,针对有界时间的情况,给出有界时间栅栏函数生成方法.首先给出有界时间栅栏函数的一些充分条件,对于多项式系统,将多项式非负的条件做平方和松弛后利用平方和规划工具求解这些充分条件得到栅栏函数;对于初等系统(包含一些初等函数),先将该初等系统转化为一个多项式系统,然后求解对应多项式系统的栅栏函数.对一些界时间不安全的实例,演示了该方法在验证有界时间安全性问题上的有效性.
英文摘要:
      Barrier certificates have been widely used in verification of continuous systems.The main idea is to find a barrier which separates the reachable set from the unsafe set such that all the trajectories starting from the initial set will never go across the barrier.Thus the system's safety can be guaranteed by constructing a barrier.In recent years, barrier certificates have been successfully used for verification of continuous systems with unbounded time.However sometimes the safety for bounded time needs to be addressed.Since a system is unsafe with unbounded time cannot imply it is also unsafe with a bounded time, the unbounded time barrier certificate method could fail to verify the safety with bounded time.In this paper, a method is presented to generate a bounded time barrier certificate for safety verification of continuous systems with bounded time.Some sufficient conditions for the bounded time barrier certificate are specified.If the continuous system is a polynomial system, relax all the conditions of positive semi-definite polynomial to the sum of squares(SOS) polynomial and then use semi-definite programming(SDP) to solve the conditions for a bounded time barrier certificate;if the continuous system is an elementary system(containing some elementary functions), transform it to a polynomial system approximately, and then solve the corresponding polynomial system for a bounded time barrier certificate.For some practical examples which are unsafe for unbounded time, the paper shows the effectiveness of the proposed method for generating bounded time barriers.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利