SearcharxivSearch

arXiv subjects

Indranil Saha

Publications and source records attributed to Indranil Saha.

18 recordsLinked to original sources

Robust Black-box Testing of Deep Neural Networks using Co-Domain Coverage

Rigorous testing of machine learning models is necessary for trustworthy deployments. We present a novel black-box approach for generating test-suites for robust testing of deep neural networks (DNNs). Most existing methods create test inputs based on maximizing some "coverage" criterion/metric such as a fraction of neurons activated by the test inputs. Such approaches, however, can only analyze each neuron's behavior or each layer's output in isolation and are unable to capture their collective effect on the DNN's output, resulting in test suites that often do not capture the various failure modes of the DNN adequately. These approaches also require white-box access, i.e., access to the DNN's internals (node activations). We present a novel black-box coverage criterion called Co-Domain Coverage (CDC), which is defined as a function of the model's output and thus takes into account its end-to-end behavior. Subsequently, we develop a new fuzz testing procedure named CoDoFuzz, which uses CDC to guide the fuzzing process to generate a test suite for a DNN. We extensively compare the test suite generated by CoDoFuzz with those generated using several state-of-the-art coverage-based fuzz testing methods for the DNNs trained on six publicly available datasets. Experimental results establish the efficiency and efficacy of CoDoFuzz in generating the largest number of misclassified inputs and the inputs for which the model lacks confidence in its decision.

cs.LG

Counter-example guided Imitation Learning of Feedback Controllers from Temporal Logic Specifications

We present a novel method for imitation learning for control requirements expressed using Signal Temporal Logic (STL). More concretely we focus on the problem of training a neural network to imitate a complex controller. The learning process is guided by efficient data aggregation based on counter-examples and a coverage measure. Moreover, we introduce a method to evaluate the performance of the learned controller via parameterization and parameter estimation of the STL requirements. We demonstrate our approach with a flying robot case study.

cs.RO

Online Concurrent Multi-Robot Coverage Path Planning

Recently, centralized receding horizon online multi-robot coverage path planning algorithms have shown remarkable scalability in thoroughly exploring large, complex, unknown workspaces with many robots. In a horizon, the path planning and the path execution interleave, meaning when the path planning occurs for robots with no paths, the robots with outstanding paths do not execute, and subsequently, when the robots with new or outstanding paths execute to reach respective goals, path planning does not occur for those robots yet to get new paths, leading to wastage of both the robotic and the computation resources. As a remedy, we propose a centralized algorithm that is not horizon-based. It plans paths at any time for a subset of robots with no paths, i.e., who have reached their previously assigned goals, while the rest execute their outstanding paths, thereby enabling concurrent planning and execution. We formally prove that the proposed algorithm ensures complete coverage of an unknown workspace and analyze its time complexity. To demonstrate scalability, we evaluate our algorithm to cover eight large $2$D grid benchmark workspaces with up to 512 aerial and ground robots, respectively. A comparison with a state-of-the-art horizon-based algorithm shows its superiority in completing the coverage with up to 1.6x speedup. For validation, we perform ROS + Gazebo simulations in six 2D grid benchmark workspaces with 10 quadcopters and TurtleBots, respectively. We also successfully conducted one outdoor experiment with three quadcopters and one indoor with two TurtleBots.

cs.RO

Optimal Integrated Task and Path Planning and Its Application to Multi-Robot Pickup and Delivery

We propose a generic multi-robot planning mechanism that combines an optimal task planner and an optimal path planner to provide a scalable solution for complex multi-robot planning problems. The Integrated planner, through the interaction of the task planner and the path planner, produces optimal collision-free trajectories for the robots. We illustrate our general algorithm on an object pick-and-drop planning problem in a warehouse scenario where a group of robots is entrusted with moving objects from one location to another in the workspace. We solve the task planning problem by reducing it into an SMT-solving problem and employing the highly advanced SMT solver Z3 to solve it. To generate collision-free movement of the robots, we extend the state-of-the-art algorithm Conflict Based Search with Precedence Constraints with several domain-specific constraints. We evaluate our integrated task and path planner extensively on various instances of the object pick-and-drop planning problem and compare its performance with a state-of-the-art multi-robot classical planner. Experimental results demonstrate that our planning mechanism can deal with complex planning problems and outperforms a state-of-the-art classical planner both in terms of computation time and the quality of the generated plan.

