This paper presents an iterative approach for heterogeneous multi-agent route planning in environments with unknown resource distributions. We focus on a team of robots with diverse capabilities tasked with executing missions specified using Capability Temporal Logic (CaTL), a formal framework built on Signal Temporal Logic to handle spatial, temporal, capability, and resource constraints. The key challenge arises from the uncertainty in the initial distribution and quantity of resources in the environment. To address this, we introduce an iterative algorithm that dynamically balances exploration and task fulfillment. Robots are guided to explore the environment, identifying resource locations and quantities while progressively refining their understanding of the resource landscape. At the same time, they aim to maximally satisfy the mission objectives based on the current information, adapting their strategies as new data is uncovered. This approach provides a robust solution for planning in dynamic, resource-constrained environments, enabling efficient coordination of heterogeneous teams even under conditions of uncertainty. Our method's effectiveness and performance are demonstrated through simulated case studies.

We propose a two-level hierarchical architecture for controlling an autonomous vehicle (ego) in complex urban driving environments. This approach ensures both collision avoidance and adherence to traffic rules while maintaining real-time performance. At the top level of our framework, we use a simple dynamic model for ego and a simplified representation of the environment to formulate a Model Predictive Control (MPC) problem. The traffic rules are represented by Signal Temporal Logic (STL) formulas and incorporated as mixed integer-linear constraints within the MPC optimization. The top level MPC solution is then simulated at the bottom level, which employs detailed models of both ego dynamics and the environment. If a collision or traffic rule violation occurs, the bottom level provides feedback to the top level in the form of correction constraints, which are mixed integer-linear constraints affecting the state and control input of ego. This closed-loop feedback from the bottom level helps address discrepancies between the simplified models used in the MPC and the complex real-world models. We assess the effectiveness and runtime performance of our method by comparing it with existing approaches, through simulations of various urban driving scenarios in the CARLA simulator.

The paper considers the route planning problem for a vehicle with limited capacity operating in a road network. The vehicle is assigned a set of transportation requests that are more complex than traveling between two locations, may involve dependencies between their sub-tasks, and include deadlines and priorities. The requests arrive gradually over the deployment time-horizon, and thus replanning is needed for new requests. We address cases when not all requests can be serviced by their deadlines despite car sharing. We introduce multiple quality measures for plans that account for requests' delays with respect to deadlines and priorities. We formalize the problem as planning in a weighted transition system under syntactically co-safe LTL formulas. We develop an online planning and replanning algorithm based on the automata-based approach to least-violating plan synthesis and on translation to a Mixed Integer Linear Program (MILP). Furthermore, we show that the MILP reduces to graph search for a subclass of quality measures that satisfy a monotonicity property. We show the approach in simulations, including a case study on the mid-Manhattan road network over the span of 24 hours.

In this work, we address the problem of control synthesis for a homogeneous team of robots given a global temporal logic specification and formal user preferences for relaxation in case of infeasibility. The relaxation preferences are represented as a Weighted Finite-state Edit System and are used to compute a relaxed specification automaton that captures all allowable relaxations of the mission specification and their costs. For synthesis, we introduce a Mixed Integer Linear Programming (MILP) formulation that combines the motion of the team of robots with the relaxed specification automaton. Our approach combines automata-based and MILP-based methods and leverages the strengths of both approaches, while avoiding their shortcomings. Specifically, the relaxed specification automaton explicitly accounts for the progress towards satisfaction, and the MILP-based optimization approach avoids the state-space explosion associated with explicit product-automata construction, thereby efficiently solving the problem. The case studies highlight the efficiency of the proposed approach.

This paper introduces an iterative approach to multi-agent route planning under chance constraints. A heterogeneous team of agents with various capabilities is tasked with a Capability Temporal Logic (CaTL) mission, a fragment of Signal Temporal Logic. The agents’ motion is modeled as a finite weighted graph, where the weights represent travel durations. Given the probability distribution over the durations of each edge’s traversal, we want to find paths for all agents such that (a) the specification robustness is maximized, (b) travel time is minimized, and (c) the success probability is maximized. We tackle the problem using an iterative approach. In each stage, it selects edges’ traversal duration and success probabilities and then solves a multi-agent route planning problem. We use an efficient Mixed-Integer Linear Programming (MILP) encoding for the latter. Our method provides a framework for agents to make informed decisions in choosing the most suitable edge attributes (travel durations and success probabilities) that consider agents’ capabilities to perform tasks in the environment. The proposed iterative method leverages graph structure to generate a more efficient search space. The effectiveness of our method is demonstrated through simulated case studies where obtaining the optimal solution would otherwise be computationally expensive. Our approach efficiently explores the solution space, generating better solutions and improving the performance of multi-agent route planning with uncertain travel durations.

