Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Robotic Controllers

Theme Leaders: Hadas Kress-Gazit (Cornell) and Lydia Kavraki (Rice)

Imagine a robot waiter having to surve customers with plates. Can we formalize its specification and automatically synthesize his behavior? How can he cope with the different data on the menu? If another waiter robot broke a glass, can he avoid trumpling over it on his way to the kitchen? How can we design it in a composite way, leveraging working provable subcomponents?

Design of robotic systems, being complete autonomous machines, involves many facets that are absent in the design of other computerized systems. The robotics theme thus present new challenges for automatic synthesis as envisioned by ExCAPE. Motion planning is a prominent example. ExCAPE researchers have developed an open source motion planning library implementing motions solvers that allow the satisfaction of a high level specification while at the same time ensuring a feasible robot motion plan is produced. Other researched areas include synthesis in partially unknown environments, syntheis with costs, synthesis with complex dynamics, and synthesis for multi-robot motion planning.

Synthesis with Costs

PI: Kress-Gazit (Cornell)

We address the problem of synthesizing optimal robot controllers for adversarial environments. Our main observation is that the quality of a path to a goal has two dimensions: (1) the number of phases in which the robot waits for the environment to perform some actions and (2) the cost of the robot’s actions to reach the goal. Our synthesis algorithm can take any prioritization over the possible cost combinations into account, and computes the optimal strategy in a symbolic manner, despite the fact that the action costs can be non-integer [JK13,JEK13].

Synthesis for Robots with Complex Dynamics

PIs: Kress-Gazit (Cornell) and Tabuada (UCLA)

In one approach to synthesizing a reactive control software for robots with complex dynamics, we developed an automatic construction of low-level controllers that ensure the correct continuous execution of a highlevel mission plan. Controllers are generated using trajectory-based verification to produce a set of robust reach tubes which strictly guarantee that the required motions achieve the desired task specification. Reach tubes, computed here by solving a series of sum-of-squares optimization problems, are composed in such a way that all trajectories ensure correct high-level behaviors [HK13]. In a second approach to the problem, we incorporated into the synthesis process an automatically generated abstraction of the robot dynamics. Thus if the controller can be synthesized, the behavior will be correct. We then examined how to provide revisions to the specifications when the dynamics of the robot cause the specification to be unrealizable.

Synthesis for Arbitrary Action Durations

PI: Kress-Gazit (Cornell)

We reason about how to synthesize and execute robot controllers for robots with different actions that are not instantaneous, so that the continuous execution is correct with respect to the specification no matter which action completes first. We have shown how this methods generalizes to multi robot tasks [RPK13,RK14].

Synthesis with Identifiers

PIs: Kress-Gazit (Cornell) and Seshia (Berkeley)

We consider the synthesis of reactive systems from specifications with identifiers. Identifiers are useful to parametrize the input and output of a reactive system, for example, to state which client requests a grant from an arbiter, or the type of object that a robot is expected to fetch. Traditional reactive synthesis algorithms only handle a constant bounded range of such identifiers. However, in practice, we might not want to restrict the number of clients of an arbiter or the set of object types handled by a robot a priori. We first present a concise automata-based formalism for specifications with identifiers. The synthesis problem for such specifications is undecidable. We therefore give an algorithm that is always sound, and complete for unrealizable safety specifications. Our algorithm is based on computing a pattern-based abstraction of a synthesis game that captures the realizability problem for the specification. The abstraction does not restrict the possible solutions to finite-state ones and captures the obligations for the system in the synthesis game [ESK14].

Robot Plan Synthesis in Partially-Unknown Environments

PIs: Kavraki (Rice), Kress-Gazit (Cornell) and Vardi (Rice)

We address the problem of robot plan synthesis in partially-unknown environments by combining a multi-layered synergistic framework with an iterative planning strategy [MLKKV13]. The approach employs the synergistic planning framework, which can handle complex dynamical systems, to generate continuous robotic trajectories that satisfy a given temporal logic specification. Once an unknown environment feature is encountered during the execution of the trajectory, the synergistic framework is called again to generate a new plan from the current state of the robot. The replanning step is fast because the expensive computations related to the temporal logic specification do not need to be repeated. In this approach, the planner deals with the unknown features only when they are discovered. In the case that the discovered feature renders the specification unsatisfiable, the planner uses a satisfaction metric to generate a trajectory that satisfies the specification as closely as possible. Case studies on a second-order car-like robot in an office environment with unknown obstacles illustrate the efficacy of the framework. In all the case studies, the planner successfully synthesized optimal robot trajectories with respect to the satisfaction metric of the specification.

Platform-based Design for Robot programming

PIs: Pappas (Penn), Sangiovanni-Vincetelli (UC Berkeley), and Tabuada (UCLA)

