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
Google Publications
Other 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
Statistical probabilistic model checking with a focus on time-bounded properties
Error control for probabilistic model checking
Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, Springer, Berlin / Heidelberg (2006), pp. 142-156
Numerical vs. statistical probabilistic model checking
Marta Kwiatkowska
Gethin Norman
David Parker
International Journal on Software Tools for Technology Transfer, vol. 8 (2006), pp. 216-228
Probabilistic verification for ``black-box'' systems
Proceedings of the 17th International Conference on Computer Aided Verification, Springer, Berlin / Heidelberg (2005), pp. 253-265
Planning and execution with phase transitions
Proceedings of the Twentieth National Conference on Artificial Intelligence, AAAI Press, Menlo Park, California (2005), pp. 1030-1035
The first probabilistic track of the international planning competition
Michael L. Littman
David Weissman
John Asmuth
Journal of Artificial Intelligence Research, vol. 24 (2005), pp. 851-887
Ymer: A statistical model checker
Proceedings of the 17th International Conference on Computer Aided Verification, Springer, Berlin / Heidelberg (2005), pp. 429-433
Solving generalized semi-Markov decision processes using continuous phase-type distributions
Reid G. Simmons
Proceedings of the Nineteenth National Conference on Artificial Intelligence, AAAI Press, Menlo Park, California (2004), pp. 742-747
Numerical vs. statistical probabilistic model checking: An empirical study
Marta Kwiatkowska
Gethin Norman
David Parker
Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin / Heidelberg (2004), pp. 46-60
Policy generation for continuous-time stochastic domains with concurrency
Reid G. Simmons
Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling, AAAI Press, Menlo Park, California (2004), pp. 325-333
A framework for planning in continuous-time stochastic domains
David J. Musliner
Reid G. Simmons
Proceedings of the Thirteenth International Conference on Automated Planning and Scheduling, AAAI Press, Menlo Park, California (2003), pp. 195-204
VHPOP: Versatile heuristic partial order planner
Reid G. Simmons
Journal of Artificial Intelligence Research, vol. 20 (2003), pp. 405-430
On the role of ground actions in refinement planning
Reid G. Simmons
Proceedings of the Sixth International Conference on Artificial Intelligence Planning and Scheduling Systems, AAAI Press, Menlo Park, California (2002), pp. 54-61
Probabilistic verification of discrete event systems using acceptance sampling
Reid G. Simmons
Proceedings of the 14th International Conference on Computer Aided Verification, Springer, Berlin / Heidelberg (2002), pp. 223-235
Coordination for multi-robot exploration and mapping
Reid G. Simmons
David Apfelbaum
Wolfram Burgard
Dieter Fox
Mark Moors
Sebastian Thrun
Proceedings of the Seventeenth National Conference on Artificial Intelligence, AAAI Press, Menlo Park, California (2000), pp. 852-858
A deterministic algorithm for solving imprecise decision problems
Love Ekenberg
Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference, AAAI Press, Menlo Park, California (2000), pp. 313-317
Artificial decision making under uncertainty in intelligent buildings
Magnus Boman
Paul Davidsson
Proceedings of the Fifteenth Conference on Uncertainty in Artificial Intelligence, Morgan Kaufmann Publishers, San Francisco, California (1999), pp. 65-70
