p-Automata - Foundation for Probabilistic Model Checking

点击翻译按钮获取中文摘要

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.