Report Number: CS-TR-98-1601
Institution: Stanford University, Department of Computer Science
Title: Formal Verification of Probabilistic Systems
Author: Alfaro, Luca de
Date: June 1998
Abstract: This dissertation presents methods for the formal modeling
and specification of probabilistic systems, and 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.
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/98/1601/CS-TR-98-1601.pdf