This work presents an optimization-based control synthesis approach for an extension of Signal Temporal Logic (STL) called weighted Signal Temporal Logic (wSTL). wSTL was proposed to accommodate user preferences for importance and priorities over concurrent and sequential tasks as well as satisfaction times denoted by weights over the logical and temporal operators, respectively. We propose a Mixed Integer Linear Programming (MILP) based approach for synthesis with wSTL specifications. These specifications have the same qualitative semantics as STL but differ in their quantitative semantics, which is recursively modulated with weights. Additionally, we extend the formal definition of wSTL to include the semantics for until and release temporal operators and present an efficient encoding for these operators in the MILP formulation. As opposed to the original implementation of wSTL, where the arithmetic-geometric mean robustness was used with gradient-based methods prone to local optima, our encoding allows the use of a weighted version of traditional robustness and efficient global MILP solvers. We demonstrate the operational performance of the proposed formulation using multiple case studies, showcasing the distinct functionalities over Boolean and temporal operators. Moreover, we elaborate on multiple case studies for synthesizing controllers for an agent navigating a non-convex environment under different constraints highlighting the difference in synthesized control plans for STL and wSTL. Finally, we compare the time and complexity performance of encodings for STL and wSTL.

This paper presents an agent-agnostic framework to control swarms of robots tasked with temporal and logical missions expressed as Metric Temporal Logic (MTL) formulas. We consider agents that can receive global commands from a high-level planner, but no inter-agent communication. Moreover, agents are grouped into sub-swarms whose number can vary over the mission time horizon due to splitting and merging. However, a strict upper bound on the maximum number of sub-swarms is imposed to ensure their safe operation in the environment. We propose a two-phase approach. In the first phase, we compute the trajectories of the sub-swarms, splitting, and merging actions using a Mixed Integer Linear Programming approach that ensures the satisfaction of the MTL specification with minimal swarm division over the mission time horizon. Moreover, it enforces the upper bound on the number of sub-swarms. In the second phase, splitting fractions for sub-swarms resulting from splitting actions are computed. A distributed randomized protocol with no interagent communication ensures agent assignments matching the splitting fractions. Finally, we show the operation and performance of the approach in simulations with multiple tasks that require swarm splitting or merging.

This work presents a step towards utilizing incrementally-improving symbolic perception knowledge of the robot's surroundings for provably correct reactive control synthesis applied to an autonomous driving problem. Combining abstract models of motion control and information gathering, we show that assume-guarantee specifications (a subclass of Linear Temporal Logic) can be used to define and resolve traffic rules for cautious planning. We propose a novel representation called symbolic refinement tree for perception that captures the incremental knowledge about the environment and embodies the relationships between various symbolic perception inputs. The incremental knowledge is leveraged for synthesizing verified reactive plans for the robot. The case studies demonstrate the efficacy of the proposed approach in synthesizing control inputs even in case of partially occluded environments.

Time-series data classification is central to the analysis and control of autonomous systems, such as robots and self-driving cars. Temporal logic-based learning algorithms have been proposed recently as classifiers of such data. However, current frameworks are either inaccurate for real-world applications, such as autonomous driving, or they generate long and complicated formulae that lack interpretability. To address these limitations, we introduce a novel learning method, called Boosted Concise Decision Trees (BCDTs), to generate binary classifiers that are represented as Signal Temporal Logic (STL) formulae. Our algorithm leverages an ensemble of Concise Decision Trees (CDTs) to improve the classification performance, where each CDT is a decision tree that is empowered by a set of techniques to generate simpler formulae and improve interpretability. The effectiveness and classification performance of our algorithm are evaluated on naval surveillance and urban-driving case studies.

Mobility-on-demand systems are transforming the way we think about the transportation of people and goods. Most research effort has been placed on scalability issues for systems with a large number of agents and simple pickup/drop-off demands. In this paper, we consider fair multi-vehicle route planning with streams of complex, temporal logic transportation demands. We consider an approximately envy-free fair allocation of demands to limited-capacity vehicles based on agents' accumulated utility over a finite time horizon, representing for example monetary reward or utilization level. We propose a scalable approach based on the construction of assignment graphs that relate agents to routes and demands, and pose the problem as an Integer Linear Program (ILP). Routes for assignments are computed using automata-based methods for each vehicle and demands sets of size at most the capacity of the vehicle while taking into account their pickup wait time and delay tolerances. In addition, we integrate utility-based weights in the assignment graph and ILP to ensure approximative fair allocation. We demonstrate the computational and operational performance of our methods in ride-sharing case studies over a large environment in mid-Manhattan and Linear Temporal Logic demands with stochastic arrival times. We show that our method significantly decreases the utility deviation between agents and the vacancy rate.

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.

Transporting objects using quadrotors with cables has been widely studied in the literature. However, most of those approaches assume that the cables are previously attached to the load by human intervention. In tasks where multiple objects need to be moved, the efficiency of the robotic system is constrained by the requirement of manual labor. Our approach uses a non-stretchable cable connected to two quadrotors, which we call the catenary robot, that fully automates the transportation task. Using the cable, we can roll and drag the cuboid object (box) on planar surfaces. Depending on the surface type, we choose the proper action, dragging for low friction, and rolling for high friction. Therefore, the transportation process does not require any human intervention as we use the cable to interact with the box without requiring fastening. We validate our control design in simulation and with actual robots, where we show them rolling and dragging boxes to track desired trajectories.

