Many existing approaches for coordinating heterogeneous teams of robots either consider small numbers of agents, are application-specific, or do not adequately address common real-world requirements, e.g., strict deadlines or intertask dependencies. We introduce scalable and robust algorithms for task-based coordination from high-level specifications (ScRATCHeS) to coordinate such teams. We define a specification language, capability temporal logic, to describe rich, temporal properties involving tasks requiring the participation of multiple agents with multiple capabilities, e.g., sensors or end effectors. Arbitrary missions and team dynamics are jointly encoded as constraints in a mixed integer linear program, and solved efficiently using commercial off-the-shelf solvers. ScRATCHeS optionally allows optimization for maximal robustness to agent attrition at the penalty of increased computation time. We include an online replanning algorithm that adjusts the plan after an agent has dropped out. The flexible specification language, fast solution time, and optional robustness of ScRATCHeS provide a first step toward a multipurpose on-the-fly planning tool for tasking large teams of agents with multiple capabilities enacting missions with multiple tasks. We present randomized computational experiments to characterize scalability and hardware demonstrations to illustrate the applicability of our methods.

Networked dynamical systems are increasingly used as models for a variety of processes ranging from robotic teams to collections of genetically engineered living cells. As the complexity of these systems increases, so does the range of emergent properties that they exhibit. In this work, we define a new logic called Spatial-Temporal Logic (SpaTeL) that is a unification of signal temporal logic (STL) and tree spatial superposition logic (TSSL). SpaTeL is capable of describing high-level spatial patterns that change over time, e.g., "Power consumption in the northwest quadrant of the city drops below 100 megawatts if the power consumption in the southwest quadrant remains above 200 megawatts for two hours." We present a statistical model checking procedure that evaluates the probability with which a networked system satisfies a SpaTeL formula. We also develop a synthesis procedure that determines system parameters maximizing the average degree of satisfaction, a continuous measure that quantifies how strongly a system execution satisfies a given formula. We demonstrate our algorithms on two systems: a biochemical reaction-diffusion system and a demand-side management system for a smart neighborhood.

We consider the problem of controlling a system with unknown, stochastic dynamics to achieve a complex, time-sensitive task. An example of this problem is controlling a noisy aerial vehicle with partially known dynamics to visit a pre-specified set of regions in any order while avoiding hazardous areas. In particular, we are interested in tasks which can be described by signal temporal logic (STL) specifications. STL is a rich logic that can be used to describe tasks involving bounds on physical parameters, continuous time bounds, and logical relationships over time and states. STL is equipped with a continuous measure called the robustness degree that measures how strongly a given sample path exhibits an STL property [4, 3]. This measure enables the use of continuous optimization problems to solve learning [7, 6] or formal synthesis problems [9] involving STL.

This paper presents an inference algorithm that can discover temporal logic properties of a system from data. Our algorithm operates on finite time system trajectories that are labeled according to whether or not they demonstrate some desirable system properties (e.g. "the car successfully stops before hitting an obstruction"). A temporal logic formula that can discriminate between the desirable behaviors and the undesirable ones is constructed. The formulae also indicate possible causes for each set of behaviors (e.g. "If the speed of the car is greater than 15 m/s within 0.5s of brake application, the obstruction will be struck") which can be used to tune designs or to perform on-line monitoring to ensure the desired behavior. We introduce reactive parameter signal temporal logic (rPSTL), a fragment of parameter signal temporal logic (PSTL) that is expressive enough to capture causal, spatial, and temporal relationships in data. We define a partial order over the set of rPSTL formulae that is based on language inclusion. This order enables a directed search over this set, i.e. given a candidate rPSTL formula that does not adequately match the observed data, we can automatically construct a formula that will fit the data at least as well. Two case studies, one involving a cattle herding scenario and one involving a stochastic hybrid gene circuit model, are presented to illustrate our approach.

This paper considers the problem of finding the most informative path for a sensing robot under temporal logic constraints, a richer set of constraints than have previously been considered in information gathering. An algorithm for informative path planning is presented that leverages tools from information theory and formal control synthesis, and is proven to give a path that satisfies the given temporal logic constraints. The algorithm uses a receding horizon approach in order to provide a reactive, on-line solution while mitigating computational complexity. Statistics compiled from multiple simulation studies indicate that this algorithm performs better than a baseline exhaustive search approach.