Search

We present an efficient algorithm for multi-robot motion planning from linear temporal logic (LTL) specifications. We assume that the dynamics of each robot can be described by a discrete-time, linear system together with constraints on the control inputs and state variables. Given an LTL formula specifying the multi-robot mission, our goal is to construct a set of collision-free trajectories for all robots, and the associated control strategies, to satisfy We show that the motion planning problem can be formulated as the feasibility problem for a formula p over Boolean and convex constraints, respectively capturing the LTL specification and the robot dynamics. We then adopt a satisfiability modulo convex (SMC) programming approach that exploits a monotonicity property of p to decompose the problem into smaller subproblems. Simulation results show that our algorithm is more than one order of magnitude faster than state-of-the-art sampling-based techniques for high-dimensional state spaces while supporting complex missions.

Distributed mobile robotics (DMR) involves teams of networked robots navigating in a physical space to achieve tasks in a coordinated fashion. A major challenge in DMR is to program the ensemble of robots with formal guarantees and high assurance of correct operation. To this end, we introduce Drona, a framework for building reliable DMR applications. This paper makes three central contributions: (1) We present a novel and provably correct decentralized asynchronous motion planner that can perform on-the-fly collision-free planning for dynamically generated tasks. Moreover, the motion planner is the first to take into account the fact that distributed robots may have clocks that are only synchronized up to a tolerance, i.e., they are almost synchronous; (2) We formalize the DMR system as a mixed-synchronous system, and present a sound abstraction-based verification approach for DMR systems, and (3) Drona provides a state-machine based language for safe event-driven programming of a DMR system and the code generated by the compiler can be executed on platforms such as the robot operating system (ROS). To demonstrate the efficacy of Drona, we build and verify a priority mail delivery system. Using our abstraction-based verification approach we were able to find, within a few minutes, bugs which could not be found by performing random simulation for several hours. Our verified decentralized motion-planner scales efficiently for large number of robots (upto 128 robots) and workspace sizes (upto a 256×256 grid).

We present a scalable robot motion planning algorithm for reach-avoid problems. We assume a discrete-time, linear model of the robot dynamics and a workspace described by a set of obstacles and a target region, where both the obstacles and the region are polyhedra. Our goal is to construct a trajectory, and the associated control strategy, that steers the robot from its initial point to the target while avoiding obstacles. Differently from previous approaches, based on the discretization of the continuous state space or uniform discretization of the workspace, our approach, inspired by the lazy satisfiability modulo theory paradigm, decomposes the planning problem into smaller subproblems, which can be efficiently solved using specialized solvers. At each iteration, we use a coarse, obstacle-based discretization of the workspace to obtain candidate high-level, discrete plans that solve a set of Boolean constraints, while completely abstracting the low-level continuous dynamics. The feasibility of the proposed plans is then checked via a convex program, under constraints on both the system dynamics and the control inputs, and new candidate plans are generated until a feasible one is found. To achieve scalability, we show how to generate succinct explanations for the infeasibility of a discrete plan by exploiting a relaxation of the convex program that allows detecting the earliest possible occurrence of an infeasible transition between workspace regions. Simulation results show that our algorithm favorably compares with state-of-the-art techniques and scales well for complex systems, including robot dynamics with up to 50 continuous states.

We consider the collision-free motion planning problem for a group of robots using a library of motion primitives. To cope with the complexity of the problem, we introduce an incremental algorithm based on an SMT solver, where we divide the robots into small groups based on a priority assignment algorithm. The priority assignment algorithm assigns priorities to the robots in such a way that the robots do not block the cost-optimal trajectories of the other robots. While the priority assignment algorithm attempts to assign distinct priorities to the robots, the algorithm ends up with assigning the same priority to some robots due to the dependencies among themselves. The algorithm includes the robots with the same priority in the same group. Our incremental algorithm then considers the robot groups one by one based on their priority and synthesizes the trajectories for the group of robots together. While synthesizing the trajectories for the robots in one group, the algorithm considers the higher priority robots as dynamic obstacles, and introduces a minimal delay in executing the cost-optimal trajectories to avoid collision with the higher priority robots. We apply our method to synthesize trajectories for a group of quadrotors in our lab space. Experimental results show that we can synthesize trajectories for tens of robots with complex dynamics in a reasonable time.