cs.RO

A Conflict-Aware Optimal Goal Assignment Algorithm for Multi-Robot Systems

The fundamental goal assignment problem for a multi-robot application aims to assign a unique goal to each robot while ensuring collision-free paths, minimizing the total movement cost. A plausible algorithmic solution to this NP-hard problem involves an iterative process that integrates a task planner to compute the goal assignment while ignoring the collision possibilities among the robots and a multi-agent path-finding algorithm to find the collision-free trajectories for a given assignment. This procedure involves a method for computing the next best assignment given the current best assignment. A naive way of computing the next best assignment, as done in the state-of-the-art solutions, becomes a roadblock to achieving scalability in solving the overall problem. To obviate this bottleneck, we propose an efficient conflict-guided method to compute the next best assignment. Additionally, we introduce two more optimizations to the algorithm -- first for avoiding the unconstrained path computations between robot-goal pairs wherever possible, and the second to prevent duplicate constrained path computations for multiple robot-goal pairs. We extensively evaluate our algorithm for up to a hundred robots on several benchmark workspaces. The results demonstrate that the proposed algorithm achieves nearly an order of magnitude speedup over the state-of-the-art algorithm, showcasing its efficacy in real-world scenarios.

cs.MA

Frugal Actor-Critic: Sample Efficient Off-Policy Deep Reinforcement Learning Using Unique Experiences

Efficient utilization of the replay buffer plays a significant role in the off-policy actor-critic reinforcement learning (RL) algorithms used for model-free control policy synthesis for complex dynamical systems. We propose a method for achieving sample efficiency, which focuses on selecting unique samples and adding them to the replay buffer during the exploration with the goal of reducing the buffer size and maintaining the independent and identically distributed (IID) nature of the samples. Our method is based on selecting an important subset of the set of state variables from the experiences encountered during the initial phase of random exploration, partitioning the state space into a set of abstract states based on the selected important state variables, and finally selecting the experiences with unique state-reward combination by using a kernel density estimator. We formally prove that the off-policy actor-critic algorithm incorporating the proposed method for unique experience accumulation converges faster than the vanilla off-policy actor-critic algorithm. Furthermore, we evaluate our method by comparing it with two state-of-the-art actor-critic RL algorithms on several continuous control benchmarks available in the Gym environment. Experimental results demonstrate that our method achieves a significant reduction in the size of the replay buffer for all the benchmarks while achieving either faster convergent or better reward accumulation compared to the baseline algorithms.

cs.LG

A reactive neural network framework for water-loaded acidic zeolites

Under operating conditions, the dynamics of water and ions confined within protonic aluminosilicate zeolite micropores are responsible for many of their properties, including hydrothermal stability, acidity and catalytic activity. However, due to high computational cost, operando studies of acidic zeolites are currently rare and limited to specific cases and simplified models. In this work, we have developed a general reactive neural network potential (NNP) attempting to cover the entire class of acidic zeolites, including the full range of experimentally relevant water concentrations and Si/Al ratios. This NNP combines dramatic sampling acceleration, retaining the reference metaGGA DFT level, with the capacity for discovery of new chemistry, such as collective defect formation mechanisms at the zeolite surface. Furthermore, we exemplify how the NNP can be used as a basis for further extensions/improvements which include data-efficient adoption of higher-level (hybrid) references via $\Delta$-learning and the acceleration of rare event sampling via automatic construction of collective variables. These developments represent a significant step towards accurate simulations of realistic catalysts under operando conditions.

cond-mat.mtrl-sci

Online On-Demand Multi-Robot Coverage Path Planning

