一种高效的显式模型检验方法

随着软硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.在显式模型检验工具Murphi的基础上,针对其可达状态空间组织存在的问题进行改进,提出了基于整型指针与Fibonacci散列的可达状态空间组织方法,实现了一个高效的显式模型检验原型系统,在确保验证正确的同时有效缩短了验证时间,并能在系统规范不可满足的情况下给出反例,有助于系统设计人员快速定位错误.理论分析和实验结果表明了本方法的有效性.     

Competitive Statehood in Libya: Governing Differently a Specific Setting or Deconstructing its Weak Sovereign State with a Fateful Drift Toward Chaos?

Abstract

Libya in 2011 witnessed a real process of political change, though different from all the policy-oriented jargon equating transition with a teleological transition to democracy. Due to the resilience of the Qadhafi regime in power and with the essential role of NATO intervention, the process was eased out by a eight-month civil war. Governance in post-Qadhafi Libya was not done through the rebuilding of centralized authorities. But it took the specific form of the emergence of multiple non-state actors embedded in local dynamics and then connected with weakened central authorities that had access to the huge Libyan resources. That raised complex questions about the quality of this mode of governance, especially at a time of pressing problems for Libya and its neighbors, whether direct ones (Tunisia, Egypt, Mali) or farther countries across the Mediterranean sea: terrorism with the expansion of Da’esh into the country and flows of refugees crossing Libya’s uncontrolled borders and flowing into Italy and then Europe by thousands.     

船舶静态电场跟踪的渐进更新扩展卡尔曼滤波器

为了实现利用船舶静态电场对船舶进行跟踪的目的,针对传统卡尔曼滤波算法中存在的问题,设计一种新的非线性滤波器。建立船舶的状态空间模型,分析传统卡尔曼滤波算法在船舶跟踪中存在的问题;依据渐进贝叶斯思想,利用连续白噪声与离散白噪声序列噪声协方差之间的关系,设计一种新的渐进更新扩展卡尔曼滤波器。仿真结果表明,该滤波器能有效地抑制由于初始误差较大而造成的滤波性能下降和滤波发散,能够有效地跟踪船舶,具有较高的实用价值。     

通用扩张状态观测器鲁棒飞行控制方法

针对存在参数不确定、外界干扰与测量噪声情况下飞行控制问题,提出一种基于通用扩张状态观测器的鲁棒飞行控制方法。首先基于状态相关的Riccati方程（SDRE）控制方法,对飞行器俯仰通道非线性模型进行扩展线性化;而后引入基于通用扩张状态观测器的控制方法,设计干扰补偿增益,实现对外界干扰的估计与补偿;最后通过在线解算状态相关矩阵及代数黎卡提方程,得出状态反馈增益与干扰补偿增益,实现对飞行器期望攻角的跟踪控制。通过与已有方法进行对比,验证了本文所提方法不仅对系统模型不确定性与外界干扰具有较强鲁棒性,而且在较大测量噪声情况下,其依然能够保证良好的跟踪控制效果,具有较强的工程应用价值。     

航空发动机自适应模拟退火遗传算法建模

以阶跃输入响应进行模型的检验,提出了航空发动机状态模型的建立方法:在抽功法所建立的状态空间模型的基础上,利用自适应模拟退火遗传算法对A、C矩阵元素进行寻优,解决了状态空间模型的响应与非线性模型不能够很好吻合的难题。仿真表明,得到的状态空间模型无论是动态过程还是稳态过程都能取得较高的建模精度,为航空发动机分布式控制的研究奠定了强有力的基础。     

我国城市消防远程监控系统建设刍议

从我国大力加快城市消防远程监控系统建设的背景出发,分析了城市消防远程监控系统的特点、主要功能,叙述了我国城市消防远程监控系统建设的发展历程和发展规划,并从消防部门角度就推进城市消防远程监控系统建设需要注意的相关问题进行了探讨。     

多尺度方法在强非线性系统中应用的一个注释

多尺度法在求解非线性系统时,目前所得到的结果多集中在弱非线性系统上。论文对多尺度法进行了改进。对强非线性杜芬系统进行了变换,得到了强非线性杜芬系统存在3个解的结论,其中大的和小的是稳定的,中间的是不稳定的,物理上实现哪个稳定运动取决于初始条件。     

基于fMRI的静息状态脑功能复杂网络分析

分析静息状态下人脑中不同区域之间的功能连接模式对研究静息状态下人脑正常功能活动具有重要意义。基于复杂网络理论对脑功能网络进行建模,考察静息状态脑功能网络的结构和拓扑特性。结果显示,网络具有小世界性质和无标度特性。进一步引入一种概率混合模型分析网络社团结构,得到的10个子网络中包含视觉系统、听觉系统、运动系统、默认网络以及与执行和工作记忆相关的脑区。推测出静息状态脑功能网络是由这些相对独立又彼此关联的子网络组成,其中楔前叶和扣带回作为网络的关键节点,在信息调度和传递中占据重要地位。     

基于Stateflow的PERT网络仿真方法

介绍了基于Stateflow的PERT网络仿真方法,详细阐述了建模思路、建模步骤以及难点问题的解决方法,并对PERT网络实例进行了仿真。该方法容许工序的持续时间服从任意分布,而且可以考虑所有可能出现的关键路线。     

基于指标值状态的自适应权重确定法

评估问题中指标值可能是已知的也可能是未知的,提出一种基于属性值状态的指标权重确定方法,该方法融合了粗糙集和区间数有序相离度的理论,根据指标值状态,自适应求取指标权重;同时引入调节算子,调节对主客观因素考虑的重视程度。详细地给出了自适应算法的步骤,并对算法的保序条件进行了分析,举例说明了该方法的应用,结果表明:方法简单实用,易于实现。