TechTalks from event: Technical session talks from ICRA 2012

Conference registration code to access these videos can be accessed by visiting this link: PaperPlaza. Step-by-step to access these videos are here: step-by-step process .
Why some of the videos are missing? If you had provided your consent form for your video to be published and still it is missing, please contact

Formal Methods

  • Temporal Logic Motion Control Using Actor-Critic Methods Authors: Ding, Xu Chu; Wang, Jing; Lahijanian, Morteza; Paschalidis, Yannis; Belta, Calin
    In this paper, we consider the problem of deploying a robot from a specification given as a temporal logic statement about some properties satisfied by the regions of a large, partitioned environment. We assume that the robot has noisy sensors and actuators and model its motion through the regions of the environment as a Markov Decision Process (MDP). The robot control problem becomes finding the control policy maximizing the probability of satisfying the temporal logic task on the MDP. For a large environment, obtaining transition probabilities for each state-action pair, as well as solving the necessary optimization problem for the optimal policy are usually not computationally feasible. To address these issues, we propose an approximate dynamic programming framework based on a least-square temporal difference learning method of the actor-critic type. This framework operates on sample paths of the robot and optimizes a randomized control policy with respect to a small set of parameters. The transition probabilities are obtained only when needed. Hardware-in-the-loop simulations confirm that convergence of the parameters translates to an approximately optimal policy.
  • Robust Multi-Robot Optimal Path Planning with Temporal Logic Constraints Authors: Ulusoy, Alphan; Smith, Stephen L.; Ding, Xu Chu; Belta, Calin
    In this paper we present a method for automatically planning robust optimal paths for a group of robots that satisfy a common high level mission specification. Each robot's motion in the environment is modeled as a weighted transition system, and the mission is given as a Linear Temporal Logic (LTL) formula over a set of propositions satisfied by the regions of the environment. In addition, an optimizing proposition must repeatedly be satisfied. The goal is to minimize the maximum time between satisfying instances of the optimizing proposition while ensuring that the LTL formula is satisfied even with uncertainty in the robots' traveling times. We characterize a class of LTL formulas that are robust to robot timing errors, for which we generate optimal paths if no timing errors are present, and we present bounds on the deviation from the optimal values in the presence of errors. We implement and experimentally evaluate our method considering a persistent monitoring task in a road network environment.
  • Stunt Driving via Policy Search Authors: Lau, Tak Kit; Liu, Yunhui
    To explore or exploit? In this paper, we discuss the long-standing exploration-exploration dilemma in context of designing a learning controller for stunt-style driving with scarce samples. By making an efficient use of a single demonstration by an expert, our algorithm leverages our intuitive understanding of driving to extract a coarse dynamics model from the collected driving data, then formulate the policy search in a setting of gradient update with a specially designed cost function. Both theoretical and empirical results are detailed and discussed.
  • Probabilistic Control from Time-Bounded Temporal Logic Specifications in Dynamic Environments Authors: Medina Ayala, Ana Ivonne; Andersson, Sean; Belta, Calin
    The increasing need for real time robotic systems capable of performing tasks in changing and constrained environments demands the development of reliable and adaptable motion planning and control algorithms. This paper considers a mobile robot whose performance is measured by the completion of temporal logic tasks within a certain period of time. In addition to such time constraints, the planning algorithm must also deal with changes in the robot’s workspace during task execution. In our case, the robot is deployed in a partitioned environment subjected to structural changes in which doors shift from open to closed and vice-versa. The motion of the robot is modeled as a Continuous Time Markov Decision Process and the robot’s mission is expressed as a Continuous Stochastic Logic (CSL) temporal logic specification. An approximate solution to find a control strategy that satisfies such specifications is derived for a subset of probabilistic CSL formulae. Simulation and experimental results are provided to illustrate the method.
  • Non-Gaussian Belief Space Planning: Correctness and Complexity Authors: Platt, Robert; Tedrake, Russ; Kaelbling, Leslie; Lozano-Perez, Tomas
    We consider the partially observable control problem where it is potentially necessary to perform complex information-gathering operations in order to localize state. One approach to solving these problems is to create plans in {em belief-space}, the space of probability distributions over the underlying state of the system. The belief-space plan encodes a strategy for performing a task while gaining information as necessary. Unlike most approaches in the literature which rely upon representing belief state as a Gaussian distribution, we have recently proposed an approach to non-Gaussian belief space planning based on solving a non-linear optimization problem defined in terms of a set of state samples~cite{platt_isrr2011}. In this paper, we show that even though our approach makes optimistic assumptions about the content of future observations for planning purposes, all low-cost plans are guaranteed to gain information in a specific way under certain conditions. We show that eventually, the algorithm is guaranteed to localize the true state of the system and to reach a goal region with high probability. Although the computational complexity of the algorithm is dominated by the number of samples used to define the optimization problem, our convergence guarantee holds with as few as two samples. Moreover, we show empirically that it is unnecessary to use large numbers of samples in order to obtain good performance.
  • Proving the Correctness of Concurrent Robot Software Authors: Kazanzides, Peter; Kouskoulas, Yanni; Deguet, Anton; Shao, Zhong
    Component-based software has been proposed as a methodology for improving software reuse and has increasingly been adopted by robot software developers. At the same time, robot systems typically have real-time performance requirements and performance gains can often be obtained by multi-threading. It is challenging, however, to create correct multi-threaded software, especially when standard mutual exclusion primitives, such as mutexes and semaphores, are eschewed in favor of more efficient, lock-free mechanisms. It is even more difficult to find these errors, as they can remain dormant for years until triggered by just the &quot;right&quot; conditions. Our approach, therefore, is to apply Formal Methods to reason about the correctness of these mechanisms. As a first step, we adopted a recently-developed program logic called History for Local Rely/Guarantee (HLRG) and applied it to prove the correctness (after first finding and fixing an error) of one such mechanism in the open source <i>cisst</i> software package. This strategy is not specific to <i>cisst</i> and can be applied to other packages.