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 所写的一半。一个世纪前，“程序测试可以用来显示错误的存在，但永远不能显示它们的不存在！”测试是检测软件系统中错误的最常用技术，具有随机性的软件通常会产生多个可能不同的错误。因此，多次对具有随机性的软件进行测试并不能保证检查不同的执行。此外，如果发现错误，则很难重现它，因此，在存在随机性的情况下，技术是补充的。测试对于检测至关重要bugs.****** 模型检查是 Clarke、Emerson 和 Sifakis 提出的一种技术，它补充了寻找 bug 的方法。 粗略地说，该技术由三个主要步骤组成。模型通常是一个状态机，其中每个状态是系统快照的抽象，状态之间的转换描述了系统演化的所有可能方式。其次，软件系统的感兴趣的属性被表达为逻辑公式。 , 模型模型检查器是一种将模型和属性作为输入并尝试检查模型中是否满足该属性的工具。通常，模型检查器会确认该属性在模型中成立。模型，或者它提供了一个反例，证明该属性不成立（这可能表明建模软件系统中存在错误），或者它耗尽了内存或时间。*****在这个提案中，我专注于模型具有随机性的软件系统，通常称为检查此类模型的属性称为概率模型检查，为了评估概率模型检查的新技术和工具，研究人员要么考虑了少数现实的概率模型，要么使用了随机生成的概率模型。前一种方法让我们对结果缺乏信心，后一种方法只有在生成的模型与实践中遇到的模型具有相同的特征时才能给我们带来有用的结果。******我的研究计划的两个目标是* **- 开发技术和支持概率模型检查的工具，以及***-生成概率模型的真实实例来评估这些技术和工具。**