Generating and 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.**