· I successfully defended my dissertation in April. A copy will be available here soon!
· Our paper Theory and techniques for synthesizing efficient breadth-first search algorithms has been accepted to Formal Methods, 2012
· Cost-Based Learning in Planning (presented at the Workshop on Planning and Learning, Intl. Conf. On Planning and Scheduling, 2011)
The goal of my research in program synthesis is to investigate ways in which efficient scalable search algorithms can be constructed from formal specifications by a competent designer, with mechanical assistance. Search algorithms cover not just traditional graph and string algorithms found in textbooks but also combinatorially hard problems such as planning and scheduling. It is not the same as automatic programming, which seeks to automatically generate code from specifications.
The particular approach that I follow was developed by Doug Smith at Kestrel Institute, and I refer to it as guided program synthesis. In order to synthesize a program from a given specification, the developer picks an appropriate algorithm class from a library of algorithm classes (such as Global Search, Local Search, Divide and Conquer, Fixpoint Iteration, etc.). Each algorithm class has a program schema with operators that must be instantiated by the developer in accordance with the axioms of the class. The result is a correct but inefficient algorithm that meets the given specification. It is transformed into an efficient algorithm by the application of program transformations such as finite differencing, partial evaluation, and context-dependent simplification. Finally, a backend code generator spits out code in a chosen target language. Support for this style of program development is provided by the Specware toolset from Kestrel. This correct-by-construction approach via instantiation of specific operators is to be contrasted with the stepwise verification-based refinement of entire programs in formal methods such as Z and B.
1. The first contribution of my dissertation is a solution to the problem of how to carry out breadth-first search efficiently (mainly space). This characterization, which we call efficient breadth-first search (EBFS) is based on dominance relations. Greedy and Quasi-greedy algorithms fall out as specializations of EBFS. The surprising result here is that this characterization of greedy algorithms is broader than the existing well-known characterization using the Greedy Algorithm of Edmonds parameterized over algebraic structures called greedoids.
2. I strongly believe that every formal approach should be accompanied by a methodology by which it can be used by a competent and knowledgeable developer, and not require a PhD in mathematics or leaps of insight. The second contribution of my work is therefore some techniques for systematically deriving dominance relations without rabbits (Dijkstra’s term for steps that appear magically out of nowhere) and how to demonstrate that the resulting dominance relations satisfy the requirements for the resulting algorithm to be greedy.
3. The third contribution is showing how to apply these ideas to the synthesis of fast domain-specific planners. Nearly all the state-of-the-art planners in the planning literature are heuristic domain-independent planners. They generally do not scale well and their space requirements also become quite prohibitive. The key to scalable planners is to incorporate domain-specific information. Planners such as TLPlan that incorporate domain-specific information in the form of control rules are orders of magnitude faster. However, devising the control rules is a labor-intensive task and requires domain expertise and insight. The correctness of the rules is also not guaranteed. We introduce a method by which domain-specific dominance relations can be systematically derived, which can then be turned into control rules, and demonstrate the method on a planning problem (Logistics). The approach relies on a novel action landmark discovery algorithm described in my dissertation.
There are a number of exciting ways in which to extend this work which I am hoping to pursue
Although the effort required to instantiate the various operators in guided program synthesis is much less than in standard refinement based approaches, it would be nice to provide machine assistance to developer. Fortunately the calculations required to carry out the instantiation are often straightforward enough to be automated. A predecessor to Specware, called KIDS, had this capability with a constructive theorem prover that was able to derive antecedents, as well as derive interesting consequents of first-order formulas. I am interested in resuscitating this as well as augmenting its capability to include the kinds of calculations that are needed to derive dominance relations. Much of the recent advance in program synthesis (e.g. see From Program Verification to Program Synthesis) can be attributed to the ability to automate the instantiation of program fragments using powerful SAT and SMT solvers. Some of the theories built into SMT solvers are also very useful for us.
In almost all practical situations, there will be uncertainty. In some earlier work I showed how to eliminate the uncertainty in some situations using quantifier elimination. However such approaches in general result in overly conservative solutions. More generally, we can view the situation as a system in which various players or agents interact. There are controllable players and uncontrollable ones (e.g. the environment or adversaries). This falls under the general category of reactive systems, of which discrete controllers are another example. To solve the problem using synthesis, we need to determine a refinement of the controllable players such that in the resulting algorithm, the goal is met. This will require extending the framework of Global Search but some of the groundwork for this has already been done. Applications of this work are in
· Scheduling multimedia and hypermedia documents (components of the documents have uncertain durations)
· Process and job-shop scheduling (varying processing time due to processor load)
· Conditional planning (uncertainty in the outcome of the environment's actions)
For many problems, an optimal solution is very difficult to obtain, if not unknown, even for relatively modest sized inputs. For example the 20x20 Job-Shop Problem (schedule 20 jobs, each consisting of 20 tasks) remains unsolved, over 20 years after the 10x10 problem was solved (which itself remained unsolved for almost 30 years). For problems in which the search for an optimal solution is computationally infeasible, a better alternative might be to first quickly find a reasonable/acceptable feasible solution, and then rewrite that solution into a more efficient (possibly optimal) one. The arrangement is similar to how a compiler first generates code and then applies optimizations to it. I have identified problem subclasses for which we can do this efficiently but there is more to be done. Applications of this work are in
· Combined planning and scheduling problems (most real world planning problems are in this category)
· Efficiently mapping abstract models to target architectures (e.g. allocating processes to processors while respecting resource requirements)
· Theory and techniques for synthesizing efficient breadth-first search algorithms, 18th Intl. Symp. on Formal Methods 2012
· Cost-Based Learning in Planning, 3rd Workshop on Planning and Learning, ICAPS, 2011
· A Class of Greedy Algorithms and its Relation to Greedoids, Intl. Colloq. On Theoretical Aspects of Computing (ICTAC), 2010
· Synthesis of Greedy Algorithms Using Dominance Relations, 2nd NASA Symposium on Formal Methods (NFM), 2010
· Synthesis of Fast Programs for Maximum Segment Sum Problems, Generative Programming and Component Engineering (GPCE), 2009
· Tactical Synthesis of Efficient Global Search Algorithms, 1st NASA Symposium on Formal Methods (NFM), 2009
· Tactic-Driven Synthesis of Global Search Algorithms Based on Constraint Satisfaction, Middle Earth Programming Languages Seminar (MEPLS), 2009
· Handling Uncertainty in Job-Shop Scheduling, 1st International Workshop on Living with Uncertainty (IWLU), 2007
· Modeling Interactions in Feature Oriented Software Designs, in Feature Interactions in Telecommunications and Software Systems VIII, IOS Press, 2005.
· Specializing and Optimizing Declarative Domain Models, The 4th OOPSLA Workshop on Domain-Specific Modeling, October 2004
· Transforming Declarative Models Using Patterns in MDA, The OOPSLA Workshop on Best Practices for Model Driven Software Development, October 2004
Here are my notes from the 2009 Summer School on Planning and Scheduling. I will update these on an ongoing basis as I learn more about the subject. Please let me know if you find them useful or see anything wrong or missing. Also, note that they constitute a personal view of the field and thus should not be taken to be survey of the field or anything of that sort!
· Full AAAI award to attend the 2009 and 2011 Summer Schools in Planning and Scheduling
· Award to participate in the Doctoral Symposium at ICAPS 2011
I have over 12 years experience in the tech industry, having worked as a Member of Technical Staff at Oracle Corp., an Architect at Evolve Software (a now defunct startup), both in the Bay Area, and as a Domain Engineer at Semantic Designs in Austin, Texas. I returned to the University of Texas at Austin to pursue my PhD. In 2006, I was an intern at NASA Ames with Ewen Denney on the AutoBayes and AutoFilter program generators.
· Post-graduate Student, Computer Laboratory, Cambridge, England
· BSc. (Honours), Dept. of Computer Science, Manchester University, England
· I organize the Synthesis reading group at UT
· I enjoy Swing Dancing
You are visitor number