We present a compositional motion planning framework for multi-robot systems based on an encoding to satisfiability modulo theories (SMT). In our framework, the desired behavior of a group of robots is specified using a set of safe linear temporal logic (LTL) properties. Our method relies on a library of motion primitives, each of which corresponds to a controller that ensures a particular trajectory in a given configuration. Using the closed-loop behavior of the robots under the action of different controllers, we formulate the motion planning problem as an SMT solving problem and use an off-the-shelf SMT solver to generate trajectories for the robots. Our approach can also be extended to synthesize optimal cost trajectories where optimality is defined with respect to the available motion primitives. Experimental results show that our framework can efficiently solve complex motion planning problems in the context of multi-robot systems.

Background: During the surge of COVID-19 pandemic, the mechanism of reporting and documentation of deaths was inadequate. It is crucial to establish the mechanism for measuring the actual events of COVID-19 and associated mortalities as well during this pandemic situation. This is the first instance of application of different rapid methods for death estimation during the pandemic situation. If found to be valid, these methods may be useful for other countries with limited resources and less developed death registration system. Objective: To find out the feasibility, acceptability of different rapid method for estimating the cause of deaths among the general population & healthcare workers and also to estimate the number of deaths among allopathic doctors. Methodology: The study was conducted from September 2022 to October 2023. Target population being adult deceased person between 1st April 2020 to 30th November 2022 among general population, health care worker and allopathic doctor. For the general population, the study was conducted in one urban municipal area and two sub-centres of Habra Block I under North 24 Parganas district with WHO Verbal Autopsy (VA) tool for adult. Complete enumeration with snowballing, compartmental and capture-recapture method was adopted for general population, health care worker and allopathic doctor respectively. Results: Overall, 300 VA could be performed (121 urban & 179 rural) among general population. There were challenges related to both feasibility & acceptability in terms of data access, permission and cooperation. Research team employed a combination of persistence, local collaboration, and strategic decision-making to successfully collect data. Acceptability was more in rural area. Total number of deceased doctors was estimated to be 246 from two different lists. Conclusion: Rapid methods may be employed as a part of response systems during pandemic or any future disasters if adequate governmental support and assistance is obtained along with aid from the local people.

Context. The grey mullet, Mugil cephalus, is an edible fish of high economic importance. Breeding biology with reference to hormonal/growth factor regulation of oocyte maturation needs to be known for its commercial production. Objective. The present study was conducted to examine the potency of maturation inducing hormones, chorionic gonadotropin (hCG), bovine-insulin, and insulin like growth factor1 (h-IGF-1) I on ovarian steroidogenesis and oocyte maturation. Design. The role of hormones and growth factors on steroidogenesis and oocyte maturation was investigated using specific inhibitors, Wortmannin for phosphatidylinositol-3 (PI3) kinase, trilostane for 3β-hydroxysteroid dehydrogenase, 1-octanol and 1-heptanol for gap junctions, actinomycin D for transcription and cycloheximide for translation of signal molecules. Methods. Actions of hormonal and growth factors were examined for steroidogenesis, by radioimmunoassay and oocyte maturation by germinal vesicle breakdown (GVBD). Specific inhibitors were used to determine the cell signaling pathways, PI3 kinase. Results. All the inhibitors attenuated the hCGinduced oocyte maturation (GVBD%), steroidogenesis including transcription, translation, gap junctions and PI3 kinase signaling. These inhibitors failed to inhibit h-IGF-I and b-insulin-induced oocyte maturation, steroidogenesis, translation and PI3 kinase signaling. Conclusion. hCG induces oocyte maturation via steroid dependent pathway involving gap junctions, transcription, translation and PI3 kinase signaling, unlike h-IGF-I and b-insulin in the mullet. [ABSTRACT FROM AUTHOR]