Publications

Recent advances in autonomous driving have raised the problem of safety to the forefront and incentivized research into establishing safety guarantees. In this paper, we propose a safety verification framework as a safety standard for driving controllers with full or shared autonomy based on compositional and contract-based principles. Our framework enables us to synthesize safety guarantees over entire road networks by first building a library of locally verified models, and then composing local models together to verify the entire network. Composition is achieved using assume-guarantee contracts that are synthesized concurrently during verification. Thus, we can reuse local models within and across networks, add additional models to cover local road geometries without re-verifying the entire library, and perform all computations in a parallel and distributed way, which enables computational tractability. Furthermore, we employ controller contracts such that any controller satisfying them can be certified safe. We demonstrate the practical effectiveness of our framework by certifying controllers over parts of the Manhattan road network.

Sampling-based methods have advanced the state of the art in robotic motion planning and control across complex, high-dimensional domains. With few exceptions, such approaches only admit simple constraints and objectives, such as collision-avoidance and reaching a goal state. In this work we leverage the best of two worlds: the scalability of sampling-based motion planning and the precise formal guarantees of temporal logic. We present an incremental sampling-based algorithm that synthesizes a motion control policy satisfying a bounded Signal Temporal Logic formula over properties of a given environment. Our key insight is that we can bias the selection of samples using a quantitative measure of how well the best path in the current tree of samples satisfies the specification. This allows us both to converge to a path that satisfies the specification, and to improve upon an existing path, i.e. to satisfy the specification with maximum robustness. We illustrate the performance of our method in several case studies.

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.

In this paper, we focus on robot motion planning from timed temporal logic specifications. We propose a sampling-based algorithm and an associated language-guided biasing scheme. We leverage the notion of temporal relaxation of time-window temporal logic formulae (TWTL) to reformulate the temporal logic synthesis problem into an optimization problem. Our algorithm exhibits an exploration-exploitation structure, but retains probabilistic completeness. Moreover, if the problem does not have a solution due to time constraints, the algorithm returns a candidate path that satisfies a minimally relaxed version of the specification. The path may inform operators about timing problems with the specification or the system. We provide simulations to highlight the performance of the proposed algorithm.

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.

Designing systems in synthetic biology typically involves composing pieces of DNA to achieve a desired behavior. In order to accomplish this goal, methods for specifying the function realized by genetic modules are necessary. Additionally, it is often difficult to efficiently explore the design space of genetic circuits while taking into account various biological constraints. In this work, we propose a methodology for automatically characterizing genetic constructs using signal temporal logic (STL) specifications. These specifications allow for composition using an extension to STL that adds the notion of input, output, and internal signals. Furthermore, we have devised a procedure that employs tree-based searching and pruning techniques to explore the design space of a genetic circuit given a library of modules and a desired specification.

This paper addresses a persistent vehicle routing problem, where a team of vehicles is required to achieve a task repetitively. The task is given as a Time-Window Temporal Logic (TWTL) formula defined over the environment. The fuel consumption of each vehicle is explicitly captured as a stochastic model. As vehicles leave the mission area for refueling, the number of vehicles may not always be sufficient to achieve the task. We propose a decoupled and efficient control policy to achieve the task or its minimal relaxation. We quantify the temporal relaxation of a TWTL formula and present an algorithm to minimize it. The proposed policy has two layers: 1) each vehicle decides when to refuel based on its remaining fuel, 2) a central authority plans the joint trajectories of the available vehicles to achieve a minimally relaxed task. We demonstrate the proposed approach via simulations and experiments involving a team of quadrotors that conduct persistent surveillance.

In this work, we present a novel method for automating persistent surveillance missions involving multiple vehicles. Automata-based techniques were used to generate collision-free motion plans for a team of vehicles to satisfy a temporal logic specification. Vector fields were 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 over 50 runs to validate the theoretical results.

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 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.

In this work, we present a novel method for automating persistent surveillance missions involving multiple vehicles. Automata-based techniques were used to generate collision-free motion plans for a team of vehicles to satisfy a temporal logic specification. Vector fields were 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 over 50 runs to validate the theoretical results.

In this paper, we propose a sampling-based motion planning algorithm that finds an infinite path satisfying a Linear Temporal Logic (LTL) formula over a set of properties satisfied by some regions in a given environment. The algorithm has three 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 guarantees the low complexity of the overall method. Third, it is probabilistically complete. Examples illustrating the usefulness and the performance of the method are included.

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 developed 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 three 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 guarantees the low complexity of the overall method. Third, it is probabilistically complete. We also provide a conditional result showing that the incremental checking procedure has the best possible complexity bound. The on-line algorithm leverages ideas of potential functions, which ensure progress towards satisfaction of the global specification, and on monitors for LTL. Examples illustrating the usefulness and the performance of the framework are included.
 

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).

Background

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.

Results

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.

Conclusions

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.

A cognitive collaborative multi-agent control architecture that addresses real-world control problems for swarms of mobile robots is proposed. The swarm's emergent behaviour is obtained by using a distributed Particle Swarm Optimization inspired algorithm. A swarm-user interface is also presented and offers a way for a human operator to interact with and guide the robotic swarm without limiting its emergent intelligence. The architecture is designed as a multi-agent system developed using JADE Framework. Three types of agents were defined: local behaviour agent, social behaviour agent and graphical user interface (GUI) agent. Each robot is associated with a pair of a local and a social behaviour agents which implement the reactive component and the interaction between the robots. The swarm forms a hierarchical structure composed of subswarms and neighbourhoods based on tasks and goals defined by the user or the swarm itself. The GUI agent is used as a link between the human expert and the swarm. The architecture was tested on a swarm of e-puck robots.