In this article, we propose a method to replan coverage paths for a robot operating in an environment with initially unknown static obstacles. Existing coverage approaches reduce coverage time by covering along the minimum number of coverage lines (straight-line paths). However, recomputing such paths online can be computationally expensive resulting in robot stoppages that increase coverage time. A naive alternative isgreedy detourreplanning, i.e., replanning with minimum deviation from the initial path, which is efficient to compute but may result in unnecessary detours. In this work, we propose an anytime coverage replanning approach namedOARP-Replanthat performs near-optimal replans to an interrupted coverage path within a given time budget. We do this by solving linear relaxations of integer linear programs to identify sections of the interrupted path that can be optimally replanned within the time budget. We validate OARP-Replan in simulation and perform comparisons against a greedy detour replanner and other state-of-the-art coverage planners. We also demonstrate OARP-Replan in experiments using an industrial-level autonomous robot.

In this paper, we propose a new method for solving multirobot motion planning problems with complex constraints. We focus on an important class of problems that require an allocation of spatially distributed tasks to robots, along with efficient paths for each robot to visits their task locations. We introduce a framework for solving these problems that naturally couples allocation with path planning. The allocation problem is encoded as a Boolean Satisfiability problem (SAT) and the path planning problem is encoded as a traveling salesman problem (TSP). In addition, the framework can handle complex constraints such as battery life limitations, robot carrying capacities, and robot-task incompatibilities. We propose an algorithm that leverages recent advances in Satisfiability Modulo Theory (SMT) to combine state-of-the-art SAT and TSP solvers. We characterize the correctness of our algorithm and evaluate it in simulation on a series of patrolling, periodic routing, and multirobot sample collection problems. The results show our algorithm significantly outperforms state-of-the-art mathematical programming solvers.

We emphasize the need to articulate precise, declarative properties in the context of securing Digital ICs. We do this by discussing two pieces of our work on securing Digital ICs. In one, we discuss a seemingly compelling approach to protecting Intellectual Property -- IC camouflaging. We demonstrate that an adversary can carry out a decamouflaging attack, in practice, much more efficiently than previously thought. Underlying our attack is strong foundations: an identification of the computational-complexity of the problems an attacker faces, and how they can be addressed using off-the-shelf constraint solvers. We identify the lack of a precise characterization of "security" in this context as an issue. In the other piece of work, we present an example of the articulation of such a security property for 3D IC technology, in the context of securing a supply-chain. The property is articulated declaratively, with explicit assumptions that underlie the threat model.

The Sat-Tsp language was recently proposed [1] for expressing and solving high-level robotic path planning problems. In this paper we show how different constraints that commonly appear in path planning problems, such as set constraints, counting constraints, and ordering constraints can all be expressed in the Sat-Tsp language. We also show how the language can be used to express multi-robot path planning problems. We evaluate our existing solver approaches on test problems that include a variety of complex constraints and we demonstrate the language through a ROS implementation. We also provide a new approach that reduces the Sat-Tsp language to the generalized traveling salesman problem language. We show that this new approach outperforms our existing approaches on problems that contain one-on-a-set constraints.

In this paper we introduce a new language in which discrete path planning problems for mobile robots can be specified and solved. Given an environment represented as a graph and a Boolean variable for each vertex to represent its inclusion/exclusion on the path, we consider the problem of finding the shortest path (or tour) in the graph subject to a Boolean satisfiability (Sat) formula defined over the vertex variables. We call this problem Sat-Tsp. We show the expressiveness of this language for specifying complex motion planning objectives in a discrete environment. We then present three solution techniques for this problem, including a novel reduction to the well known travelling salesman problem (Tsp). We present extensive simulation results which compare the performance of the three solvers on standard benchmarks from Tsp, Sat, and Generalized Tsp (Gtsp) literature.