Computer Science Department
School of Computer Science, Carnegie Mellon University
Verification and Planning for Stochastic Processes
with Asynchronous Events
Håkan Lorens Samir Younes
Keywords: Model checking, probabilistic verification, decision theoretic planning, failure analysis, stochastic processes, Markov chains, hypothesis testing, acceptance sampling, discrete event simulation, phase-type distributions, sequential analysis, temporal logic, transient analysis
Asynchronous stochastic systems are abundant in the real world.
Examples include queuing systems, telephone exchanges, and computer
networks. Yet, little attention has been given to such systems
in the model checking and planning literature, at least not without
making limiting and often unrealistic assumptions regarding the
dynamics of the systems. The most common assumption is that of
history-independence: the Markov assumption. In this thesis, we
consider the problems of verification and planning for stochastic
processes with asynchronous events, without relying on the Markov
assumption. We establish the foundation for statistical probabilistic
model checking, an approach to probabilistic model checking based
on hypothesis testing and simulation. We demonstrate that this
approach is competitive with state-of-the-art numerical solution
methods for probabilistic model checking. While the verification
result can be guaranteed only with some probability of error, we
can set this error bound arbitrarily low (at the cost of efficiency).
Our contribution in planning consists of a formalism, the generalized
semi-Markov decision process (GSMDP), for planning with asynchronous
stochastic events. We consider both goal directed and decision theoretic
planning. In the former case, we rely on statistical model checking
to verify plans, and use the simulation traces to guide plan repair.
In the latter case, we present the use of phase-type distributions
to approximate a GSMDP with a continuous-time MDP, which can then
be solved using existing techniques. We demonstrate that the
introduction of phases permits us to take history into account when
making action choices, and this can result in policies of higher
quality than we would get if we ignored history dependence.