Publications

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.

Temporal logics (TLs) have been widely used to formalize interpretable tasks for cyber-physical systems. Time Window Temporal Logic (TWTL) has been recently proposed as a specification language for dynamical systems. In particular, it can easily express robotic tasks, and it allows for efficient, automata-based verification and synthesis of control policies for such systems. In this paper, we define two quantitative semantics for this logic, and two corresponding monitoring algorithms, which allow for real-time quantification of satisfaction of formulas by trajectories of discrete-time systems. We demonstrate the new semantics and their runtime monitors on numerical examples.

Real-time and human-interpretable decision-making in autonomous systems is a significant but challenging task, which usually requires predictions of possible future events from limited data. While machine learning techniques have achieved promising results in this field, they lack interpretability and the ability to make online predictions for sequential behaviors. In this paper, we introduce a time-incremental learning framework to predict the labels of time-series signals that are received incrementally over time, referred to as prefix signals. These signals are being observed as they are generated, and their time lengths are shorter than their corresponding time horizons. We present a novel decision tree-based approach to learn a finite number of Signal Temporal Logic (STL) specifications from a given dataset and construct a predictor based on them. Each STL specification serves as a binary classifier of the time-series data and captures a specific part of the dataset's temporal properties over time. The predictor is built by assigning time-variant weights to the STL formulas, which represent their classification impacts. The weights are learned using neural networks to minimize the misclassification rate of classifying prefix signals with different time lengths. The predictor is then used to predict the labels of prefix signals by computing the weighted sum of their robustnesses with respect to the STL formulas. The effectiveness and classification performance of our algorithm is evaluated on urban-driving and naval-surveillance case studies.

We develop a novel framework to assess the risk of misperception in a traffic sign classification task in the presence of exogenous noise. We consider the problem in an autonomous driving setting, where visual input quality gradually improves due to improved resolution, and less noise since the distance to traffic signs decreases. Using the estimated perception statistics obtained using the standard classification algorithms, we aim to quantify the risk of misperception to mitigate the effects of imperfect visual observation. By exploring perception outputs, their expected high-level actions, and potential costs, we show the closed-form representation of the conditional value-at-risk (CVaR) of misperception. Several case studies support the effectiveness of our proposed methodology.

This paper explores continuous-time control synthesis for target-driven navigation to satisfy complex high-level tasks expressed in linear temporal logic (LTL). We propose a model-free framework using deep reinforcement learning (DRL) where the underlying dynamical system is unknown (an opaque box). Unlike prior work, we consider scenarios where the given LTL specification might be infeasible and therefore cannot be accomplished globally. Instead of modifying the given LTL formula, we provide a general DRL-based approach to satisfy it with minimal violation. To do this, we transform a previously multi-objective DRL problem, which requires simultaneous automata satisfaction and minimum violation cost, into a single objective. By guiding the DRL agent with a sampling-based path planning algorithm for the potentially infeasible LTL task, the proposed approach mitigates the myopic tendencies of DRL, which are often an issue when learning general LTL tasks that can have long or infinite horizons. This is achieved by decomposing an infeasible LTL formula into several reach-avoid sub-tasks with shorter horizons, which can be learned in a modular DRL architecture. Furthermore, we overcome the challenge of the exploration process for DRL in cluttered environments by using path planners to design rewards that are dense in the configuration space. The benefits of the presented approach are demonstrated through testing on various complex nonlinear systems and compared with state-of-the-art baselines. The video demonstration can be found here: https://youtu.be/DqesqBsja9k.

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

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.

This paper introduces a partial satisfaction (PS) notion for Signal Temporal Logic (STL), finding solutions for specifications that might contain unfeasible or conflicting subformulae. We formulate the planning problem for teams of agents with robust PS of STL missions as a bi-level optimization problem. The goal is to maximize the number of subformulae satisfied with preference to larger ones that have lower depth in the syntax tree of the overall specification. The second objective is to maximize the smallest STL robustness of the feasible subformulae. First, we propose three Mixed Integer Linear Programming (MILP) methods to solve the inner level of the optimization problem, two exact and a relaxation. Then, the MILP solutions are used to find approximate solutions to the outer level optimization using a linear program. Finally, we show the performance of our methods in two multi-robot case studies: motion planning in continuous spaces, and routing for heterogeneous teams over finite graph abstractions.

Risk awareness is an important factor to consider when deploying policies on robots in the real-world. Defining the right set of risk metrics can be difficult. In this work, we use a logic monitor that keeps track of the environmental agents’ behaviors and provides a risk metric that the controlled agent can incorporate during planning. We introduce LogicRiskNet, a learning structure that can be constructed from temporal logic formulas describing rules governing a safe agent’s behaviors. The network’s parameters can be learned from demonstration data. By using temporal logic, the network provides an interpretable architecture that can explain what risk metrics are important to the human. We integrate LogicRiskNet in an inverse optimal control (IOC) framework and show that we can learn to generate trajectory plans that accurately mimic the expert’s risk handling behaviors solely from demonstration data. We evaluate our method on a real-world driving dataset.

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 work, we propose a method for integration of temporal logic formulas into a neural network. Our main contribution is a new logic optimization layer that uses differentiable optimization on the formulas’ robustness function. This allows incorporating traffic rules into deep learning based trajectory prediction approaches. In the forward pass, an initial prediction from a base predictor is used to initialize and guide the robustness optimization process. Backpropagation through the logic layer allows for simultaneously adjusting the parameters of the rules and the initial prediction network. The integration of a logic layer
affords both improved predictions, as well as quantification rule satisfaction and violation during predictor execution. As such, it can serve as a parametric safetyenvelope for black box behavior models. We demonstrate how integrating traffic rules improves the predictor performance using real traffic data from the NuScenes dataset.

