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.