Håkan L. S. Younes

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.
Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    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
    Reid G. Simmons
    Information and Computation, 204(2006), pp. 1368-1409
    Preview abstract Probabilistic verification of continuous-time stochastic processes has received increasing attention in the model-checking community in the past five years, with a clear focus on developing numerical solution methods for model checking of continuous-time 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. We present a statistical approach to probabilistic model checking, employing hypothesis testing and discrete-event simulation. 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. View details
    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
    Preview abstract We introduce a framework for expressing correctness guarantees of model-checking algorithms. The framework allows us to qualitatively compare different solution techniques for probabilistic model checking, both techniques based on statistical sampling and numerical computation of probability estimates. We provide several new insights into the relative merits of the different approaches. In addition, we present a new statistical solution method that can bound the probability of error under any circumstances by sometimes reporting undecided results. Previous statistical solution methods could only bound the probability of error outside of an ``indifference region.'' View details
    Numerical vs. statistical probabilistic model checking
    Marta Kwiatkowska
    Gethin Norman
    David Parker
    International Journal on Software Tools for Technology Transfer, 8(2006), pp. 216-228
    Preview abstract Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare the two solution techniques when applied to the verification of time-bounded until formulae in the temporal stochastic logic CSL, both theoretically and through empirical evaluation on a set of case studies. Our study differs from most previous comparisons of numerical and statistical approaches in that CSL model checking is a hypothesis-testing problem rather than a parameter-estimation problem. We can therefore rely on highly efficient sequential acceptance sampling tests, which enables statistical solution techniques to quickly return a result with some uncertainty. We also propose a novel combination of the two solution techniques for verifying CSL queries with nested probabilistic operators. View details
    Ymer: A statistical model checker
    Proceedings of the 17th International Conference on Computer Aided Verification, Springer, Berlin / Heidelberg(2005), pp. 429-433
    Preview abstract We present Ymer, a tool for verifying probabilistic transient properties of stochastic discrete event systems. Ymer implements both statistical and numerical model checking techniques. We focus on two features of Ymer: distributed acceptance sampling and statistical model checking of nested probabilistic statements. View details
    Probabilistic verification for ``black-box'' systems
    Proceedings of the 17th International Conference on Computer Aided Verification, Springer, Berlin / Heidelberg(2005), pp. 253-265
    Preview abstract We explore the concept of a ``black-box'' stochastic system, and propose an algorithm for verifying probabilistic properties of such systems based on very weak assumptions regarding system dynamics. Properties are expressed as formulae in a probabilistic temporal logic. Our presentation is a generalization of and an improvement over recent work by Sen et al. on probabilistic verification for ``black-box'' systems. View details
    The first probabilistic track of the international planning competition
    Michael L. Littman
    David Weissman
    John Asmuth
    Journal of Artificial Intelligence Research, 24(2005), pp. 851-887
    Preview abstract The 2004 International Planning Competition, IPC-4, included a probabilistic planning track for the first time. We describe the new domain specification language we created for the track, our evaluation methodology, the competition domains we developed, and the results of the participating teams. View details
    Planning and execution with phase transitions
    Proceedings of the Twentieth National Conference on Artificial Intelligence, AAAI Press, Menlo Park, California(2005), pp. 1030-1035
    Preview abstract We consider a special type of continuous-time Markov decision processes (MDPs) that arise when phase-type distributions are used to model the timing of non-Markovian events and actions. We focus, primarily, on the execution of phase-dependent policies. Phases are introduced into a model to represent relevant execution history, but there is no physical manifestation of phases in the real world. We treat phases as partially observable state features and show how a belief distribution over phase configurations can be derived from observable state features through the use of transient analysis for Markov chains. This results in an efficient method for phase tracking during execution that can be combined with the $Q_\mbox{MDP}$ value method for POMDPs to make action choices. We also discuss, briefly, how the structure of MDPs with phase transitions can be exploited in structured value iteration with symbolic representation of vectors and matrices. View details
    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
    Preview abstract Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare the two solution techniques when applied to the verification of time-bounded until formulae in the temporal stochastic logic CSL. This study differs from most previous comparisons of numerical and statistical approaches in that CSL model checking is a hypothesis testing problem rather than a parameter estimation problem. We can therefore rely on highly efficient sequential acceptance sampling tests, which enables statistical solution techniques to quickly return a result with some uncertainty. This suggests that statistical techniques can be useful as a first resort during system prototyping, rather than as a last resort as often suggested. We also propose a novel combination of the two solution techniques for verifying CSL queries with nested probabilistic operators. View details
    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
    Preview abstract We adopt the framework of Younes, Musliner, and Simmons for planning with concurrency in continuous-time stochastic domains. Our contribution is a set of concrete techniques for policy generation, failure analysis, and repair. These techniques have been implemented in TEMPASTIC, a novel temporal probabilistic planner, and we demonstrate the performance of the planner on two variations of a transportation domain with concurrent actions and exogenous events. TEMPASTIC makes use of a deterministic temporal planner to generate initial policies. Policies are represented using decision trees, and we use incremental decision tree induction to efficiently incorporate changes suggested by the failure analysis. View details
    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
    Preview abstract We consider a general model of stochastic discrete event systems with asynchronous events, and propose to develop efficient algorithms for verification and control of such systems. View details
    VHPOP: Versatile heuristic partial order planner
    Reid G. Simmons
    Journal of Artificial Intelligence Research, 20(2003), pp. 405-430
    Preview abstract VHPOP is a partial order causal link (POCL) planner loosely based on UCPOP. It draws from the experience gained in the early to mid 1990's on flaw selection strategies for POCL planning, and combines this with more recent developments in the field of domain independent planning such as distance based heuristics and reachability analysis. We present an adaptation of the additive heuristic for plan space planning, and modify it to account for possible reuse of existing actions in a plan. We also propose a large set of novel flaw selection strategies, and show how these can help us solve more problems than previously possible by POCL planners. VHPOP also supports planning with durative actions by incorporating standard techniques for temporal constraint reasoning. We demonstrate that the same heuristic techniques used to boost the performance of classical POCL planning can be effective in domains with durative actions as well. The result is a versatile heuristic POCL planner competitive with established CSP-based and heuristic state space planners. View details
    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
    Preview abstract We propose a framework for policy generation in continuoustime stochastic domains with concurrent actions and events of uncertain duration. We make no assumptions regarding the complexity of the domain dynamics, and our planning algorithm can be used to generate policies for any discrete event system that can be simulated. We use the continuous stochastic logic (CSL) as a formalism for expressing temporally extended probabilistic goals and have developed a probabilistic anytime algorithm for verifying plans in our framework. We present an efficient procedure for comparing two plans that can be used in a hill-climbing search for a goal-satisfying plan. Our planning framework falls into the Generate, Test and Debug paradigm, and we propose a transformational approach to plan generation. This relies on effective analysis and debugging of unsatisfactory plans. Discrete event systems are naturally modeled as generalized semi-Markov processes (GSMPs). We adopt the GSMP as the basis for our planning framework, and present preliminary work on a domain independent approach to plan debugging that utilizes information from the verification phase. View details
    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
    Preview abstract Less than a decade ago, the focus in refinement planning was on partial order planners using lifted actions. Today, the currently most successful refinement planners are all state space planners using ground actions -- i.e. actions where all parameters have been substituted by objects. In this paper, we address the role of ground actions in refinement planning, and present empirical results indicating that their role is twofold. First, planning with ground actions represents a bias towards early commitment of parameter bindings. Second, ground actions help enforce joint parameter domain constraints. By implementing these two techniques in a least commitment planner such as UCPOP, together with using an informed heuristic function to guide the search for solutions, we show that we often need to generate far fewer plans than when planning with ground action, while the number of explored plans remains about the same. In some cases a vast reduction can also be achieved in the number of explored plans. View details
    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
    Preview abstract We propose a model independent procedure for verifying properties of discrete event systems. The dynamics of such systems can be very complex, making them hard to analyze, so we resort to methods based on Monte Carlo simulation and statistical hypothesis testing. The verification is probabilistic in two senses. First, the properties, expressed as CSL formulas, can be probabilistic. Second, the result of the verification is probabilistic, and the probability of error is bounded by two parameters passed to the verification procedure. The verification of properties can be carried out in an anytime manner by starting off with loose error bounds, and gradually tightening these bounds. View details
    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
    Preview abstract Today there are numerous tools for decision analysis, suitable both for human and artificial decision makers. Most of these tools require the decision maker to provide precise numerical estimates of probabilities and utilities. Furthermore, they lack the capability to handle inconsistency in the decision models, and will fail to deliver an answer unless the formulation of the decision problem is consistent. In this paper we present an algorithm for evaluating imprecise decision problems expressed using belief distributions, that also can handle inconsistency in the model. The same algorithm can be applied to decision models where probabilities and utilities are given as intervals or point values, which gives us a general method for evaluating inconsistent decision models with varying degree of expressiveness. View details
    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
    Preview abstract This paper addresses the problem of exploration and mapping of an unknown environment by multiple robots. The mapping algorithm is an on-line approach to likelihood maximization that uses hill climbing to find maps that are maximally consistent with sensor data and odometry. The exploration algorithm explicitly coordinates the robots, based on estimates of expected information gain at different locations. It tries to maximize overall utility by minimizing the potential for overlap in information gain amongst the various robots. For both the exploration and mapping algorithms, most of the computations are distributed. The techniques have been tested extensively in real-world trials and simulations. The results demonstrate the performance improvements and robustness that accrue from our multi-robot approach to exploration. View details
    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
    Preview abstract Our hypothesis is that by equipping certain agents in a multi-agent system controlling an intelligent building with automated decision support, two important factors will be increased. The first is energy saving in the building. The second is customer value---how the people in the building experience the effects of the actions of the agents. We give evidence for the truth of this hypothesis through experimental findings related to tools for artificial decision making. A number of assumptions related to agent control, through monitoring and delegation of tasks to other kinds of agents, of rooms at a test site are relaxed. Each assumption controls at least one uncertainty that complicates considerably the procedures for selecting actions part of each such agent. We show that in realistic decision situations, room-controlling agents can make bounded rational decisions even under dynamic real-time constraints. This result can be, and has been, generalized to other domains with even harsher time constraints. View details