Calin Belta: Automatic deployment of robotic teams from temporal logic specifications

The existing approaches to motion planning and control for
multi-agent mobile systems have two main limitations. First, the
specification language is not rich enough, and only allows for "Go
from R1 to R2 and avoid obstacles". However, in several robotic
applications, "rich" temporal and logic statements about the
reachability of regions of interest are necessary, e.g., "Always avoid R4. Visit R1 or R2 and then go to R3 and stay there for all
future times. After R3 is occupied, start visiting R2 and R5, in
this order, infinitely often.” Second, most of the existing
approaches for robotic teams are bottom-up. In other words, they
show that local interaction rules induce interesting global
behavior. However, the inverse problem seems more relevant to
robotics: Can we automatically synthesize provably correct control
and communication strategies from rich, global specifications? In
this talk, I will present some preliminary answers to this
question.

Julia Braman: Safety Verification of Goal-based Control Programs for Autonomous Robotic Systems

Fault-tolerant control programs for autonomous robotic systems use conditional branching based on system states, which adds robustness and complexity to the plan. Goal networks are control programs based on intent and constraints on the state space that naturally allow different control tactics to be explored in a fault-tolerant manner. A method has been created to automatically verify these goal networks versus unsafe sets of conditions on the system state. Uncertainty in the system's state due to noisy measurements can induce failures even in verified control programs; in this case, a failure probability for the goal network can be calculated. An example control program for an autonomous robotic aerobot probe to Titan, a moon of Saturn, is analyzed using these verification procedures.

Magnus Egerstedt:  Motion description languages for multi-robot systems: From specifications to optimal control

In order to simplify, reuse, and verify the control design for complex robot navigation tasks, a divide-and-conquer approach has emerged as a possible solution. The main idea is to identify a number of control modes, defined with respect to particular tasks, sensory sources, or operating points, and then combine these modes together in a suitable manner. Moreover, when dealing with multi-robot systems, the inter-robot dependencies must be incorporated into the mode descriptions as well in order to describe the needed communications resources and specify the coordination laws. This work focuses on three particular challenges in this area, namely 1) the definition of a so-called "networked motion description language" (MDLn) for specifying high-level control programs for group interactions by creating multi-modal executions of the system through a concatenation of modes, 2) the creation of suitable, tokenized control modes from empirical data, and 3) computational algorithms for optimal mode concatenation. Applications in robotics and biological systems (including groups of ants and schooling fish) will be examined and related to the theoretical developments.

Lydia Kavraki: Falsification of Safety Properties expressed in Linear Temporal Logic in Hybrid Systems

Our recent work has proposed a multi-layered approach for hybrid-system falsification that combines motion planning with discrete search and discovers safety violations by computing witness trajectories to unsafe states. The discrete search uses the discrete hybrid system transitions and a state-space decomposition to guide the motion planner during the search for witness trajectories. This talk will discuss how the above methodology can be combined with model checking for the falsification of safety properties specified by syntactically safe linear temporal logic formulas for the case of hybrid systems with general nonlinear dynamics and input controls.

Joint work with E. Plaku and M. Vardi.

Eric Klavins: Stochastic, concurrent programs for reconfigurable robot systems

We consider sets of guarded commands distributed among modules of a reconfigurable system. To each command is associated a probabilistic rate, so that the entire system can be modeled as a stochastic process similar to a low-copy-number chemical reaction network. In this framework, we show how to represent novel algorithms that allow reconfigurable robots to "digest" structures and rebuild them. A key feature of the system is that we can specify the degree to which a deterministic algorithm can be relaxed into a probabilistic one. This allows for probabilistically guaranteed completion of the algorithms under various fault models.

Joint work with Nils Napp, Steve Safarik and Fayette Shaw

Hadas Kress-Gazit: Synthesizing controllers for reactive tasks

Robots move and act in dynamically changing environments and as such they must react to different situations they encounter. To make robots useful and safe, their reactions must be correct with respect to some user-specified high level behavior. In this work, temporal logic is used to define reactive, high level, correct behavior for the robot such as “whenever you see a person, follow them” or “if your battery is running low, go back home and recharge”. Synthesis techniques together with control primitives are then used to generate hybrid controllers that are guaranteed to make the robot achieve its high level goals.

Sayan Mitra: Virtual Infrastructure for Programming Mobile Robots

Developing coordination-based systems for mobile robots can be quite challenging owing to the dynamic and unpredictable nature of the environment: robots may be continuously joining and leaving the system, and furthermore, wireless communication is notoriously unreliable due to collisions, contention, and various wireless interference. We describe how virtual infrastructure can be used for programming complex coordination tasks for mobile robots. As an example, we illustrate how to coordinate the motion of mobile robots in a 2-dimensional plane in the presence of dynamic changes in the underlying mobile ad hoc network, i.e., nodes joining, leaving, or failing. The robots cooperate to implement a virtual stationary automaton (VSA) Layer based on replicated state machines. Each VSA is a special type of Timed Automaton and is associated with each region of the plane. The VSAs coordinate among themselves to distribute the robots as needed throughout the plane. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane and yet will reach a suitable location within bounded time. Self-stabilization also ensures, for example, that the robots can adapt to changes in the desired formation.

Claire Tomlin: Hierarchical, hybrid architecture for robot motion planning and control

Recent advances in research and technology have enabled robots to accomplish tasks that were unimaginable even ten years ago. Before robots can be integrated into mainstream society, however, additional work is required to be able to prove that they will always act as desired, even in uncertain and varying conditions. In this talk, we will present some of the latest research being done in this area by the Berkeley Hybrid Systems Lab using the STARMAC quadrotor platform. By using tools from a wide variety of areas, including hybrid control theory, machine learning, and systems optimization, we have developed novel techniques for path planning, modeling and control of a quadrotor through complex maneuvers, and frameworks for human-robot cooperative task completion. Although much of this work is still in development, we believe that it shows promise for the end goal of provably safe robot operations.