We consider the problem of scheduling and planning the motion of a fleet of robots involved in semiconductor manufacturing. The robots are tasked with transportation demands of goods that must be fulfilled according to given time constraints and synchronization rules. The demands and synchronization rules are specified using Time Window Temporal Logic (TWTL). Inspiring by model checking techniques, we develop a solution able to guarantee to satisfy both demands and synchronization rules. The proposed approach is tested through simulation on a semiconductor production site of the European project "Power Semiconductor and Electronics Manufacturing 4.0 - (SemI40)".

Existing approaches for coordinating teams of heterogeneous agents either consider small numbers of agents, are application-specific solutions, or do not adequately address requirements, e.g., deadlines or inter-task dependencies,common to real-world applications. We develop a framework called Scalable and Robust Algorithms for Task-based Coordination from High-level Specifications(ScRATCHS) to coordinate such teams. We define a specification language, called Capability Temporal Logic (CaTL), to describe rich, temporal properties involving tasks requiring the participation of multiple agents with multiple capabilities,e.g., sensors or end effectors. An example specification is "Ensure at least 10 airborne cameras and 3 airborne lidars are surveying Site A for at least 15 minutes simultaneously during every hour-long period. Make sure that 5 cameras are always observing Site B. Send 10 lidars to Site B within 3 hours of deployment and remain there until 4 ground vehicles with infrared sensors arrive 2 hours later." Arbitrary missions and team dynamics are jointly encoded as constraints in a mixed integer linear program (MILP), which can be solved efficiently using commercial off-the-shelf solvers. ScRATCHS also enables optimization of the resulting plan to be maximally robust to agent attrition at the penalty of increased computation time. The flexible specification language, fast solution time, and optional robustness of ScRATCHS provide a first step towards a multi-purpose on-the-fly planning tool for a supervisor tasking large teams with multiple capabilities enacting missions with multiple tasks. We validate our approach using randomized computational experiments and via a hardware demonstration.

This paper introduces the \textit{Logic-based Value Iteration Network} (LVIN) framework, which combines imitation learning and logical automata to enable agents to learn complex behaviours from demonstrations. We address two problems with learning from expert knowledge: (1) how to generalize learned policies for a task to larger classes of tasks, and (2) how to account for erroneous demonstrations. Our LVIN model solves finite gridworld environments by instantiating a recurrent, convolutional neural network as a value iteration procedure over a learned Markov Decision Process (MDP) that factors into two MDPs: a small finite state automaton (FSA) corresponding to logical rules, and a larger MDP corresponding to motions in the environment. The parameters of LVIN (value function, reward map, FSA transitions, large MDP transitions) are approximately learned from expert trajectories.

Signal Temporal Logic (STL) is a formal language for describing a broad range of real-valued, temporal properties in cyber-physical systems. While there has been extensive research on verification and control synthesis from STL requirements, there is no formal framework for comparing two STL formulae. In this paper, we show that under mild assumptions, STL formulae admit a metric space. We propose two metrics over this space based on i) the Pompeiu-Hausdorff distance and ii) the symmetric difference measure, and present algorithms to compute them. Alongside illustrative examples, we present applications of these metrics for two fundamental problems: a) design quality measures: to compare all the temporal behaviors of a designed system, such as a synthetic genetic circuit, with the "desired" specification, and b) loss functions: to quantify errors in Temporal Logic Inference (TLI) as a first step to establish formal performance guarantees of TLI algorithms.

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this first edition, we present five benchmarks with different levels of complexities and stochastic flavours. We make use of six different tools and frameworks (in alphabetical order): Barrier Certificates, FAUST2, FIRM-GDTL, Modest, SDCPN modelling & MC simulation and SReachTools; and attempt to solve instances of the five different benchmark problems. Through these benchmarks, we capture a snapshot on the current state-of the art tools and frameworks within the stochastic modelling domain. We also present the challenges encountered within this domain and highlight future plans which will push forward the development of more tools and methodologies for performing formal verification and optimal policy synthesis of stochastic processes.

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.

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.

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 specifications language, that is arguably well suited for the robotics applications, together with quantitative semantics, i.e., robustness degree. We propose a RL approach to learn tasks expressed as TLTL formulae that uses their associated robustness degree as reward functions, instead of the manually crafted heuristics trying to capture the same specifications. 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.

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.

In this work, we present a novel vision-based solution for operating a vehicle under Gaussian Distribution Temporal Logic (GDTL) constraints without global positioning infrastructure. We first present the mapping component that builds a high-resolution map of the environment by flying a team of two 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. Finally, the ground robot executes the control policy given pose estimates from a dedicated aerial robot that tracks and localizes the ground robot. The proposed method is validated using a two-wheeled ground robot and a quadrotor with a camera for ten successful experimental trials.

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