期刊文献+
共找到2篇文章
< 1 >
每页显示 20 50 100
软件模型检测中的抽象模型研究综述 被引量:12
1
作者 魏欧 石玉峰 +2 位作者 徐丙凤 黄志球 陈哲 《计算机研究与发展》 EI CSCD 北大核心 2015年第7期1580-1603,共24页
抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统... 抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统的用于支持自上逼近或者自下逼近的布尔Kripke结构;2)分别对应于3值和4值Kripke结构的Kripke模态迁移系统(Kripke modal transition systems,KMTS)和混合迁移系统(mixed transition system,MixTS),可同时支持自上逼近和自下逼近的抽象;3)具有超迁移关系的广义Kripke模态迁移系统(generalized Kripke modal transition system,GKMTS)和超迁移系统(hyper transition system,HTS),可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果.最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向. 展开更多
关键词 抽象模型 自上逼近 自下逼近 模型检测 多值模型
下载PDF
Nonholonomic motion planning for a free-falling cat using spline approximation 被引量:4
2
作者 GE XinSheng GUO ZhengXiong 《Science China(Physics,Mechanics & Astronomy)》 SCIE EI CAS 2012年第11期2100-2105,共6页
An optimal motion planning of a free-falling cat based on the spline approximation is investigated.Nonholonomicity arises in a free-falling cat subjected to nonintegrable velocity constraints or nonintegrable conserva... An optimal motion planning of a free-falling cat based on the spline approximation is investigated.Nonholonomicity arises in a free-falling cat subjected to nonintegrable velocity constraints or nonintegrable conservation laws.The equation of dynamics of a free-falling cat is obtained by using the model of two symmetric rigid bodies.The control of the system can be converted to the motion planning problem for a driftless system.A cost function is used to incorporate the final errors and control energy.The motion planning is to determine control inputs to minimize the cost function and is formulated as an infinite dimensional optimal control problem.By using the control parameterization,the infinite dimensional optimal control problem can be transformed to a finite dimensional one.The particle swarm optimization(PSO) algorithm with the cubic spline approximation is proposed to solve the finite dimension optimal control problem.The cubic spline approximation is introduced to realize the control parameterization.The resulting controls are smooth and the initial and terminal values of the control inputs are zeros,so they can be easily generated by experiment.Simulations are also performed for the nonholonomic motion planning of a free-falling cat.Simulated experimental results show that the proposed algorithm is more effective than the Newtoian algorithm. 展开更多
关键词 falling cat nonholonomic constraint motion planning spline approximation particle swarm optimization
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部