多智体系统中约简状态空间的限界模型检测算法

为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.     

TSO内存模型下限界可线性化的可判定性研究

TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是Total Store Order（简称TSO）内存模型下可线性化的三个变种。在本文中我们提出了?-限界TSO-to-TSO可线性化和?-限界TSO可线性化,考察了?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题。它们分别是这三种可线性化的限界版本,都使用?-扩展历史,这样的扩展历史对应的执行有着限界数目（不超过?个）的函数调用、函数返回、调用刷出和返回刷出动作。?-扩展历史对应执行中的写动作数目是不限界的,进而执行中使用的存储缓冲区的大小也是不限界的,对应的操作语义是无穷状态迁移系统,所以三个限界版本可线性化的验证问题是不平凡的。 我们将定义在并发数据结构与顺序规约之间的?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题归约到?-扩展历史集合之间的TSO-to-TSO可线性化问题,从而以统一的方式验证了TSO内存模型下可线性化的三个限界版本。验证方法的关键步骤是判定一个并发数据结构是否有一个特定的?-扩展历史。我们证明了这个问题是可判定的,证明方法是将这一问题归约为已知可判定的易失通道机器的控制状态可达问题。本质上,这一归约将每一个函数调用或函数返回动作转化为写、刷出或cas（compare-and-swap）动作。在TSO-to-TSO可线性化的定义中,一个函数调用或函数返回动作会同时影响存储缓冲区和控制状态。为了模拟函数调用或函数返回动作对存储缓冲区的影响,我们在每个函数调用或函数返回动作之后立刻执行一个特定的写动作。这个写动作及其对应的刷出动作模拟了函数调用或函数返回动作对存储缓冲区的影响。我们引入观察者进程,为每个函数调用或函数返回动作“绑定”一个观察者进程的cas动作,以这种方式模拟了函数调用或函数返回动作对控制状态的影响。因此,我们证明了TSO内存模型下可线性化的这三个限界版本都是可判定的。我们进而证明了在TSO内存模型下判定可线性化的这三个限界版本的复杂度都在递归函数的Fast-Growing层级中。我们通过证明已知对应复杂度的单通道简单通道机器的可达问题和TSO内存模型下可线性化的三个限界版本可以互相归约得到这个结论。     

铁路机车车辆静态限界测量系统校准方法研究

静态限界是保证机车安全运行的基本条件,为了满足铁路机车静态限界快速、精确、自动测量的需要,本文基于电控移动机构和激光测距传感器建立了机车车辆静态限界测量系统.根据系统工作原理及结构组成,研究了系统校准方法,并设计了专用校准附件.该方法操作方便,实用性强,能够在现场一次性完成测量系统的局部标定与系统标定.经检定,该系统测量精度优于0.5 mm,满足了高速铁路机车车辆静态限界测量的要求.     

Bounded Model Checking for Probabilistic Computation Tree Logic

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

概率计算树逻辑的限界模型检测

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

改进的验证正确性ACTL性质的限界模型检测方法

近些年来,基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充,已经得到了一定的发展。其中,大部分的研究成果都集中在了使用该方法来进行系统查错方面,而在正确性性质的验证上一直难有突破,原因在于正确性性质的验证依赖于一个完备上界,而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变,就能够在一定程度上解决这一问题,进行正确性性质的验证。在此基础上对该编码方法进行改进,从而提高它的求解效率,扩大其应用领域。     

铁路限界物激光检测仪的设计与实现

实现了一个基于激光扫描的铁路限界物嵌入式检测仪及其后台分析系统.利用先进的激光测距仪、定位精准的步进电机和高灵敏度的倾角仪实现对铁路限界物及相关参数的快速、准确、可靠测量.后台分析系统运行于PC机,紧密结合检测仪所采集数据进行图形化分析处理.     

基于单片机的温度远程控制系统设计

本文介绍了一种基于单片机和VB的库房温度远程控制系统.该系统采用高精度的数字温度传感器及简单实用的输出控制电路同时对两个库房的温度进行检测和控制.检测误差小于±0.5摄氏度.通过RS232串行总线,用户可对温度实施远程控制,通过上位机可实现报警温度设置、库房实时温度的显示、温度曲线绘制、存储、查询、统计、控制等功能,系统操作简便、自动化程度高、扩展方便且具有良好的人机交互功能.该系统经过实验,取得了较为满意的控制效果.     

基于主视图投影的列车障碍物侵限实时感知方法

