Generating and Checking Probabilistic Models

生成和检查概率模型

• 批准号: RGPIN-2019-06372
• 负责人: VanBreugel, Franck
• 金额: $ 1.68万
• 依托单位: York University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=679259
• 关键词: Generating; Checking; Probabilistic; Models

Nowadays, many software systems rely on randomness. For example, it is well known that randomness provides computer games with the ability to surprise players, which is a key factor in their long-term appeal. Randomness is also prominent in machine learning, as exemplified by the use of randomized algorithms such as stochastic gradient descent. Randomness is also ubiquitous in cryptography. These are just three examples that show how pervasive randomness is in today's software.******As Dijkstra wrote half a century ago, “Program testing can be used to show the presence of bugs, but never to show their absence!” Testing is the most commonly used technique to detect bugs in software systems. Software with randomness usually gives rise to multiple, potentially different, executions. Hence, running a test on software with randomness multiple times does not provide any guarantee that different executions are checked. Furthermore, if a bug has been found, reproducing it is difficult. Therefore, in the presence of randomness, techniques complementary to testing are essential for detecting bugs.******Model checking, a technique introduced by Clarke, Emerson, and Sifakis, complements testing in the quest to find bugs. Roughly, this technique consists of three major steps. Firstly, the software system is modeled. The resulting model is usually a state machine, where each state is an abstraction of a snapshot of the system and transitions between states describe all possible ways the system can evolve. Secondly, the properties of interest of the software system are expressed as formulas of a logic. Thirdly, the model checker is run. A model checker is a tool that takes as input a model and a property and attempts to check whether the property is satisfied in the model. Generally, there are three outcomes. Either the model checker confirms that the property holds in the model, or it provides a counterexample demonstrating that the property does not hold (which may indicate a bug in the modeled software system), or it runs out of memory or time.******In this proposal, I focus on models of software systems with randomness, which are often called probabilistic models. Checking properties of such models is known as probabilistic model checking. To evaluate new techniques and tools for probabilistic model checking, researchers either have considered less than a handful of realistic probabilistic models or have used randomly generated probabilistic models. Both approaches have serious shortcomings. The former approach gives us little confidence in the results. The latter approach only gives us useful results if the generated models have the same characteristics as models encountered in practice.******The two goals of my research program are***- developing techniques and tools that support probabilistic model checking, and***- generating realistic instances of probabilistic models to evaluate those techniques and tools.**

如今，许多软件系统依赖于随机性。例如，众所周知，随机性为电脑游戏提供了让玩家感到惊讶的能力，这是它们长期吸引力的关键因素。随机性在机器学习中也很突出，随机梯度下降等随机化算法的使用就是例证。随机性在密码学中也是普遍存在的。这只是说明当今软件中随机性是多么普遍的三个例子。*正如Dijkstra在半个世纪前所写的那样，“程序测试可以用来显示错误的存在，但永远不能用来显示它们的缺失！”测试是检测软件系统中错误的最常用技术。具有随机性的软件通常会导致多次执行，可能是不同的执行。因此，在具有随机性的软件上多次运行测试并不能保证检查不同的执行。此外，如果已经发现了错误，复制它是困难的。因此，在随机性存在的情况下，补充测试的技术对于检测错误是必不可少的。Clarke、Emerson和Sifakis引入的一种技术--模型检查--在寻找错误的过程中对测试进行了补充。粗略地说，这项技术包括三个主要步骤。首先，对软件系统进行建模。得到的模型通常是一个状态机，其中每个状态都是系统快照的抽象，状态之间的转换描述了系统可以演化的所有可能方式。其次，将软件系统的感兴趣属性表示为逻辑公式。第三，运行模型检查器。模型检查器是一种工具，它将模型和属性作为输入，并尝试检查该属性在模型中是否得到满足。一般来说，有三种结果。要么模型检查器确认属性在模型中成立，要么它提供一个反例来证明属性不成立(这可能表明建模的软件系统中存在错误)，或者它耗尽了内存或时间。*在这个建议中，我关注的是具有随机性的软件系统的模型，这通常被称为概率模型。检查此类模型的属性称为概率模型检查。为了评估概率模型检验的新技术和工具，研究人员要么考虑了不到几个现实的概率模型，要么使用了随机生成的概率模型。这两种方法都有严重的缺陷。前一种方法让我们对结果几乎没有信心。后一种方法只有在生成的模型具有与实践中遇到的模型相同的特征时才会给出有用的结果。*我的研究计划的两个目标是*-开发支持概率模型检查的技术和工具，以及*-生成概率模型的真实实例以评估这些技术和工具。**