Formal verification of probabilistic systems.

摘要

Methods for the formal verification and specification of systems are a critical tool for the development of correct systems, and they have been applied to the design of hardware, software and control systems. While some system properties can be studied in a non-probabilistic setting, others, such as system performance and reliability, require a probabilistic characterization of the system. The formal analysis of these properties is especially necessary in the case of safety-critical systems, which must be designed to meet specific reliability and performance guarantees.; This dissertation focuses on methods for the formal modeling and specification of probabilistic systems, and on algorithms for the automated verification of these systems. Our system models describe the behavior of a system in terms of probability, nondeterminism, fairness and time.; The formal specification languages we consider are based on extensions of branching-time temporal logics, and enable the expression of single-event and long-run average system properties. This latter class of properties, not expressible with previous formal languages, includes most of the performance properties studied in the field of performance evaluation, such as system throughput and average response time. We also introduce a classification of probabilistic properties, which explains the relationship between the different classes of properties expressible in the proposed languages.; Our choice of system models and specification languages has been guided by the goal of providing efficient verification algorithms. The algorithms rely on the theory of Markov decision processes, and exploit a connection between the graph-theoretical and probabilistic properties of these processes. This connection also leads to new results about classical problems, such as an extension to the solvable cases of the stochastic shortest path problem, an improved algorithm for the computation of reachability probabilities, and new results on the average reward problem for semi-Markov decision processes.