p-Automata - Foundation for Probabilistic Model Checking

随机系统，涉及概率方面的系统，在许多科学和工程学科中使用。在计算机科学中，这样的系统是概率算法、随机事件建模、队列分析等的基础模型。例如，通信协议使用随机性来打破等效过程之间的对称性，而移动的网络建模使用概率来捕获节点的出现、消失和移动。新的计算模式是一种小型设备和高度移动性，跨越传统边界。因此，能够对这样的系统进行分析和推理变得越来越重要。模型检测是对离散（非随机）系统进行推理的最成功的技术之一。模型检测是一种形式化的方法，其中系统的数学模型与规格说明进行对比。规范通常以高级逻辑语言给出，允许编写想要的（或不想要的）行为的描述。模型检查要么确认属性（在模型中）成立，要么产生一个显示规范失败的执行。离散系统的模型检测已经非常成功。到目前为止，它已经成为硬件行业的标准验证技术，在软件行业中也越来越重要。这一成功在很大程度上依赖于两个相辅相成的概念。首先，存在一个自动机理论框架，在这个框架内，系统和逻辑规范共存，并且可以进行推理。第二，抽象的概念，它允许只考虑与被检查的属性相关的系统信息。模型检测的一般方法的成功促使研究人员探索其对随机系统的适用性。近年来，大量的努力已经致力于概率模型检查，其中系统被建模为马尔可夫链和逻辑规范量化某些事件的概率。然而，概率模型检验比“正常”模型检验更容易受到状态爆炸问题的影响，即系统的大小（状态数）与其组件的数量呈指数关系。状态爆炸问题是一个主要的挑战，限制系统的大小，模型检查是适用的，无论有没有概率。如前所述，迄今为止，最成功的解决状态爆炸问题的方法是抽象。最近我介绍了p-自动机，一种新的计算设备模型，它将标记的马尔可夫链作为输入。我已经证明，这些自动机可以构成一个框架，推理抽象的马尔可夫链。p-自动机的基本性质的建立表明，他们支持的最重要的功能，构成一个自动机理论框架的推理马尔可夫链。这两个品质一起打开了将成功的抽象方法从离散模型检查推广到概率模型检查的道路。我相信p-自动机不仅具有使其成为推理马尔可夫链的自动机理论框架的必要特征，而且在实践中也可以这样做。在这个补助金中，我将开始展示p-自动机可以在概率模型检查的进展中发挥重要作用，并在实践中扩大其范围，从而验证复杂的随机系统。

Stochastic systems, systems involving probabilistic aspects, are used in many sciences and engineering disciplines. In computer science, such systems are the underlying model for probabilistic algorithms, modeling of stochastic events, queue analysis, and much more. For example, communication protocols use randomness to break symmetry between equivalent processes and modeling mobile networks uses probabilities to capture the appearance, disappearance, and movement of nodes. The new computing paradigm is one of small devices and a high degree of mobility, across traditional boundaries. Therefore it is becoming more and more important to be able to analyze and reason about such systems.One of the most successful techniques to reason about discrete (non-stochastic) systems has been model checking. Model checking is a formal method in which a mathematical model of a system is contrasted with a specification. The specification is usually given in a high level logical language that allows to write descriptions of wanted (or unwanted) behavior. Model checking either ascertains that the property holds (within a model) or produces an execution showing the failure of the specification. Model checking of discrete systems has been extremely successful. By now, it is a standard validation technique in hardware industry and has increasing importance in software industry. This success relied largely on two complementary concepts. First, the existence of an automata-theoretic framework within which systems and logical specifications live together and can be reasoned about. Second, the concept of abstraction, which allows to consider only information about the system that is relevant to the property that is being checked. The success of the general approach of model checking has prompted researchers to explore its applicability to stochastic systems. In recent years much effort has been devoted to probabilistic model checking, where systems are modeled as Markov chains and logical specifications quantify over the probabilities of certain events. However, probabilistic model checking suffers even more than "normal" model checking from the state-explosion problem, the fact that the size of the system (its number of states) is exponential in the number of its components. The state-explosion problem is a major challenge restricting the size of systems to which model checking is applicable, both with and without probabilities. As mentioned, the most successful approach to date to combat the state-explosion problem has been abstraction. Recently I introduced p-automata, a new model of a computation device that reads labeled Markov chains as input. I have shown that these automata can constitute a framework for reasoning abstractly about Markov chains. Basic properties of p-automata were established showing that they support the most important features that constitute an automata-theoretic framework for reasoning about Markov chains. These two qualities together open the way to generalizing the successful abstraction approach from discrete model checking to probabilistic model checking. It is my belief that p-automata not only have the necessary features that can make it an automata-theoretic framework for reasoning about Markov chains but can also do so in practice. In this grant I will start showing that p-automata can take on a major role in progressing probabilistic model checking and expanding its scope in practice, leading to the verification of complex stochastic systems.