Håkan L. S. Younes
Håkan Younes is a Staff Software Engineer at Google. 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.
Research Areas
Authored Publications
Sort By
Statistical verification of probabilistic properties with unbounded until
Edmund M. Clarke
Paolo Zuliani
Proceedings of the 13th Brazilian Symposium on Formal Methods, Springer, Berlin / Heidelberg(2010), pp. 144-160
Preview abstract
We consider statistical (sampling-based) solution methods for verifying probabilistic properties with unbounded until. Statistical solution methods for probabilistic verification use sample execution trajectories for a system to verify properties with some level of confidence. The main challenge with properties that are expressed using unbounded until is to ensure termination in the face of potentially infinite sample execution trajectories. We describe two alternative solution methods, each one with its own merits. The first method relies on reachability analysis, and is suitable primarily for large Markov chains where reachability analysis can be performed efficiently using symbolic data structures, but for which numerical probability computations are expensive. The second method employs a termination probability and weighted sampling. This method does not rely on any specific structure of the model, but error control is more challenging. We show how the choice of termination probability---when applied to Markov chains---is tied to the subdominant eigenvalue of the transition probability matrix, which relates it to iterative numerical solution techniques for the same problem.
View details
