Hot-swapping robot task goals in reactive formal synthesis
Scott Livingston

Citation
Scott Livingston. "Hot-swapping robot task goals in reactive formal synthesis". Tutorial, 18, February, 2015.

Abstract
We consider the problem of synthesizing robot controllers to realize a task that unpredictably changes with time. Tasks are formally expressed in the GR(1) fragment of temporal logic, in which some of the variables are set by an adversary. The task changes by the addition or removal of goals, which occurs online (i.e., at run-time). We present an algorithm for mending control strategies to realize tasks after the addition of goals, while avoiding global re-synthesis of the strategy. Experiments are presented for a planar surveillance task in which new regions of interest are incrementally added. Run-times are empirically shown to be favorable compared to re-synthesizing from scratch. We also present an algorithm for mending control strategies for the removal of goals. While in this setting the original strategy is still feasible, our algorithm provides a more satisfying solution by "tightening loose ends." Both algorithms are shown to yield so-called reach annotations, and thus the control strategies are easily amenable to other algorithms concerning incremental synthesis, e.g., as in previous work by the authors for navigation in uncertain environments.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Scott Livingston. <a
  href="http://www.terraswarm.org/pubs/484.html"
  ><i>Hot-swapping robot task goals in reactive
  formal synthesis</i></a>, Tutorial,  18,
  February, 2015.

• Plain text

  Scott Livingston. "Hot-swapping robot task goals in
  reactive formal synthesis". Tutorial,  18, February,
  2015.

• BibTeX

  @tutorial{Livingston15_HotswappingRobotTaskGoalsInReactiveFormalSynthesis,
      author = {Scott Livingston},
      title = {Hot-swapping robot task goals in reactive formal
                synthesis},
      day = {18},
      month = {February},
      year = {2015},
      abstract = {We consider the problem of synthesizing robot
                controllers to realize a task that unpredictably
                changes with time. Tasks are formally expressed in
                the GR(1) fragment of temporal logic, in which
                some of the variables are set by an adversary. The
                task changes by the addition or removal of goals,
                which occurs online (i.e., at run-time). We
                present an algorithm for mending control
                strategies to realize tasks after the addition of
                goals, while avoiding global re-synthesis of the
                strategy. Experiments are presented for a planar
                surveillance task in which new regions of interest
                are incrementally added. Run-times are empirically
                shown to be favorable compared to re-synthesizing
                from scratch. We also present an algorithm for
                mending control strategies for the removal of
                goals. While in this setting the original strategy
                is still feasible, our algorithm provides a more
                satisfying solution by "tightening loose ends."
                Both algorithms are shown to yield so-called reach
                annotations, and thus the control strategies are
                easily amenable to other algorithms concerning
                incremental synthesis, e.g., as in previous work
                by the authors for navigation in uncertain
                environments. },
      URL = {http://terraswarm.org/pubs/484.html}
  }
  

Posted by Barb Hoversten on 3 Feb 2015.
Groups: services