主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
张海宾,段振华.混合系统的符号化可达性分析.软件学报,2008,19(12):3111-3121
混合系统的符号化可达性分析
Symbolic Reachability Analysis of Hybrid Systems
投稿时间:2007-06-18  修订日期:2008-08-07
DOI:
中文关键词:  混合系统  矩形混合系统  可达性分析  验证  非线性混合系统
英文关键词:hybrid system  rectangular hybrid system  reachability analysis  verification  nonlinear hybrid system
基金项目:Supported by the National Natural Science Foundation of China under Grant No.60433010 (国家自然科学基金); the Defense Pre-Research Project of China under Grant No.51315050105 (装备预先研究项目)
作者单位
张海宾 西安电子科技大学 计算理论与技术研究所,陕西 西安 710071 
段振华 西安电子科技大学 计算理论与技术研究所,陕西 西安 710071 
摘要点击次数: 3976
全文下载次数: 4143
中文摘要:
      定义了一种称作混合区域的形式化结构表示矩形混合系统的状态集,它实际上是由一组特殊形式的线性不等式联立表示的多面体空间.证明了混合区域对于矩形混合系统的可达性操作的封闭性.此外,用矩形混合系统近似模拟非线性混合系统,相应地解决了非线性混合系统的可达性问题.使用混合区域,可以直接计算由某个正则的混合区域开始的可达集,这样,混合系统的可达性问题主要是求解混合区域的正则型问题,而这问题是一种线性规划问题,可以使用经典的线性规划算法加以解决.
英文摘要:
      A restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces. Hybrid zones are proved to be closed over reachability operations of rectangular hybrid systems. In addition, rectangular hybrid systems are used to simulate nonlinear hybrid systems, which enables us to use hybrid zones for reachability analysis of nonlinear hybrid systems. After the hybrid zone has been converted to the canonical form, reachability operations for hybrid systems can be implemented straightforwardly. Hence, the main computation is the operation for obtaining the canonical form of hybrid zones. Finding the canonical form can be automated by an algorithm for linear programming.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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