QQ客服 官方微博 反馈留言

	Decidability of the Reachability for a Family of Linear Vector Fields
	Gan, Ting ; Chen, Mingshuai ; Dai, Liyun ; Xia, Bican ; Zhan, Naijun
	2015
关键词	Tarski&apos Polynomial-exponential function Reachability Real root isolation Cylindrical Algebraic Decomposition (CAD) CYLINDRICAL ALGEBRAIC DECOMPOSITION QUANTIFIER ELIMINATION HYBRID SYSTEMS IMPROVED PROJECTION AUTOMATA s algebra
英文摘要	The reachability problem is one of the most important issues in the verification of hybrid systems. Computing the reachable sets of differential equations is difficult, although computing the reachable sets of finite state machines is well developed. Hence, it is not surprising that the reachability of most of hybrid systems is undecidable. In this paper, we identify a family of vector fields and show its reachability problem is decidable. The family consists of all vector fields whose state parts are linear, while input parts are non-linear, possibly with exponential expressions. Such vector fields are commonly used in practice. To the best of our knowledge, the family is one of the most expressive families of vector fields with a decidable reachability problem. The decidability is achieved by proving the decidability of the extension of Tarski's algebra with some specific exponential functions, which has been proved in [21,22] due to Strzebonski. In this paper, we propose another decision procedure, which is more efficient when all constraints are open sets. The experimental results indicate the efficiency of our approach, even better than existing approaches based on approximation and numeric computation in general.; EI; CPCI-S(ISTP); gant@pku.edu.cn; chenms@ios.ac.cn; dailiyun@pku.edu.cn; xbc@pku.edu.cn; znj@ios.ac.cn; 482-499; 9364
语种	英语
出处	EI ; SCI
出版者	AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015
内容类型	其他
源URL	[http://hdl.handle.net/20.500.11897/436914]
专题	数学科学学院
推荐引用方式 GB/T 7714	Gan, Ting,Chen, Mingshuai,Dai, Liyun,et al. Decidability of the Reachability for a Family of Linear Vector Fields. 2015-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。