【摘 要】
：
在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个
【机 构】
：
南京航空航天大学 计算机科学与技术学院,南京211106软件新技术与产业化协同创新中心,南京211106;
论文部分内容阅读
在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个“存在”问题.为了量化公式的可监控性和弱可监控性,本文提出了概率可监控性,并给出了根据其定义进行求解的方法.此外,本文还提出了基于马尔可夫链的概率可监控性求解算法,并将该算法分别基于概率模型检测器PRISM和SMT求解器进行了代码实现.实验结果表明,基于马尔可夫链的概率可监控性求解算法是正确的,且基于SMT求解器实现的算法效率明显高于基于PRISM实现的算法效率.
其他文献
根据搭载RGB-D相机的平面运动轮式机器人运动特点,本文提出一种基于等高约束条件和直线约束条件的误匹配特征点对筛选方法.本文首先在平面运动机器人相机运动约束条件下,建立
提出一种基于预测误差压缩编码的可逆信息隐藏算法.本算法利用全局混沌异或加密方法,在加密灰度图像的基础上,对图像n次均匀分块,每块采用无损预测编码原则,筛选出压缩的加密
高分辨率遥感图像中地物越来越清晰,变化检测不仅要能检测出大目标的变化,也要能检测出小目标的变化,还要兼顾干扰因素对变化性质的判断.本文针对高分辨率遥感图像变化检测,提出一种多尺度稀疏卷积模型,利用不同数量不同尺度的卷积层提取多尺度的特征,通过1×1卷积层实现跨通道信息整合,把不同通道中相关性高、同一空间位置的特征聚合在一起,有效减少了通道数量和参数数量,使得模型呈现稀疏性,大幅度削减参数的相互依存
随着信息网络的高速发展,特别是高速互联网、5G网络、物联网等的发展,网络流量信息的获取也变得更加容易,但对流量数据进行标记面临着不可逾越的困难.半监督学习能够将少量标