We present an online centralized path planning algorithm to cover a large, complex, unknown workspace with multiple homogeneous mobile robots. Our algorithm is horizon-based, synchronous, and on-demand. The recently proposed horizon-based synchronous algorithms compute all the robots' paths in each horizon, significantly increasing the computation burden in large workspaces with many robots. As a remedy, we propose an algorithm that computes the paths for a subset of robots that have traversed previously computed paths entirely (thus on-demand) and reuses the remaining paths for the other robots. We formally prove that the algorithm guarantees complete coverage of the unknown workspace. Experimental results on several standard benchmark workspaces show that our algorithm scales to hundreds of robots in large complex workspaces and consistently beats a state-of-the-art online centralized multi-robot coverage path planning algorithm in terms of the time needed to achieve complete coverage. For its validation, we perform ROS+Gazebo simulations in five 2D grid benchmark workspaces with 10 Quadcopters and 10 TurtleBots, respectively. Also, to demonstrate its practical feasibility, we conduct one indoor experiment with two real TurtleBot2 robots and one outdoor experiment with three real Quadcopters.

cs.RO

STL-Based Synthesis of Feedback Controllers Using Reinforcement Learning

Deep Reinforcement Learning (DRL) has the potential to be used for synthesizing feedback controllers (agents) for various complex systems with unknown dynamics. These systems are expected to satisfy diverse safety and liveness properties best captured using temporal logic. In RL, the reward function plays a crucial role in specifying the desired behaviour of these agents. However, the problem of designing the reward function for an RL agent to satisfy complex temporal logic specifications has received limited attention in the literature. To address this, we provide a systematic way of generating rewards in real-time by using the quantitative semantics of Signal Temporal Logic (STL), a widely used temporal logic to specify the behaviour of cyber-physical systems. We propose a new quantitative semantics for STL having several desirable properties, making it suitable for reward generation. We evaluate our STL-based reinforcement learning mechanism on several complex continuous control benchmarks and compare our STL semantics with those available in the literature in terms of their efficacy in synthesizing the controller agent. Experimental results establish our new semantics to be the most suitable for synthesizing feedback controllers for complex continuous dynamical systems through reinforcement learning.

cs.AI

MT* : Multi-Robot Path Planning for Temporal Logic Specifications

We address the path planning problem for a team of robots satisfying a complex high-level mission specification given in the form of an Linear Temporal Logic (LTL) formula. The state-of-the-art approach to this problem employs the automata-theoretic model checking technique to solve this problem. This approach involves computation of a product graph of the Buchi automaton generated from the LTL specification and a joint transition system which captures the collective motion of the robots and then computation of the shortest path using Dijkstra's shortest path algorithm. We propose MT*, an algorithm that reduces the computation burden for generating such plans for multi-robot systems significantly. Our approach generates a reduced version of the product graph without computing the complete joint transition system, which is computationally expensive. It then divides the complete mission specification among the participating robots and generates the trajectories for the individual robots independently. Our approach demonstrates substantial speedup in terms of computation time over the state-of-the-art approach, and unlike the state of the art approach, scales well with both the number of robots and the size of the workspace

cs.RO

DT*: Temporal Logic Path Planning in a Dynamic Environment

Path planning for a robot is one of the major problems in the area of robotics. When a robot is given a task in the form of a Linear Temporal Logic (LTL) specification such that the task needs to be carried out repetitively, we want the robot to follow the shortest cyclic path so that the number of times the robot completes the mission within a given duration gets maximized. In this paper, we address the LTL path planning problem in a dynamic environment where the newly arrived dynamic obstacles may invalidate some of the available paths at any arbitrary point in time. We present DT*, an SMT-based receding horizon planning strategy that solves an optimization problem repetitively based on the current status of the workspace to lead the robot to follow the best available path in the current situation. We implement our algorithm using the Z3 SMT solver and evaluate it extensively on an LTL specification capturing a pick-and-drop application in a warehouse environment. We compare our SMT-based algorithm with two carefully crafted greedy algorithms. Our experimental results show that the proposed algorithm can deal with the dynamism in the workspace in LTL path planning effectively.

