Verification and Planning for Stochastic Processes with Asynchronous Events
Abstract
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.
Sample citation
Håkan L. S. Younes. 2005.
Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania. CMU-CS-05-105.
Full paper (222 pages, 210 references)
Presentation (64 slides)