This paper considers the combination of temporal logic (TL) specifications and local objective functions to create online, multiagent, motion plans. These plans are guaranteed to satisfy a persistent mission TL specification and locally optimize an objective function (e.g. in this paper, a cost based on information entropy). The presented approach decouples the two tasks by assigning sub-teams of agents to fulfill the TL specification, while unassigned agents optimize the objective function locally. This paper also presents a novel decoupling of the classic product automaton based approach while maintaining satisfaction guarantees. We also qualitatively show that optimality loss in the local greedy minimization due to the TL constraints can be approximated based on specification complexity. This approach is evaluated with a set of simulations and an experiment of 6 robots with real sensors.
more »
« less
Planning Coordinated Event Observation for Structured Narratives
This paper addresses the problem of using autonomous robots to record events that obey narrative structure. The work is motivated by a vision of robot teams that can, for example, produce individualized highlight videos for each runner in a large-scale road race such as a marathon. We introduce a method for specifying the desired structure as a function that describes how well the captured events can be used to produce an output that meets the specification. This function is specified in a compact, legible form similar to a weighted finite automaton. Then we describe a planner that uses simple predictions of future events to coordinate the robots' efforts to capture the most important events, as determined by the specification. We describe an implementation of this approach, and demonstrate its effectiveness in a simulated race scenario both in simulation and in a hardware testbed.
more »
« less
- NSF-PAR ID:
- 10129750
- Date Published:
- Journal Name:
- Planning Coordinated Event Observation for Structured Narratives
- Page Range / eLocation ID:
- 7632 to 7638
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separation-logic proofs of imperative programs. We have implemented these as an enhancement of the verified software toolchain (VST). VST is an impredicative concurrent separation logic for the C language, implemented in the Coq proof assistant, and proved sound in Coq. For machine-checked functional-correctness verification of software at scale, VST embeds its expressive program logic in dependently typed higher-order logic (CiC). Specifications and proofs in the program logic can leverage the expressiveness of CiCβso users can overcome the abstraction gaps that stand in the way of top-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VST has supported the specification of a program as a flat collection of function specifications (in higher-order separation logic)βone proves that each function correctly implements its specification, assuming the specifications of the functions it calls. But what if a function has more than one specification? In this work, we exploit type-theoretic concepts to structure specification interfaces for C code. This brings modularity principles of modern software engineering to concrete program verification. Previous work used representation predicates to enable data abstraction in separation logic. We go further, introducing function-specification subsumption and intersection specifications to organize the multiple specifications that a function is typically associated with. As in type theory, if π is a of π, that is π<:π, then π₯:π implies π₯:π, meaning that any function satisfying specification π can be used wherever a function satisfying π is demanded. Subsumption incorporates separation-logic framing and parameter adaptation, as well as step-indexing and specifications constructed via mixed-variance functors (needed for Cβs function pointers).more » « less
-
more » « less
Robots typically interact with their environments via feedback loops consisting of electronic sensors, microcontrollers, and actuators, which can be bulky and complex. Researchers have sought new strategies for achieving autonomous sensing and control in next-generation soft robots. We describe here an electronics-free approach for autonomous control of soft robots, whose compositional and structural features embody the sensing, control, and actuation feedback loop of their soft bodies. Specifically, we design multiple modular control units that are regulated by responsive materials such as liquid crystal elastomers. These modules enable the robot to sense and respond to different external stimuli (light, heat, and solvents), causing autonomous changes to the robotβs trajectory. By combining multiple types of control modules, complex responses can be achieved, such as logical evaluations that require multiple events to occur in the environment before an action is performed. This framework for embodied control offers a new strategy toward autonomous soft robots that operate in uncertain or dynamic environments.
-
We consider the problem of deploying robots to observe the evolution of a stochastic process in order to output a sequence of observations that fit some given specification. This problem often arises in contexts such as event reporting, situation depiction, and automated narrative generation. The paper extends our prior work by formulating and examining the multi-robot case: a team of robots move about, each recording what they observe, and, if they manage to capture some event, communicating that fact with the group. In the end, all events from all the robots are collated to provide a cumulative output. A plan is used to decide what each robot will attempt to capture next, based on the state of the world and the events that have been captured (collectively) so far. This paper focuses on the question of how to compute effective multi-robot plans. A monolithic treatment, involving the optimal selection of joint choices, i.e., choosing the next elements to attempt to capture by all robots, is formulated where costs are minimized in an expected sense. Since such plans are prohibitive to compute, variants based on an approximation scheme based on solving a sequence of individual planning problems are then introduced. This scheme sacrifices some solution quality but requires far less computational expense; we show this permits one to scale to greater numbers of robots.more » « less
-
Interactive Cartographic Storytelling with Complex Spatio-Temporal Structures and Social ConnectionsIn this paper, we describe the design of an interactive cartographic storytelling platform for the 1906 Atlanta Race Massacre, a horrific incident that had a profound impact on the civil and human rights movement in the United States. This four-day event happened at various locations in downtown Atlanta and involved many people. Although multiple books and articles have been written about the 1906 Atlanta Race Massacre, they described the past events using conventional storytelling methods. We want to tell this story from a cartographic perspective because the locations are essential to this story. We also want to connect the past with the present because most people walking on the same streets today do not know the history and significance of the locations. Furthermore, most people are unaware that some major institutions are intricately connected to the people involved in the 1906 events. Telling the story this way requires us to handle a complex spatio-temporal structure and an extensive social network, which is unusual in traditional cartographic storytelling. In this paper, we discuss our design decisions and rationals. We believe our discussion will benefit other interactive story designers who deal with similar complex stories.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/ICRA.2019.8794450