cs.RO

Mobile Recharger Path Planning and Recharge Scheduling in a Multi-Robot Environment

In many multi-robot applications, mobile worker robots are often engaged in performing some tasks repetitively by following pre-computed trajectories. As these robots are battery-powered, they need to get recharged at regular intervals. We envision that in the future, a few mobile recharger robots will be employed to supply charge to the energy-deficient worker robots recurrently, to keep the overall efficiency of the system optimized.In this setup, we need to find the time instants and locations for the meeting of the worker robots and recharger robots optimally. We present a Satisfiability Modulo Theory (SMT)-based approach that captures the activities of the robots in the form of constraints in a sufficiently long finite-length time window (hypercycle) whose repetitions provide their perpetual behavior. Our SMT encoding ensures that for a chosen length of the hypercycle, the total waiting time of the worker robots due to charge constraints is minimized under certain condition, and close to optimal when the condition does not hold. Moreover, the recharger robots follow the most energy-efficient trajectories. We show the efficacy of our approach by comparing it with another variant of the SMT-based method which is not scalable but provides an optimal solution globally, and with a greedy algorithm.

cs.RO

Synthesis of Feedback Controller for Nonlinear Control Systems with Optimal Region of Attraction

We propose a framework for synthesizing a feedback control policy that maximizes the region of attraction (ROA) of a closed-loop nonlinear dynamical system. Our synthesis technique relies on stochastic optimization, which involves computation of an objective function capturing the ROA for a feedback control law. We employ a machine learning technique based on deep neural network to estimate the ROA for a given feedback controller. Overall, our technique is capable of synthesizing a controller co-optimizing traditional control objectives like LQR cost together with ROA. We demonstrate the efficacy of our technique through exhaustive experiments carried out on various nonlinear systems.

eess.SY

T* : A Heuristic Search Based Algorithm for Motion Planning with Temporal Goals

Motion planning is the core problem to solve for developing any application involving an autonomous mobile robot. The fundamental motion planning problem involves generating a trajectory for a robot for point-to-point navigation while avoiding obstacles. Heuristic-based search algorithms like A* have been shown to be extremely efficient in solving such planning problems. Recently, there has been an increased interest in specifying complex motion plans using temporal logic. In the state-of-the-art algorithm, the temporal logic motion planning problem is reduced to a graph search problem and Dijkstra's shortest path algorithm is used to compute the optimal trajectory satisfying the specification. The A* algorithm when used with a proper heuristic for the distance from the destination can generate an optimal path in a graph efficiently. The primary challenge for using A* algorithm in temporal logic path planning is that there is no notion of a single destination state for the robot. In this thesis, we present a novel motion planning algorithm T* that uses the A* search procedure in temporal logic path planning \emph{opportunistically} to generate an optimal trajectory satisfying a temporal logic query. Our experimental results demonstrate that T* achieves an order of magnitude improvement over the state-of-the-art algorithm to solve many temporal logic motion planning problems.

cs.RO

SPARCAS: A Decentralized, Truthful Multi-Agent Collision-free Path Finding Mechanism

We propose a decentralized collision-avoidance mechanism for a group of independently controlled robots moving on a shared workspace. Existing algorithms achieve multi-robot collision avoidance either (a) in a centralized setting, or (b) in a decentralized setting with collaborative robots. We focus on the setting with competitive robots in a decentralized environment, where robots may strategically reveal their information to get prioritized. We propose the mechanism SPARCAS in this setting that, using principles of mechanism design, ensures truthful revelation of the robots' private information and provides locally efficient movement of the robots. It is free from collisions and deadlocks, and handles a dynamic arrival of robots. In practice, this mechanism scales well for a large number of robots where the optimal collision-avoiding path-finding algorithm (M*) does not scale. Yet, SPARCAS does not compromise the path optimality too much. Our mechanism prioritizes the robots in the order of their `true' higher needs, but for a higher payment. It uses monetary transfers which is small enough compared to the value received by the robots.