为提高轨道交通自动驾驶列车的障碍物感知能力,需增加列车对运行场景中障碍物侵限的感知能力。针对目前多传感融合算法对限界分析较少、实时性差、算力要求高的问题,文章提出一种使用相机和激光雷达作为传感器实时感知侵限障碍物的方法。该方法基于主视图（front view, FV）二维投影平面进行信息融合,通过离线联合标定获得投影矩阵,将激光雷达点云投影到FV平面,从相机图像中提取轨道计算限界;并使用点云预测修正传感器同步误差,根据投影的障碍物点云和限界做出侵限判断。通过在列车上安装传感器和感知系统进行了数据采集和实验验证,结果显示,本方法能够在低功耗嵌入式设备中运行,算法平均耗时16.2 ms;可以实时检测列车运行时前方障碍物是否侵限,并同时获得障碍物的位置和尺寸信息。     

镀膜玻璃透射比在线检测系统的设计与应用

镀膜玻璃透射比是其光学特性的重要指标之一.基于PCI- 1617L多功能数据采集卡,在C Builder开发环境下,运用多线程技术,给出了镀膜玻璃透射比在线检测系统的设计.该系统具有对镀膜玻璃生产线玻璃透射比参数进行实时采集、曲线跟踪显示、数据实时存储、查询报表等功能.通过现场测试,测试数据误差小于2%符合国家标准,并验证了系统的可行性与可靠性.     

基于三维空间模型的特高压耐张塔跳线间隙检测方法

提出一种基于三维空间模型的特高压耐张塔跳线间隙检测方法研究,利用三维激光扫描数据建立特高压耐张塔整体空间扫描模型,并描述激光扫描建模的原理。据此确定出了待检测标的物的三维点云数据集合;通过预处理的方式去除点云数据检测系统内部噪声和环境噪声,对点云数据集合进行高斯平滑滤波、坐标转换和点云数据拼接,并输出空间点云数据的文件集合;获取的跳线检测测量结果中还有可能包含粗差、系统误差和偶然性误差,利用检测数据分析前必须消除各种误差因素的影响。实验数据表明提出方法的坐标检测精度值能够控制在+-1,并且总体的检测残差分布也位于合理的区间范围之内,实际检测效果优于传统检测方法。     

深度学习屈光检测方法研究

屈光不正是一种非常常见且对视功能发育有严重危害的眼科问题。准确与方便的屈光检测技术,对于及时发现屈光不正问题以及采取相应措施进行干预具有非常重要的意义。目前的屈光筛查设备虽然能较快进行屈光检测,但主要存在两个问题：检测准确度较低,对被测者配合度要求较高。因此,提出一种新的屈光检测方法,此方法使用基于偏心摄影验光原理的光学系统获取人脸面部近红外图像,使用图像处理技术对面部近红外图像进行处理,得到左右瞳孔图像和瞳孔位置信息,使用提出的结合了深度可分离卷积和SE模块的混合数据多输入神经网络模型进行训练与屈光度的计算。与传统偏心摄影验光原理的屈光检测方法相比,此方法有望随着数据集的扩增而达到更高的准确度,并且此方法将瞳孔位置信息作为模型的输入,可以解决传统算法对被测者配合度要求较高的问题。该研究是对屈光检测新方法的一种有益探索,使用此方法有利于屈光筛查更便利地进行,为实现非接触自助式的屈光筛查提供基础。     

虚拟测试系统的测试误差分析

在测试系统中,测试误差影响测试数据的精度.消弱其对测试结果的影响是至关重要的.首先讨论了随机误差的分布、测度,然后建立两种数据模型:基于LabVIEW平台的参数测试系统观测数据模型和理想数据模型.以此模型为基础,分析数据中的系统误差和研究系统误差的检验方法.提出了基于后验检验统计的系统误差检测法.最后修改观测数据的模型.结合此模型研究系统误差和随机误差的评定指标.     

A Survey of Outlier Detection Methodologies

Outlier detection has been used for centuries to detect and, where appropriate, remove anomalous observations from data. Outliers arise due to mechanical faults, changes in system behaviour, fraudulent behaviour, human error, instrument error or simply through natural deviations in populations. Their detection can identify system faults and fraud before they escalate with potentially catastrophic consequences. It can identify errors and remove their contaminating effect on the data set and as such to purify the data for processing. The original outlier detection methods were arbitrary but now, principled and systematic techniques are used, drawn from the full gamut of Computer Science and Statistics. In this paper, we introduce a survey of contemporary techniques for outlier detection. We identify their respective motivations and distinguish their advantages and disadvantages in a comparative review.     

面向移动增强现实的室外阴影实时检测技术

