Program Synthesis is about constructing or synthesizing correct, performant programs
from formal specifications. It is the other side of the coin from Program Verification.
Instead of verifying a program after the fact, synthesis aims to construct a program
which is guaranteed to be correct with respect to the specification. The approach has been used
to construct, for example, efficient scheduling algorithms, planners, reactive robot controllers,
bus controllers for real-world problems.
My PhD was in a specific area of program synthesis,
called algorithm synthesis.
Currently I am working on applying program synthesis to the problem of synthesizing
programs for robot planning and control.
Some interesting research topics are:
Robot Plan Synthesis
The planning problem for robotics involves both motion and task planning.
Simply handing a task plan over to the motion planner does not work because of
possible infeasibility of the task plan at the physical level. Extending OTS heuristic
planners (such as FF)
to include motion planning is also difficult because of the blow-up in the
size of the input. There is also useful task ordering information that is known
to the programmer which would significantly reduce the search space that cannot be
easily supplied to an automated planner. In addition constraints on the solution (such
as the limits on the lengths or clearances of the paths the robot takes, regions
it must avoid, fuel limits, etc.) are
difficult to express in standard planning domain languages such as PDDL, let alone
for standard heuristic planners to solve. We have introduced a novel approach that represents the underlying
motion planning space using an abstraction of manipulation graphs we call placement
graphs, as well as language in which the programmer can supply a plan outline. We derive
a set of constraints from the plan outline and placement graph which are solved.
The solution is then used to flesh out the plan outline.
Our work is described in a paper we have
submitted to ICRA 2014
Reactive Systems
Classical planning has treated planning as a one-shot problem in which a
planning problem definition and a goal are fed to a planner which returns a plan.
Increasingly, though, planning is being applied to real-world problems in which the
environment can change and goals are ongoing or maintenance goals. This is called
reactivity. There is ongoing research
in synthesizing controllers from temporal logic specifications which can handle
such situations. However, due to the
complexity of the approach (doubly exponential in the size of the specification),
scalability remains a problem. Handling infinite spaces (caused by numeric
constraints) is also difficult. We are looking at extending our plan outline approach
to such cases.
Optimization
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 an 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 shown how the rewrite rules that carry out such an
optimization can be automatically learned for Planning problems.
|