基于模型检测的非确定性概率模型学习

As computer-based systems have gained their popularity in the society, the correctness and reliability of such systems become crucial. Model checking, an automatic formal verification technique, is proposed to evaluate the target system based on its suitable model against desired behavioral properties through investigation over all states of the model. Probabilistic Model Checking (PMC), which enjoys the joint force of model checking approach and the probability theory, is capable of verifying both qualitative and quantitative properties on the given system. However, constructing accurate system models manually is regarded as an obstacle by the industry community to apply PMC in large-scale application domains, due to its time-consuming and error-prone procedure. In order to alleviate this limitation, we will focus on developing learning algorithms for automatically constructing probabilistic models, (in particular, nondeterministic probabilistic models), from sample executions; linking the convergence of the learning algorithm to the convergence of the system property; and proposing suitable distances functions to assess the quality of the learned models. Finally, we will establish a general learning framework to learn nondeterministic probabilistic models in the context of PMC.

随着计算机系统在日常生活中占据日益重要的地位，系统运行的正确性和可靠性也变得尤其重要。模型检测技术，将传统的形式化验证方法自动化，通过对系统描述模型中相关性质的自动验证来分析系统的可靠性。概率模型检测将模型检测技术与概率论相结合，能够量化地描述目标系统的随机行为，分析系统的随机性质，是模型检测领域一个新兴的研究方向。为目标系统构造一个正确的系统模型是一个复杂繁重且极易出错的过程，被工业界视为将模型检测技术更大范围应用的桎梏。本项目研究内容包括：提出基于模型检测的非确定性系统描述模型及其学习算法；研究算法收敛性与概率模型检测中系统性质收敛性；提出基于模型轨迹概率分布的距离对学习结果进行评价。最终本项目将建立一个概率模型建模平台，为概率模型检测提供高质量的系统描述模型。

随着计算机系统在日常生活中占据日益重要的地位，系统运行的正确性和可靠性也变得尤其重要。模型检测技术，将传统的形式化验证方法自动化，通过对系统描述模型中相关性质的自动验证来分析系统的可靠性。概率模型检测将模型检测技术与概率论相结合，能够量化地描述目标系统的随机行为，分析系统的随机性质，是模型检测领域一个新兴的研究方向。为目标系统构造一个正确的系统模型是一个复杂繁重且极易出错的过程，被工业界视为将模型检测技术更大范围应用的桎梏。本项目对模型学习算法以及相关收敛性问题进行了研究，提出了一个确定性模型的统一学习框架，并证明学习算法的收敛性。关于所学模型，主要研究与原始系统在轨迹性质方面的相似性，并提出来了相应的距离函数定量地描述相似性程度。本项目将研究范围扩展到了深度学习领域。首先提出了具有非对称结构的AE（UnsymmetricAuto-Encoder, UAE)模型，较传统的AE模型而言，所提出的UAE可以学习到更多更有效的物体特征，更一步的我们分析了UAE模型的梯度消失问题。其次，我们在AE模型的代价函数中显示地加入了一个具有引导性的项来帮助AE模型学习有意义的物体特征。对于AE模型，本项目进一步将其应用到了蛋白质二级结构预测问题中。针对细胞种类多样性、形状不规则性和高密度性等特点，采用深度学习领域的另一种典型网络模型，Convolutional Neural Network（CNN）模型和粒子滤波技术对细胞进行有丝分裂检测和细胞跟踪。项目发表SCI论文8篇，会议论文1篇，申请专利6项。