针对目前移动视点下视频阴影检测算法存在的误检测率高和边缘连续性差的问题,提出了一种基于边跟踪、边检测框架的实时阴影检测算法.首先对前后2帧重叠的阴影部分进行2次光流跟踪,并筛选掉前后向跟踪误差较大的点,通过Canny边缘置信保证跟踪边缘的准确性;然后通过基于光流的区域划分法得到待检测的新增区域;其次,针对纹理边缘误检测...     

惯导/里程仪组合导航系统算法研究

惯导系统误差随着导航时间而增长,而里程仪测量误差一般随着运载体行驶距离而增加,惯导系统和里程仪具有互补性,推导了简化的惯导/里程仪组合导航系统的卡尔曼滤波方程,研究了里程仪刻度系数误差校正的方法,并提出了里程仪打滑和滑行故障的判断准则,仿真结果表明：经过里程仪刻度系数校正后,组合导航系统能有效提高定位精度,并且具备一定的容错能力.     

一种自适应失效检测算法的研究与应用

失效检测技术是保证容灾备份系统高可用性的关键技术之一,但经典的自适应失效检测算法失效检测时间较长、误判率较高。为此,提出一种基于指数分布的自适应失效检测算法λ-FD,采用Push与Pull 2种心跳模式结合的方法实现算法的重查策略。实验结果表明,λ-FD在阈值取0.68时性能较优,失效检测时间为1339.5 ms,误判率为0.055 7%,远低于同等失效检测时间下经典算法φ-FD的15.19%和Chen-FD的24.92%。λ-FD在相同失效检测时间下误判率普遍低于经典的自适应失效检测算法,相同误判率时耗费的失效检测时间较短,有效提高失效检测的性能,更符合广域网中灾备系统的应用需求。     

锂电池组关键参数模块化在线检测方法研究

锂电池是一种新兴的绿色清洁能源。与其他的化学电池相比,锂电池具有寿命长、能量密度高的优点。由于电池组电压、电流、温度等关键参数至关重要,采用模块化设计思路,结合芯片采集与高可靠数字通信基础,研究了一基于LTC6804的锂电池组关键参数检测的硬件系统。对锂电池组的关键参数进行了研究。采用STM32作为控制中心,LTC6804作为电压采集芯片,INA219作为负载电流检测模块,DS18B20作为温度检测器件。系统的电路板尺寸为110 mm×84 mm。其具有高集成度、空间利用率高的特点。试验结果表明,系统下单体电压值采集绝对误差低于2 mV、电流值采集绝对误差为10 mA、温度采集绝对误差为0.5℃,整个系统具有较高的精确度和可靠性。该系统可为锂电池组提供关键参数的精确检测,对锂电池组的安全运行有着重要意义。     

Robust optimization of constrained mechanical system with joint clearance and random parameters using multi-objective particle swarm optimization

Joint clearance and uncertainty are inevitable in mechanical systems due to design tolerance, abrasion, manufacture error, assembly error and imperfections. In this study, kinematic analysis and robust optimization of constrained mechanical systems with joint clearance and random parameters were performed. Joint clearance was modeled by Lankarani-Nikravesh contact force model, and probability space was applied for characterizing uncertain parameters. A kinematic analysis method based on Baumgarte approach and confidence region method was presented to predict kinematic error of the mechanical system. Slider-crank mechanism, an illustrative example was presented to show the influence of clearance and uncertainty on the kinematic accuracy. Then, a novel multi-objective robust optimization methodology was presented for kinematic accuracy robust optimization design of the constrained mechanical system. In this approach, a multi-objective robust optimization model derived from 95% confidence region is constructed to reduce the effects of clearance and parameter uncertainty on 95% confidence region of kinematic error. The robust optimization model is a double-loop process. A multi-objective robust optimization strategy, combing Kriging surrogate model, multi-objective particle swarm optimization, confidence region and Monte Carlo methods, was proposed to search the design variables for minimizing the optimization objectives derived from confidence region while balancing computational accuracy and efficiency of the optimization process. The optimal results of the slider-crank mechanism demonstrated the validity and feasibility of the proposed robust optimization method.     

抑制非线性扰动的迭代学习控制系统研究

多轴旋转机械体速率系统和位置系统中存在一类非线性扰动,这类非线性扰动具有多周期性的性质,并具有周期不变性。为抑制多周期非线性扰动对系统的影响,在系统满足连续里普希斯条件时,得出位置多周期非线性扰动转化为时间多周期非线性扰动的条件。提出一种迭代学习控制方法,通过系统误差收敛性分析来构造学习算子,利用系统的稳态误差信号构成前馈补偿,得出补偿多轴测旋转机械体周期非线性扰动的条件,并证明了算法稳定性。仿真表明,该方法能有效地补偿系统的多周期性非线性扰动,提高多轴旋转机械体系统的控制精度,具有较高的实用价值。