Accession Number:

ADA456813

Title:

Verification and Planning for Stochastic Processes with Asynchronous Events

Descriptive Note:

Doctoral thesis

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2005-01-01

Pagination or Media Count:

223.0

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, the author considers the problems of verification and planning for stochastic processes with asynchronous events, without relying on the Markov assumption. He establishes the foundation for statistical probabilistic model checking, an approach to probabilistic model checking based on hypothesis testing and simulation. He demonstrates 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, he can set this error bound arbitrarily low at the cost of efficiency. His contribution in planning consists of a formalism, the generalized semi-Markov decision process GSMDP, for planning with asynchronous stochastic events. He considers both goal-directed and decision theoretic planning. In the former case, he relies on statistical model checking to verify plans, and uses the simulation traces to guide plan repair. In the latter case, he presents the use of phase-type distributions to approximate a GSMDP with a continuous-time MDP, which can then be solved using existing techniques. He demonstrates that the introduction of phases permits him to take history into account when making action choices, and this can result in policies of higher quality than he would get if he ignored history dependence.

Subject Categories:

  • Statistics and Probability
  • Computer Programming and Software
  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE