时态逻辑形式化描述并发系统性质

时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.     

先进上面级数字逻辑姿态控制律设计

建立了先进上面级姿态动力学模型和推力器配置方案,根据快速大角速度精确姿态机动的任务要求,设计了数字逻辑姿态控制律.考虑姿态角和姿态角速度的相互关系和测置误差的存在,将姿态相平面划分为多个控制区域,以节省燃料和避免测量误差的影响.在实际上面级参数下进行姿态机动控制仿真,采用数字逻辑姿态控制律能在16s内实现先进上面级俯仰角60°的大角度姿态机动,并能很好地保证姿态指向精度和姿态稳定度,控制效果也优于脉冲宽度调制.     

Prolog 对象系统 GKD-POS/SUN的设计与实现

GKD-POS/SUN是在模块化Prolog基础上设计并实现的一个面向对象Prolog解释器。它同时引入了模块化、模块间的通讯、切换、类、方法、继承、消息发送及接收等概念,并提供对这些概念的直接支持。本文描述了GKD-POS/SUN的语言规范、系统组织与设计、主要实现技术和相关对象操作原语。     

逻辑程序设计与关系数据库集成的一种基于预编译的解释方法

本文在研究逻辑程序设计与关系数据库的两种集成方法(解释和编译)的基础上,提出了一种新的基于预编译的解释方法,该方法保持了前两种方法的优点,克服了它们的不足。基于此方法,文中介绍了一个相应的集成系统的原型及主要实现技术,其中包括物理级的耦合连接,逻辑级的语言合成,源程序级的部分计算和静态优化,以及动态执行过程中的事实调度和版本管理等。目前,该原型作为知识库管理系统GKBMS 的内核,已投入实际应用。     

制订科学的预防维修大纲加速维修管理科学化

本文探讨了欧洲国家维修团体联盟(EFNMS)第十次学术会议的主题——“维修——为了未来的投资”的意义和内涵.在此基础上,重点介绍了为获取此种投资效益所必需制订的预防维修大纲的方法及其理论依据.     

控制系统故障的智能诊断技术

综述和讨论了故障诊断的模糊逻辑法、神经网络法和模糊神经网络法,并对其研究情况作了展望。     

Evaluating the potential effects from probabilistic selling of similar products

In this article, we consider an online retailer who sells two similar products (A and B) over a finite selling period. Any stock left at the end of the period has no value (like clothes going out of fashion at the end of a season). Aside from selling the products at regular prices, he may offer an additional option that sells a probabilistic good, “A or B,” at a discounted price. Whenever a customer buys a probabilistic good, he needs to assign one of the products for the fulfillment. Considering the choice behavior of potential customers, we model the problem using continuous‐time, discrete‐state, finite‐horizon dynamic programming. We study the optimal admission decisions and devise two scenarios, whose value functions can be used as benchmarks to evaluate the demand induction effect and demand dilution effect of probabilistic selling (PS). We further investigate an extension of the base MDP (Markov Decision Process) model in which the fulfillment of probabilistic sales is uncontrollable by the retailer. A special case of the extended model can be used as a benchmark to quantify the potential inventory pooling effect of PS. Finally, numerical experiments are conducted to evaluate the overall profit improvement, and the effects from adopting the PS strategy. © 2014 Wiley Periodicals, Inc. Naval Research Logistics, 61: 604–620, 2014     

UCAV空面多目标攻击三维轨迹规划技术

研究了单架无人作战飞机(UCAV)攻击多个地面目标的三维轨迹规划问题。首先,将问题形式化为一类特殊的旅行商问题(TSP),即带动力学约束的邻域访问TSP问题(DCTSPN)。其次,针对规划空间维度过高、搜索代价过大的问题,提出了一种基于概率路标图(PRM)的方法。该方法借鉴了基于采样的运动规划方法的思想,并结合多种组合优化技术,将原本连续状态空间中的轨迹规划问题转化为离散拓扑图上的路由问题。求解过程分为离线预处理和在线查询两个阶段。离线阶段采用Halton拟随机采样算法及Noon-Bean转换方法,将原问题转化为经典的非对称旅行商问题(ATSP);在线阶段根据战场态势的实时变化,快速更新路标图,然后采用LKH算法在线求解问题的近似最优解。为了保证生成的飞行轨迹满足平台的运动学/动力学约束,算法基于Gauss伪谱法构建了局部轨迹规划器。最后,以攻击时间最短为优化指标对算法进行了仿真实验。结果表明,本文提出的方法能够以较高的精度和在线收敛速度生成真实可行的、较优的多目标攻击轨迹。     

基于分离逻辑的程序分析技术

分离逻辑是John C Reynolds和Peter O’Hearn于2000年提出的基于Hoare逻辑分析程序中动态分配内存和指针别名的逻辑理论。首先回顾了分离逻辑系统的理论框架,然后讨论了分离逻辑在程序分析领域中符号执行、形态分析和并发程序分析验证这些领域中的应用成果,最后介绍了分离逻辑在程序分析技术中当前主要的研究方向。