This letter explores coordination of heterogeneous teams of agents from high-level specifications. We employ Capability Temporal Logic (CaTL) to express rich, temporal-spatial tasks that require cooperation between many agents with unique capabilities. CaTL specifies combinations of tasks , each with desired locations, duration, and set of capabilities, freeing the user from considering specific agent trajectories and their impact on multi-agent cooperation. CaTL also provides a quantitative robustness metric of satisfaction based on availability of required capabilities for each task. The novelty of this letter focuses on satisfaction of CaTL formulas under probabilistic conditions. Specifically, we consider uncertainties in robot motion (e.g., agents may fail to transition between regions with some probability) and local probabilistic workspace properties (e.g., if there are not enough agents of a required capability to complete a collaborative task). The proposed approach automatically formulates a mixed-integer linear program given agents, their dynamics and capabilities, an abstraction of the workspace, and a CaTL formula. In addition to satisfying the given CaTL formula, the optimization considers the following secondary goals (in decreasing order of priority): 1) minimize the risk of transition failure due to uncertainties; 2) maximize probabilities of regional collaborative satisfaction (if there is an excess of agents); 3) maximize the availability robustness of CaTL for potential agent attrition; 4) minimize the total agent travel time. We evaluate the performance of the proposed framework and demonstrate its scalability via numerical simulations.
We focus on decomposing large multi-agent path planning problems with global temporal logic goals (common to all agents) into smaller sub-problems that can be solved and executed independently. Crucially, the sub-problems' solutions must jointly satisfy the common global mission specification. The agents' missions are given as Capability Temporal Logic (CaTL) formulas, a fragment of Signal Temporal Logic (STL) that can express properties over tasks involving multiple agent capabilities (i.e., different combinations of sensors, effectors, and dynamics) under strict timing constraints. The approach we take is to jointly decompose both the temporal logic specification and the team of agents, using a satisfiability modulo theories (SMT) approach and heuristics for handling temporal operators. The output of the SMT is then distributed to subteams and leads to a significant speed up in planning time compared to planning for the entire team and specification. We include computational results to evaluate the efficiency of our solution, as well as the trade-offs introduced by the conservative nature of the SMT encoding and heuristics.
Symbolic reasoning is a key component for enabling practical use of data-driven planners in autonomous driving. In that context, deterministic finite state automata (DFA) are often used to formalize the underlying high-level decision-making process. Manual design of an effective DFA can be tedious. In combination with deep learning pipelines, DFA can serve as an effective representation to learn and process complex behavioral patterns. The goal of this work is to leverage that potential. We propose the automaton generative network (AGN), a differentiable representation of DFAs. The resulting neural network module can be used standalone or as an embedded component within a larger architecture. In evaluations on deep learning based autonomous vehicle planning tasks, we demonstrate that incorporating AGN improves the explainability, sample efficiency, and generalizability of the model.
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.
We extend Signal Temporal Logic (STL) to enable the specification of importance and priorities. The extension, called Weighted STL (wSTL), has the same qualitative (Boolean) semantics as STL, but additionally defines weights associated with Boolean and temporal operators that modulate its quantitative semantics (robustness). We show that the robustness of wSTL can be defined as weighted generalizations of all known compatible robustness functionals (i.e., robustness scores that are recursively defined over formulae) that can take into account the weights in wSTL formulae. We utilize this weighted robustness to distinguish signals with respect to a desired wSTL formula that has subformulae with different importance or priorities and time preferences, and demonstrate its usefulness in problems with conflicting tasks where satisfaction of all tasks cannot be achieved. We also employ wSTL robustness in an optimization framework to synthesize controllers that maximize satisfaction of a specification with user specified preferences.
We introduce a method to learn policies from expert demonstrations that are interpretable and manipulable. We achieve interpretability by modeling the interactions between high-level actions as an automaton with connections to formal logic. We achieve manipulability by integrating this automaton into planning via Logical Value Iteration, so that changes to the automaton have predictable effects on the learned behavior. These qualities allow a human user to first understand what the model has learned, and then either correct the learned behavior or zero-shot generalize to new, similar tasks. Our inference method requires only low-level trajectories and a description of the environment in order to learn high-level rules. We achieve this by using a deep Bayesian nonparametric hierarchical model. We test our model on several domains of interest and also show results for a real-world implementation on a mobile robotic arm platform for lunchbox-packing and cabinet-opening tasks.
In this work, we propose a novel approach for integrating rules into traffic agent trajectory prediction. Consideration of rules is important for understanding how people behave-yet, it cannot be assumed that rules are always followed. To address this challenge, we evaluate different approaches of integrating rules as inductive biases into deep learning-based prediction models. We propose a framework based on generative adversarial networks that uses tools from formal methods, namely signal temporal logic and syntax trees. This allows us to leverage information on rule obedience as features in neural networks and improves prediction accuracy without biasing towards lawful behavior. We evaluate our method on a real-world driving dataset and show improvement in performance over off-the-shelf predictors.
We develop a sampling-based motion planning algorithm that combines long-term temporal logic goals with short-term reactive requirements. The mission specification has two parts: (1) a global specification given as a linear temporal logic (LTL) formula over a set of static service requests that occur at the regions of a known environment, and (2) a local specification that requires servicing a set of dynamic requests that can be sensed locally during the execution. The proposed computational framework consists of two main ingredients: (a) an off-line sampling-based algorithm for the construction of a global transition system that contains a path satisfying the LTL formula; and (b) an on-line sampling-based algorithm to generate paths that service the local requests, while making sure that the satisfaction of the global specification is not affected. The off-line algorithm has four main features. First, it is incremental, in the sense that the procedure for finding a satisfying path at each iteration scales only with the number of new samples generated at that iteration. Second, the underlying graph is sparse, which implies low complexity for the overall method. Third, it is probabilistically complete. Fourth, under some mild assumptions, it has the best possible complexity bound. The on-line algorithm leverages ideas from LTL monitoring and potential functions to ensure progress towards the satisfaction of the global specification while servicing locally sensed requests. Examples and experimental trials illustrating the usefulness and the performance of the framework are included.
We present a solution for operating a vehicle without global positioning infrastructure while satisfying constraints on its temporal behavior, and on the uncertainty of its position estimate. The proposed solution is an end-to-end framework for mapping an unknown environment using aerial vehicles, synthesizing a control policy for a ground vehicle in that environment, and using a quadrotor to localize the ground vehicle within the map while it executes its control policy. This vision-based localization is noisy, necessitating planning in the belief space of the ground robot. The ground robot's mission is given using a language called Gaussian Distribution Temporal Logic (GDTL), an extension of Boolean logic that incorporates temporal evolution and noise mitigation directly into the task specifications. We use a sampling-based algorithm to generate a transition system in the belief space and use local feedback controllers to break the curse of history associated with belief space planning. To localize the vehicle, we build a high-resolution map of the environment by flying a team of aerial vehicles in formation with sensor information provided by their onboard cameras. The control policy for the ground robot is synthesized under temporal and uncertainty constraints given the semantically labeled map. Then the ground robot can execute the control policy given pose estimates from a dedicated aerial robot that tracks and localizes the ground robot. The proposed method is validated using two quadrotors to build a map, followed by a two-wheeled ground robot and a quadrotor with a camera for ten successful experimental trials.
In this paper, we study the translational and rotational (SE(N)) invariance properties of locally interacting multi-agent systems. We focus on a class of networked dynamical systems, in which the agents have local pairwise interactions, and the overall effect of the interaction on each agent is the sum of the interactions with other agents. We show that such systems are SE(N)-invariant if and only if they have a special, quasi-linear form. The SE(N)-invariance property, sometimes referred to as left invariance, is central to a large class of kinematic and robotic systems. When satisfied, it ensures independence to global reference frames. In an alternate interpretation, it allows for integration of dynamics and computation of control laws in the agents' own reference frames. Such a property is essential in a large spectrum of applications, e.g., navigation in GPS-denied environments. Because of the simplicity of the quasi-linear form, this result can impact ongoing research on design of local interaction laws. It also gives a quick test to check if a given networked system is SE(N)-invariant.
This paper introduces time window temporal logic (TWTL), a rich expressivity language for describing various time bounded specifications. In particular, the syntax and semantics of TWTL enable the compact representation of serial tasks, which are prevalent in various applications including robotics, sensor systems, and manufacturing systems. This paper also discusses the relaxation of TWTL formulae with respect to the deadlines of the tasks. Efficient automata-based frameworks are presented to solve synthesis, verification and learning problems. The key ingredient to the presented solution is an algorithm to translate a TWTL formula to an annotated finite state automaton that encodes all possible temporal relaxations of the given formula. Some case studies are presented to illustrate the expressivity of the logic and the proposed algorithms.
Cancer is a complex and heterogeneous genetic disease. Different mutations and dysregulated molecular mechanisms alter the pathways that lead to cell proliferation. In this paper, we explore a method which classifies genes into oncogenes (ONGs) and tumor suppressors. We optimize this method to identify specific (ONGs) and tumor suppressors for breast cancer, lung adenocarcinoma (LUAD), lung squamous cell carcinoma (LUSC) and colon adenocarcinoma (COAD), using data from the cancer genome atlas (TCGA). A set of genes were previously classified as ONGs and tumor suppressors across multiple cancer types (Science 2013). Each gene was assigned an ONG score and a tumor suppressor score based on the frequency of its driver mutations across all variants from the catalogue of somatic mutations in cancer (COSMIC). We evaluate and optimize this approach within different cancer types from TCGA. We are able to determine known driver genes for each of the four cancer types. After establishing the baseline parameters for each cancer type, we identify new driver genes for each cancer type, and the molecular pathways that are highly affected by them. Our methodology is general and can be applied to different cancer subtypes to identify specific driver genes and improve personalized therapy.
In this work, we present a novel method for automating persistent surveillance missions involving multiple vehicles. Automata-based techniques are used to generate collision-free motion plans for a team of vehicles to satisfy a temporal logic specification. Vector fields are created for use with a differential flatness-based controller, allowing vehicle flight and deployment to be fully automated according to the motion plans. The use of charging platforms with the vehicles allows for truly persistent missions. Experiments were performed with two quadrotors for two different missions over 50 runs each to validate the theoretical results.
This paper provides the proof that Enzymatic Numerical P systems with deterministic, but parallel, execution model are universal, even when the production functions used are polynomials of degree 1. This extends previous known results and provides the optimal case in terms of polynomial degree.
We study the computing power of a class of numerical P systems introduced in the framework of autonomous robot control, namely enzymatic numerical P systems. Three ways of using the evolution programs are investigated: sequential, all-parallel and one-parallel (with the same variable used in all programs or in only one, respectively); moreover, both deterministic and non-deterministic systems are considered. The Turing universality of some of the obtained classes of numerical P systems is proved (for polynomials with the smallest possible degree, one, also introducing a new proof technique in this area, namely starting the universality proof from the characterization of computable sets of numbers by means of register machines). The power of many other classes remains to be investigated.
The main contribution of this paper is the introduction of the new concept of membrane controller based on the structure and functioning of a deterministic numerical P system. The procedure for developing a membrane controller and for using it to control a mobile robot is explained and several test cases are given in which membrane controllers are used to control both simulated and real mobile robots and to generate various desired behaviours (obstacle avoidance, wall following, and follow the leader). The experiments reported in this paper validate the concept and prove that the performance of a membrane controller is comparable to or better than that of other controllers (such as fuzzy logic controllers).
This paper presents PyElph, a software tool which automatically extracts data from gel images, computes the molecular weights of the analyzed molecules or fragments, compares DNA patterns which result from experiments with molecular genetic markers and, also, generates phylogenetic trees computed by five clustering methods, using the information extracted from the analyzed gel image. The software can be successfully used for population genetics, phylogenetics, taxonomic studies and other applications which require gel image analysis. Researchers and students working in molecular biology and genetics would benefit greatly from the proposed software because it is free, open source, easy to use, has a friendly Graphical User Interface and does not depend on specific image acquisition devices like other commercial programs with similar functionalities do.
PyElph software tool is entirely implemented in Python which is a very popular programming language among the bioinformatics community. It provides a very friendly Graphical User Interface which was designed in six steps that gradually lead to the results. The user is guided through the following steps: image loading and preparation, lane detection, band detection, molecular weights computation based on a molecular weight marker, band matching and finally, the computation and visualization of phylogenetic trees. A strong point of the software is the visualization component for the processed data. The Graphical User Interface provides operations for image manipulation and highlights lanes, bands and band matching in the analyzed gel image. All the data and images generated in each step can be saved. The software has been tested on several DNA patterns obtained from experiments with different genetic markers. Examples of genetic markers which can be analyzed using PyElph are RFLP (Restriction Fragment Length Polymorphism), AFLP (Amplified Fragment Length Polymorphism), RAPD (Random Amplification of Polymorphic DNA) and STR (Short Tandem Repeat). The similarity between the DNA sequences is computed and used to generate phylogenetic trees which are very useful for population genetics studies and taxonomic classification.
PyElph decreases the effort and time spent processing data from gel images by providing an automatic step-by-step gel image analysis system with a friendly Graphical User Interface. The proposed free software tool is suitable for researchers and students which do not have access to expensive commercial software and image acquisition devices.
This paper presents a particle swarm optimization (PSO)-inspired multi-robot search application based on an innovative software system for collaborative robotic applications. The system has a multi-layer architecture which provides low- and high-level interfaces to the robots, resource (robots) management, security policies and concurrent robot access. The main result is the successful testing of the PSO-inspired algorithm on real-world experiments, using Khepera III and e-puck robots. Simulated results obtained in other studies are therefore validated by the real-world experiments. Differences between simulation and real-world experiments are presented and discussed critically.