概率系统的模型检验与其应用

项目名称： 概率系统的模型检验与其应用

项目编号： No.61472473

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 张立军

作者单位： 中国科学院软件研究所

项目金额： 62万元

中文摘要： 形式化验证技术已被成功的应用到诸如ISDN协议、IEEE Futurebus标准和Needham-Schroeder认证协议等的验证中。近来，国内外学者将研究焦点逐渐转移到包含概率、报酬（reward）、时间等的概率模型及其扩展中来。这些是刻画网络协议、嵌入式系统、生物及能源系统的关键元素。 另一方面，现今系统建模的复杂度急剧增加、其包含的组件数目越来越多。我们面临着著名的状态空间爆炸问题：模型的状态空间往往成指数爆炸趋势增长。本项目的目标是研究高效的概率模型检验技术。我们将研究互模拟状态优化、组合验证和概率模型的on-the-fly验证技术。从实践的角度来说，我们将扩展我们的概率模型检验工具IscasMC，使其支持更多模型种类、高效算法及友好的图形界面。我们的目标是把IscasMC发展成在国际同行有影响力的工具,使它能够分析复杂的系统，并在某些方面能超过PRISM等国际知名工具。

中文关键词： 概率模型检验；线性时序逻辑；马尔科夫链；马尔科夫决策过程；自动机理论

英文摘要： Formal verification techniques have been successfully applied to complex systems such as the IEEE Futurebus+ standard, Needham-Schroeder authentication algorithm and ISDN protocols. Recently, quantitative verification has become an important extension of the basic approach towards verifying systems involving probabilities, costs, and continuous-time. These characteristics are the key ingredients for modeling and analyzing networked, embedded, biological and energy systems. On the other side, the systems we are facing today are becoming more and more complex, and consist of many components. Indeed, the challenge of verifying such systems is the famous state-space explosion problem: the verification effort needed generally increases exponentially with their components. The goal of this project is to identify efficient verification techniques that are the most promising for analyzing large scale probabilistic systems. We shall focus especially on bisimulation minimization, compositional verification, and on-the-fly verification techniques for probabilistic systems. On the practical side, we plan to enrich our probabilistic model checker IscasMC to support richer models, efficient algorithms, friendly user interfaces. Our vision is to bring IscasMC an internationally recognized tool in the probabilistic verification community, which can compete with the leading tool PRISM in some respect.

英文关键词： probabilistic model checking;linear temporal logic;Markov chain;Markov decision process;automata theory