Platform-based design means that the design proceeds in a double direction: (A) bottom-up: this is the direction that allows the designer to build the platform library, choosing the abstractions of functionalities and performance from a given architectural space; (B) top-down: in this direction, the design composes the library elements in order to define a specific function. This is a mapping process. Usually, in the top-down approach, the designer tries to compose a specific solution in an iterative way. Once he has arranged a possible implementation, he evaluates the performance information that the platform components of the library provide at that level and, eventually, he/she proceeds with additional iterations until the implementation meets the desired performance. Always in the top-level direction, if there is the need of specifuc platform elements that are not available at that time, the designer is allowed to instantiate new platform blocks through the definition of placeholders, that are added to the library and implemented in the lower level of abstraction in a second time. In order to avoid large-loop iterations, it is possible to define more platforms at different layers of abstraction. This process, that bring at the definition of a platform stack, is the key of the PBD. In the restaurant waiter scenario, some steps have been taken to meet the PBD principles. The first step is to define the basic functionalities that the robot is equipped with. This requires extrapolation of some information from the physical level in order to build the library of components. These elements from the lowest level include some physical quantities that could be useful in the design process (for example, energy, precision, time). We are also working to find a "common language" for guaranteeing that all the synthesis groups can interface correctly with the motion planner.

Plan Synthesis for Stochastic Systems

PI: Kavraki (Rice)

The problem of planning for robots with action uncertainty from high-level task descriptions is considered in this project. The main objective is to develop a framework that efficiently synthesizes optimal policies for uncertain systems to satisfy a temporal logic specification with maximum probability. To achieve this objective, the evolution of the stochastic system is first abstracted to a discrete, bounded-parameter Markov decision process (BMDP). The procedure is automated by algorithmic discretization of the system's states space and computation of optimal local policies enabling the system to transit between neighboring discrete regions [LLMK14a, LLMK14b]. Then, a global control policy over the product of the BMDP abstraction and the DFA representing the specification is generated. Analysis of the framework reveals that as the resolution of the abstraction becomes finer, the global policy converges to optimal [LLMK14c]. Simulated experiments confirm the theoretical results and illustrate that high-quality policies can be obtained in seconds, orders of magnitude faster than existing methods.

Compositional Multi-Robot Motion Planning

PIs: Pappas (Penn) and Seshia (Berkeley)

We consider the problem of compositional motion planning for multi-robot systems [SRKPS14]. Given the runtime behavior of a group of robots, specified using a set of safe LTL properties, the goal is to synthesize the robots motion plan. Our method relies on a library of motion primitives that provides a set of controllers to be used to control the behavior of the robots in different configurations. Using the closed loop behavior of the robots under the action of different controllers, we formulate the motion planning problem as a constraint solving problem and use an off-the-shelf satisfiability modulo theories (SMT) solver to solve the constraints and generate trajectories for the individual robot. Our approach can also be extended to synthesize optimal cost trajectories where optimality is defined with respect to the available motion primitives. Experimental results show that this framework has potential to solve complex motion planning problems in the context of multi-robot systems. See here the tool, ComPlan, devloped for this task, and a short video.

Collision Avoidance in Vehicular Systems

PI: Lafortune (Michigan)

We are investigating the problem of supervisory control of vehicular networks for collision avoidance at intersections. Our efforts in the past year have been focused on the case of imperfect measurement in the position of the vehicles. Our approach to this problem is to use abstraction techniques for modeling a set of vehicles as a discrete event system, using controllable and uncontrollable events to model control actions, uncontrolled vehicles, and a disturbance. We have shown that this modeling formalism can also be used to incorporate measurement uncertainty by adding another class of observable but uncontrollable events to model measurement. To deal with the fact that the set of measurements are a subset of a continuous rather than a discrete space, we partitioned the set of continuous measurements into a set of equivalence classes (determined with respect to the spatial discretization of the abstraction), and defined an observable but uncontrollable event corresponding to each equivalence class. The same techniques can be extended to other robotic systems, which typically have to deal with the same complicating factors, namely disturbances, uncontrollable environments, and measurement uncertainty [DCDL13,DL14].

Developing Realizable Temporal Logic Specifications

PI: Alur (Penn)

The reactive synthesis problem is to find a finite-state controller that satisfies a given temporal-logic specification regardless of how its environment behaves. Developing a formal specification is a challenging and tedious task and initial specifications are often unrealizable. In many cases, the source of unrealizability is the lack of adequate assumptions on the environment of the system. In this paper, we consider the problem of automatically correcting an unrealizable specification given in the generalized reactivity (1) fragment of linear temporal logic, by adding assumptions on the environment. When a temporal-logic specification is unrealizable, the synthesis algorithm computes a counter-strategy as a witness. Our algorithm then analyzes this counter-strategy and synthesizes a set of candidate environment assumptions that can be used to remove the counter-strategy from environment's possible behaviors. We demonstrate the applicability of our approach with several examples and case studies from the robotics domain [AMT13].

Tools and Projects:
  • LTLMoP: Linear Temporal Logic MissiOn Planning
  • OMPL: The Open Motion Planning Library
  • ComPlan: Compositional motion planning for multi-robot systems

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996