In this paper, we introduce an automata-based framework for planning with relaxed specifications. User relaxation preferences are represented as weighted finite state edit systems that capture permissible operations on the specification, substitution and deletion of tasks, with complex constraints on ordering and grouping. We propose a three-way product automaton construction method that allows us to compute minimal relaxation policies for the robots using shortest path algorithms. The three-way product automaton captures the robot’s motion, specification satisfaction, and available relaxations at the same time. Additionally, we consider a bi-objective problem that balances temporal relaxation of deadlines within specifications with changing and deleting tasks. Finally, we present the runtime performance and a case study that highlights different modalities of our framework.

We introduce a method to learn imitative 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, 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. We build upon previous work by no longer requiring additional supervised information which is hard to collect in practice. We achieve this by using a deep Bayesian nonparametric hierarchical model. We test our model on several domains and also show results for a real-world implementation on a mobile robotic arm platform.

In this paper, we examine the problem of navigating cluttered environments without explicit object detection and tracking. We introduce the dynamic risk density to map the congestion density and spatial flow of the environment to a cost function for the agent to determine risk when navigating that environment. We build upon our prior work, wherein the agent maps the density and motion of objects to an occupancy risk, then navigate the environment over a specified risk level set. Here, the agent does not need to identify objects to compute the occupancy risk, and instead computes this cost function using the occupancy density and velocity fields around them. Simulations show how this dynamic risk density encodes movement information for the ego agent and closely models the object-based congestion cost. We implement our dynamic risk density on an autonomous wheelchair and show how it can be used for navigating unstructured, crowded and cluttered environments.

In this paper we consider a fleet of self-driving cars operating in a road network governed by rules of the road, such as the Vienna Convention on Road Traffic, providing rides to customers to serve their demands with desired deadlines. We focus on the associated motion planning problem that trades-off the demands' delays and level of violation of the rules of the road to achieve social optimum among the vehicles. Due to operating in the same environment, the interaction between the cars must be taken into account, and can induce further delays. We propose an integrated route and motion planning approach that achieves scalability with respect to the number of cars by resolving potential collision situations locally within so-called bubble spaces enclosing the conflict. The algorithms leverage the road geometries, and perform joint planning only for lead vehicles in the conflict and use queue scheduling for the remaining cars. Furthermore, a framework for storing previously resolved conflict situations is proposed, which can be use for quick querying of joint motion plans. We show the mobility-on-demand setup and effectiveness of the proposed approach in simulated case studies involving up to 10 self-driving vehicles.

This work focuses on integrated routing and motion planning for an autonomous vehicle in a road network. We consider a problem in which customer demands need to be met within desired deadlines, and the rules of the road need to be satisfied. The vehicle might not, however, be able to satisfy these two goals at the same time. We propose a systematic way to compromise between delaying the satisfaction of the given demand and violating the road rules. We utilize scLTL formulas to specify desired behavior and develop a receding horizon approach including a periodically interacting routing algorithm and a RRT*-based motion planner. The proposed solution yields a provably minimum-violation trajectory. An illustrative case study is included.

Reinforcement learning (RL) depends critically on the choice of reward functions used to capture the desired behavior and constraints of a robot. Usually, these are handcrafted by a expert designer and represent heuristics for relatively simple tasks. Real world applications typically involve more complex tasks with rich temporal and logical structure. In this paper we take advantage of the expressive power of temporal logic (TL) to specify complex rules the robot should follow, and incorporate domain knowledge into learning. We propose Truncated Linear Temporal Logic (TLTL) as a specification language, We propose Truncated Linear Temporal Logic (TLTL) as a specification language, that is arguably well suited for the robotics applications, We show in simulated trials that learning is faster and policies obtained using the proposed approach outperform the ones learned using heuristic rewards in terms of the robustness degree, i.e., how well the tasks are satisfied. Furthermore, we demonstrate the proposed RL approach in a toast-placing task learned by a Baxter robot.

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.

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.

This paper introduces a framework for inference of timed temporal logic properties from data. The dataset is given as a finite set of pairs of finite-time system traces and labels, where the labels indicate whether the traces exhibit some desired behavior (e.g., a ship traveling along a safe route). We propose a decision-tree based approach for learning signal temporal logic classifiers. The method produces binary decision trees that represent the inferred formulae. Each node of the tree contains a test associated with the satisfaction of a simple formula, optimally tuned from a predefined finite set of primitives. Optimality is assessed using heuristic impurity measures, which capture how well the current primitive splits the data with respect to the traces' labels. We propose extensions of the usual impurity measures from machine learning literature to handle classification of system traces by leveraging upon the robustness degree concept. The proposed incremental construction procedure greatly improves the execution time and the accuracy compared to existing algorithms. We present two case studies that illustrate the usefulness and the computational advantages of the algorithms. The first is an anomaly detection problem in a maritime environment. The second is a fault detection problem in an automotive powertrain system.

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.

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. Our method 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. Building on our previous work [1], the focus of this paper is on the on-line part of the overall method.

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.

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.