Generating and Checking Probabilistic Models

生成和检查概率模型

• 批准号: RGPIN-2019-06372
• 负责人: vanBreugel, Franck
• 金额: $ 1.68万
• 依托单位: York University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2021
• 资助国家: 加拿大
• 起止时间: 2021-01-01 至 2022-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=738872
• 关键词: 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 引入的一项技术，它补充了寻找错误的测试。粗略地说，该技术由三个主要步骤组成。首先，对软件系统进行建模。生成的模型通常是一个状态机，其中每个状态都是系统快照的抽象，状态之间的转换描述了系统演化的所有可能方式。其次，软件系统的感兴趣的属性被表达为逻辑公式。第三，运行模型检查器。模型检查器是一种工具，它将模型和属性作为输入，并尝试检查模型中是否满足该属性。一般来说，有三种结果。模型检查器要么确认该属性在模型中成立，要么提供一个反例来证明该属性不成立（这可能表明建模软件系统中存在错误），或者耗尽内存或时间。在这个提案中，我重点关注具有随机性的软件系统模型，通常称为概率模型。检查此类模型的属性称为概率模型检查。为了评估用于概率模型检查的新技术和工具，研究人员要么考虑了少数现实的概率模型，要么使用了随机生成的概率模型。这两种方法都有严重的缺点。前一种方法让我们对结果缺乏信心。如果生成的模型与实践中遇到的模型具有相同的特征，则后一种方法只能为我们提供有用的结果。我的研究计划的两个目标是 - 开发支持概率模型检查的技术和工具，以及 - 生成概率模型的真实实例来评估这些技术和工具。