cs.RO

A Comparative Study of a Class of Mean Field Theories of the Glass Transition

In a recently developed microscopic mean field theory, we have shown that the dynamics of a system, when described only in terms of its pair structure, can predict the correct dynamical transition temperature. Further, the theory predicted the difference in dynamics of two systems (the Lennard-Jones and the WCA) despite them having quite similar structures. This is in contrast to the Schweizer-Saltzman (SS) formalism which predicted the dynamics of these two systems to be similar. The two theories although similar in spirit have certain differences. Here we present a comparative study of these two formalisms to find the origin of the difference in their predictive power. We show that not only the dynamics in the potential energy surface, as described by our earlier study, but also that in the free energy surface, like in the SS theory, can predict the correct dynamical transition temperature. Even an approximate one component version of our theory, similar to the system used in the SS theory, can predict the transition temperature reasonably well. According to our analysis, the absence of the Vineyard approximation in the SS formalism led it to predict similar dynamics for the two systems. Interestingly, we show here that despite the above mentioned shortcomings the SS theory can actually predict the correct transition temperatures. Thus microscopic mean field theories of this class which express dynamics in terms of the pair structure of the liquid while being unable to predict the actual dynamics of the system are successful in predicting the correct dynamical transition temperature.

cond-mat.soft

Synthesis of Minimal Error Control Software

Software implementations of controllers for physical systems are at the core of many embedded systems. The design of controllers uses the theory of dynamical systems to construct a mathematical control law that ensures that the controlled system has certain properties, such as asymptotic convergence to an equilibrium point, while optimizing some performance criteria. However, owing to quantization errors arising from the use of fixed-point arithmetic, the implementation of this control law can only guarantee practical stability: under the actions of the implementation, the trajectories of the controlled system converge to a bounded set around the equilibrium point, and the size of the bounded set is proportional to the error in the implementation. The problem of verifying whether a controller implementation achieves practical stability for a given bounded set has been studied before. In this paper, we change the emphasis from verification to automatic synthesis. Using synthesis, the need for formal verification can be considerably reduced thereby reducing the design time as well as design cost of embedded control software. We give a methodology and a tool to synthesize embedded control software that is Pareto optimal w.r.t. both performance criteria and practical stability regions. Our technique is a combination of static analysis to estimate quantization errors for specific controller implementations and stochastic local search over the space of possible controllers using particle swarm optimization. The effectiveness of our technique is illustrated using examples of various standard control systems: in most examples, we achieve controllers with close LQR-LQG performance but with implementation errors, hence regions of practical stability, several times as small.

eess.SY

A Simplification of a Real-Time Verification Problem

We revisit the problem of real-time verification with dense dynamics using timeout and calendar based models and simplify this to a finite state verification problem. To overcome the complexity of verification of real-time systems with dense dynamics, Dutertre and Sorea, proposed timeout and calender based transition systems to model the behavior of real-time systems and verified safety properties using k-induction in association with bounded model checking. In this work, we introduce a specification formalism for these models in terms of Timeout Transition Diagrams and capture their behavior in terms of semantics of Timed Transition Systems. Further, we discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of (a large fragment of) these timeout and calender based transition systems into that on clockless finite state models through a two-step process comprising of digitization and canonical finitary reduction. This technique enables us to verify safety invariants for real-time systems using finite state model-checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction based proof methodology. Moreover, we can verify liveness properties for real-time systems, which is not possible by using induction with infinite state model checkers. We present examples of Fischer's Protocol, Train-Gate Controller, and TTA start-up algorithm to illustrate how such an approach can be efficiently used for verifying safety, liveness, and timeliness properties specified in LTL using finite state model checkers like SAL-smc and Spin. We also demonstrate how advanced modeling concepts like inter-process scheduling, priorities, interrupts, urgent and committed location can be specified as extensions of the proposed specification formalism.

cs.LO