Abstract: Probabilistic verification of stochastic processes has received increasing attention in the model-checking community in the past decade, with a clear focus on developing numerical solution methods for model checking of Markov chains. Numerical techniques tend to scale poorly with an increase in the size of the model (the "state space explosion problem"), however, and are feasible only for restricted classes of stochastic discrete-event systems. In this talk, I present a statistical approach to probabilistic model checking, employing hypothesis testing and discrete-event simulation. This approach is widely applicable, as it requires only that we can simulate the dynamics of the system, and it scales well with model size. Since we rely on statistical hypothesis testing, we cannot guarantee that the verification result is correct, but we can at least bound the probability of generating an incorrect answer to a verification problem. I will discuss different techniques for hypothesis testing and different ways of controlling the probability of error in the results.

Haakan Younes is a Software Engineer at Google, Inc. Before joining Google, he was a Postdoctoral Fellow in the Computer Science Department at Carnegie Mellon University. His research focused on methods for analyzing and controlling the effects of uncertainty in system design and decision making. He has developed algorithms for probabilistic model checking and established the generalized semi-Markov decision process as a framework for decision-theoretic planning under temporal uncertainty. He earned distinction as Best Newcomer at the 2002 International Planning Competition with his heuristic partial-order/temporal planner VHPOP, and his PhD thesis earned him the first ICAPS Outstanding Dissertation Award in 2007. Dr. Younes received an M.S. (1998) in Computer Science and Technology from the Royal Institute of Technology in Sweden, and an M.S. (2002) and a PhD (2004) in Computer Science from Carnegie Mellon University. Appointments: dcm@cs.cmu.edu