Author name cluster

Calin Belta

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

40 papers

2 author rows

ICRA Conference 2023 Conference Paper

Safe Model-based Control from Signal Temporal Logic Specifications Using Recurrent Neural Networks

Wenliang Liu 0001
Mirai Nishioka
Calin Belta

We propose a policy search approach to learn controllers from specifications given as Signal Temporal Logic (STL) formulae. The system model, which is unknown but assumed to be an affine control system, is learned together with the control policy. The model is implemented as two feedforward neural networks (FNNs) - one for the drift, and one for the control directions. To capture the history dependency of STL specifications, we use a recurrent neural network (RNN) to implement the control policy. In contrast to prevalent model-free methods, the learning approach proposed here takes advantage of the learned model and is more efficient. We use control barrier functions (CBFs) with the learned model to improve the safety of the system. We validate our algorithm via simulations and experiments. The results show that our approach can satisfy the given specification within very few system runs, and can be used for on-line control.

IROS Conference 2022 Conference Paper

Classification of Time-Series Data Using Boosted Decision Trees

Erfan Aasi
Cristian Ioan Vasile
Mahroo Bahreinian
Calin Belta

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.

IROS Conference 2021 Conference Paper

The Reasonable Crowd: Towards evidence-based and interpretable models of driving behavior

Bassam Helou
Aditya Dusi
Anne Collin
Noushin Mehdipour
Zhiliang Chen
Cristhian Lizarazo
Calin Belta
Tichakorn Wongpiromsarn

Autonomous vehicles must balance a complex set of objectives. There is no consensus on how they should do so, nor on a model for specifying a desired driving behavior. We created a dataset to help address some of these questions in a limited operating domain. The data consists of 92 traffic scenarios, with multiple ways of traversing each scenario. Multiple annotators expressed their preference between pairs of scenario traversals. We used the data to compare an instance of a rulebook [1], carefully hand-crafted independently of the dataset, with several interpretable machine learning models such as Bayesian networks, decision trees, and logistic regression trained on the dataset. To compare driving behavior, these models use scores indicating by how much different scenario traversals violate each of 14 driving rules. The rules are interpretable and designed by subject-matter experts. First, we found that these rules were enough for these models to achieve a high classification accuracy on the dataset. Second, we found that the rulebook provides high interpretability without excessively sacrificing performance. Third, the data pointed to possible improvements in the rulebook and the rules, and to potential new rules. Fourth, we explored the interpretability vs performance trade-off by also training non-interpretable models such as a random forest. Finally, we make the dataset publicly available to encourage a discussion from the wider community on behavior specification for AVs. Please find it at github.com/bassam-motional/Reasonable-Crowd.

IROS Conference 2018 Conference Paper

Distributed Sensing Subject to Temporal Logic Constraints

Zachary T. Serlin
Kevin Leahy 0001
Roberto Tron
Calin Belta

This paper considers the combination of temporal logic (TL) specifications and local objective functions to create online, multiagent, motion plans. These plans are guaranteed to satisfy a persistent mission TL specification and locally optimize an objective function (e. g. in this paper, a cost based on information entropy). The presented approach decouples the two tasks by assigning sub-teams of agents to fulfill the TL specification, while unassigned agents optimize the objective function locally. This paper also presents a novel decoupling of the classic product automaton based approach while maintaining satisfaction guarantees. We also qualitatively show that optimality loss in the local greedy minimization due to the TL constraints can be approximated based on specification complexity. This approach is evaluated with a set of simulations and an experiment of 6 robots with real sensors.

ICRA Conference 2017 Conference Paper

Minimum-violation scLTL motion planning for mobility-on-demand

Cristian Ioan Vasile
Jana Tumova
Sertac Karaman
Calin Belta
Daniela Rus

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.

IROS Conference 2017 Conference Paper

Reinforcement learning with temporal logic rewards

Xiao Li 0013
Cristian Ioan Vasile
Calin Belta

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.

TCS Journal 2017 Journal Article

Time window temporal logic

Cristian-Ioan Vasile
Derya Aksaray
Calin Belta

This paper introduces time window temporal logic (TWTL), a rich expressive 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.

ICRA Conference 2016 Conference Paper

Dynamic routing of energy-aware vehicles with Temporal Logic Constraints

Derya Aksaray
Cristian Ioan Vasile
Calin Belta

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.

TIME Conference 2014 Conference Paper

Formal Methods for Dynamical Systems

Calin Belta

In control theory, "complex" models of physical processes, such as systems of differential equations, are usually checked against "simple" specifications, such as stability and set invariance. In formal methods, "rich" specifications, such as languages and formulae of temporal logics, are checked against "simple" models of software programs and digital circuits, such as finite transition graphs. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. The formal verification and synthesis problems have been shown to be undecidable even for very simple classes of infinitespace continuous and hybrid systems. However, provably correct but conservative approaches, in which the satisfaction of a property by a dynamical system is implied by the satisfaction of the property by a finite over-approximation (abstraction) of the system, have received a lot of attention in recent years. Some classes of systems allowing for computationally efficient verification and control from temporal logic specifications are reviewed. For continuous and discrete-time linear systems and continuous-time multi-linear systems, it is shown that finite abstractions can be constructed through polyhedral operations only. By using techniques from model checking and automata games, this allows for verification and control from specifications given as Linear Temporal Logic (LTL) formulae over linear predicates in the state variables. A connection between the existence of Lyapunov functions and finite bisimulations is established for discrete-time linear and switched linear systems. Finally, optimality and correctness requirements are combined in a model predictive approach to generate control strategies for discrete-time linear systems. The usefulness of these computational tools is illustrated with various examples such as verification and synthesis of biological circuits in synthetic biology and motion planning and control in robotics.

ICRA Conference 2014 Conference Paper

Reactive sampling-based temporal logic path planning

Cristian Ioan Vasile
Calin Belta

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.

ICRA Conference 2013 Conference Paper

A receding horizon algorithm for informative path planning with temporal logic constraints

Austin Jones
Mac Schwager
Calin Belta

This paper considers the problem of finding the most informative path for a sensing robot under temporal logic constraints, a richer set of constraints than have previously been considered in information gathering. An algorithm for informative path planning is presented that leverages tools from information theory and formal control synthesis, and is proven to give a path that satisfies the given temporal logic constraints. The algorithm uses a receding horizon approach in order to provide a reactive, on-line solution while mitigating computational complexity. Statistics compiled from multiple simulation studies indicate that this algorithm performs better than a baseline exhaustive search approach.

ICRA Conference 2013 Conference Paper

Control of noisy differential-drive vehicles from time-bounded temporal logic specifications

Igor Cizelj
Calin Belta

We address the problem of controlling a noisy differential drive mobile robot such that the probability of satisfying a specification given as a Bounded Linear Temporal Logic (BLTL) formula over a set of properties at the regions in the environment is maximized. We assume that the vehicle can precisely determine its initial position in a known map of the environment. However, inspired by practical limitations, we assume that the vehicle is equipped with noisy actuators and, during its motion in the environment, it can only measure the angular velocity of its wheels using limited accuracy incremental encoders. Assuming the duration of the motion is finite, we map the measurements to a Markov Decision Process (MDP). We use recent results in Statistical Model Checking (SMC) to obtain an MDP control policy that maximizes the probability of satisfaction. We translate this policy to a vehicle feedback control strategy and show that the probability that the vehicle satisfies the specification in the environment is bounded from below by the probability of satisfying the specification on the MDP. We illustrate our method with simulations and experimental results.

ICRA Conference 2013 Conference Paper

Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications

Tichakorn Wongpiromsarn
Alphan Ulusoy
Calin Belta
Emilio Frazzoli
Daniela Rus

We consider automatic synthesis of control policies for non-independent, heterogeneous multi-agent systems with the objective of maximizing the probability of satisfying a given specification. The specification is expressed as a formula in linear temporal logic. The agents are modeled by Markov decision processes with a common set of actions. These actions, however, may or may not affect the behaviors of all the agents. To alleviate the well-known state explosion problem, an incremental approach is proposed where only a small subset of agents is incorporated in the synthesis procedure initially and more agents are successively added until the limitations on computational resources are reached. The proposed algorithm runs in an anytime fashion, where the probability of satisfying the specification increases as the algorithm progresses.

IROS Conference 2013 Conference Paper

Negotiating the probabilistic satisfaction of temporal logic motion specifications

Igor Cizelj
Calin Belta

We propose a human-supervised control synthesis method for a stochastic Dubins vehicle such that the probability of satisfying a specification given as a formula in a fragment of Probabilistic Computational Tree Logic (PCTL) over a set of environmental properties is maximized. Under some mild assumptions, we construct a finite approximation for the motion of the vehicle in the form of a tree-structured Markov Decision Process (MDP). We introduce an efficient algorithm, which exploits the tree structure of the MDP, for synthesizing a control policy that maximizes the probability of satisfaction. For the proposed PCTL fragment, we define the specification update rules that guarantee the increase (or decrease) of the satisfaction probability. We introduce an incremental algorithm for synthesizing an updated MDP control policy that reuses the initial solution. The initial specification can be updated, using the rules, until the supervisor is satisfied with both the updated specification and the corresponding satisfaction probability. We propose an offline and an online application of this method.

IROS Conference 2013 Conference Paper

Sampling-based temporal logic path planning

Cristian Ioan Vasile
Calin Belta

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.

ICRA Conference 2013 Conference Paper

Temporal logic control for an autonomous quadrotor in a nondeterministic environment

Alphan Ulusoy
Michael Marrazzo
Konstantinos Oikonomopoulos
Ryan Hunter
Calin Belta

We present an experimental setup for automatic deployment of a quadrotor in an environment with known topology and nondeterministically changing properties. The missions are specified as rich, temporal logic statements about the satisfaction of the properties. The main objective is to be able to synthesize, test, and evaluate control policies for complex aerial missions. Our testbed consists of quadrotors, a motion capture system that provides precise and continuous position information of the quadrotor, projectors that can emulate dynamically changing environments, physical obstacles, and computers that control the quadrotor, the motion capture system, and the projectors. Our computational approach is hierarchical. At the bottom level, we partition the environment and construct an abstraction in the form of a finite transition system such that the quadrotor can execute its transitions by using low level feedback controllers. At the top level, we draw inspiration from LTL model checking and use a value iteration algorithm to determine an optimal control policy that guarantees the satisfaction of the specification under nondeterministically changing properties. We illustrate the approach for the particular case of a surveillance mission in a city-like environment.

IROS Conference 2013 Conference Paper

Temporal logic motion planning in unknown environments

Ana I. Medina Ayala
Sean B. Andersson
Calin Belta

In this paper, we consider a robot motion planning problem from a specification given as a syntactically co-safe linear temporal logic formula over a set of properties known to be satisfied at the regions of an unknown environment. The robot is assumed to be equipped with deterministic motion and accurate sensing capabilities. The environment is assumed to be partitioned into a finite number of identical square cells. By bringing together tools from formal verification, graph theory, and grid-based exploration, we develop an incremental algorithm that makes progress towards satisfying the specification while the robot discovers the environment using its local sensors. We show that the algorithm is sound and complete. We illustrate the feasibility and effectiveness of our approach through a simulated case study.

IROS Conference 2012 Conference Paper

Incremental temporal logic synthesis of control policies for robots interacting with dynamic agents

Tichakorn Wongpiromsarn
Alphan Ulusoy
Calin Belta
Emilio Frazzoli
Daniela Rus

We consider the synthesis of control policies from temporal logic specifications for robots that interact with multiple dynamic environment agents. Each environment agent is modeled by a Markov chain whereas the robot is modeled by a finite transition system (in the deterministic case) or Markov decision process (in the stochastic case). Existing results in probabilistic verification are adapted to solve the synthesis problem. To partially address the state explosion issue, we propose an incremental approach where only a small subset of environment agents is incorporated in the synthesis procedure initially and more agents are successively added until we hit the constraints on computational resources. Our algorithm runs in an anytime fashion where the probability that the robot satisfies its specification increases as the algorithm progresses.

ICRA Conference 2012 Conference Paper

LTL robot motion control based on automata learning of environmental dynamics

Yushan Chen
Jana Tumova
Calin Belta

We develop a technique to automatically generate a control policy for a robot moving in an environment that includes elements with partially unknown, changing behavior. The robot is required to achieve an optimal surveillance mission, in which a certain request needs to be serviced repeatedly, while the expected time in between consecutive services is minimized. We define a fragment of Linear Temporal Logic (LTL) to describe such a mission and formulate the problem as a temporal logic game. Our approach is based on two main ideas. First, we extend results in automata learning to detect patterns of the partially unknown behavior of the elements in the environment. Second, we employ an automata-theoretic method to generate the control policy. We show that the obtained control policy converges to an optimal one when the unknown behavior patterns are fully learned. We implemented the proposed computational framework in MATLAB. Illustrative case studies are included.

ICRA Conference 2012 Conference Paper

Probabilistic control from time-bounded temporal logic specifications in dynamic environments

Ana I. Medina Ayala
Sean B. Andersson
Calin Belta

The increasing need for real time robotic systems capable of performing tasks in changing and constrained environments demands the development of reliable and adaptable motion planning and control algorithms. This paper considers a mobile robot whose performance is measured by the completion of temporal logic tasks within a certain period of time. In addition to such time constraints, the planning algorithm must also deal with changes in the robot's workspace during task execution. In our case, the robot is deployed in a partitioned environment subjected to structural changes in which doors shift from open to closed and vice-versa. The motion of the robot is modeled as a Continuous Time Markov Decision Process and the robot's mission is expressed as a Continuous Stochastic Logic (CSL) temporal logic specification. An approximate solution to find a control strategy that satisfies such specifications is derived for a subset of probabilistic CSL formulae. Simulation and experimental results are provided to illustrate the method.

IROS Conference 2012 Conference Paper

Probabilistically safe control of noisy Dubins vehicles

Igor Cizelj
Calin Belta

We address the problem of controlling a stochastic version of a Dubins vehicle such that the probability of satisfying a temporal logic specification over a set of properties at the regions in a partitioned environment is maximized. We assume that the vehicle can determine its precise initial position in a known map of the environment. However, inspired by practical limitations, we assume that the vehicle is equipped with noisy actuators and, during its motion in the environment, it can only measure its angular velocity using a limited accuracy gyroscope. Through quantization and discretization, we construct a finite approximation for the motion of the vehicle in the form of a Markov Decision Process (MDP). We allow for task specifications given as temporal logic statements over the environmental properties, and use tools in Probabilistic Computation Tree Logic (PCTL) to generate an MDP control policy that maximizes the probability of satisfaction. We translate this policy to a vehicle feedback control strategy and show that the probability that the vehicle satisfies the specification in the original environment is bounded from below by the maximum probability of satisfying the specification on the MDP.

ICRA Conference 2012 Conference Paper

Robust multi-robot optimal path planning with temporal logic constraints

Alphan Ulusoy
Stephen L. Smith 0001
Xu Chu Ding
Calin Belta

In this paper we present a method for automatically planning robust optimal paths for a group of robots that satisfy a common high level mission specification. Each robot's motion in the environment is modeled as a weighted transition system, and the mission is given as a Linear Temporal Logic (LTL) formula over a set of propositions satisfied by the regions of the environment. In addition, an optimizing proposition must repeatedly be satisfied. The goal is to minimize the maximum time between satisfying instances of the optimizing proposition while ensuring that the LTL formula is satisfied even with uncertainty in the robots' traveling times. We characterize a class of LTL formulas that are robust to robot timing errors, for which we generate optimal paths if no timing errors are present, and we present bounds on the deviation from the optimal values in the presence of errors. We implement and experimentally evaluate our method considering a persistent monitoring task in a road network environment.

ICRA Conference 2012 Conference Paper

Temporal logic motion control using actor-critic methods

Xu Chu Ding
Jing Wang 0044
Morteza Lahijanian
Ioannis Ch. Paschalidis
Calin Belta

In this paper, we consider the problem of deploying a robot from a specification given as a temporal logic statement about some properties satisfied by the regions of a large, partitioned environment. We assume that the robot has noisy sensors and actuators and model its motion through the regions of the environment as a Markov Decision Process (MDP). The robot control problem becomes finding the control policy maximizing the probability of satisfying the temporal logic task on the MDP. For a large environment, obtaining transition probabilities for each state-action pair, as well as solving the necessary optimization problem for the optimal policy are usually not computationally feasible. To address these issues, we propose an approximate dynamic programming framework based on a least-square temporal difference learning method of the actor-critic type. This framework operates on sample paths of the robot and optimizes a randomized control policy with respect to a small set of parameters. The transition probabilities are obtained only when needed. Hardware-in-the-loop simulations confirm that convergence of the parameters translates to an approximately optimal policy.

IROS Conference 2011 Conference Paper

Optimal multi-robot path planning with Temporal Logic constraints

Alphan Ulusoy
Stephen L. Smith 0001
Xu Chu Ding
Calin Belta
Daniela Rus

In this paper we present a method for automatically planning optimal paths for a group of robots that satisfy a common high level mission specification. Each robot's motion in the environment is modeled as a weighted transition system. The mission is given as a Linear Temporal Logic formula. In addition, an optimizing proposition must repeatedly be satisfied. The goal is to minimize the maximum time between satisfying instances of the optimizing proposition. Our method is guaranteed to compute an optimal set of robot paths. We utilize a timed automaton representation in order to capture the relative position of the robots in the environment. We then obtain a bisimulation of this timed automaton as a finite transition system that captures the joint behavior of the robots and apply our earlier algorithm for the single robot case to optimize the group motion. We present a simulation of a persistent monitoring task in a road network environment.

IROS Conference 2011 Conference Paper

Temporal logic control in dynamic environments with probabilistic satisfaction guarantees

Ana I. Medina Ayala
Sean B. Andersson
Calin Belta

Mobile robotic systems move in environments that are constantly changing due to the presence of dynamic obstacles. In this work we consider one such environment in which the dynamic nature comes from doors that can open or close during the robot's mission. We derive a solution to the automatic deployment of a robot from a temporal logic specification assuming three different levels of knowledge and sensing capabilities of the robot. Under each one of these settings, the motion of the robot is modeled either as a Markov decision process (MDP) or mixed observability MDP. The objective is to find a control strategy that maximizes the probability of satisfying a specification given in Probabilistic Computation Tree Logic (PCTL). We describe an optimal solution in one setting and sub-optimal, reactive solutions in the other two. We illustrate our methods with simulation results.

IROS Conference 2010 Conference Paper

A hierarchical approach to automatic deployment of robotic teams with communication constraints

Yushan Chen
Sam Birch
Alin Stefanescu
Calin Belta

We consider the following problem: GIVEN (1) a set of service requests occurring at known locations in an environment, (2) a set of temporal and logical constraints on how the requests need to be serviced, (3) a team of robots and their capacities to service the requests individually or through collaboration, FIND robot control and communication strategies guaranteeing the correct servicing of the requests. Our approach is hierarchical. At the top level, we check whether the specification, which is a regular expression over the requests, is distributable among the robots given their service and cooperation capabilities; if the answer is positive, we generate individual specifications in the form of finite state automata, and interaction rules in the form of synchronizations on shared requests. At the bottom level, we check whether the local specifications and the synchronizations can be implemented given the motion and communication constraints of the robots; if the answer is positive, we generate robot motion and service plans, which are then mapped to control and communication strategies. We illustrate the method with experimental and simulation results.

ICRA Conference 2010 Conference Paper

Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees

Morteza Lahijanian
Joseph Wasniewski
Sean B. Andersson
Calin Belta

We present a computational framework for automatic deployment of a robot from a temporal logic specification over a set of properties of interest satisfied at the regions of a partitioned environment. We assume that, during the motion of the robot in the environment, the current region can be precisely determined, while due to sensor and actuation noise, the outcome of a control action can only be predicted probabilistically. Under these assumptions, the deployment problem translates to generating a control strategy for a Markov Decision Process (MDP) from a temporal logic formula. We propose an algorithm inspired from probabilistic Computation Tree Logic (PCTL) model checking to find a control strategy that maximizes the probability of satisfying the specification. We illustrate our method with simulation and experimental results.

ICRA Conference 2010 Conference Paper

On the need for communication in distributed implementations of LTL motion specifications

Marius Kloetzer
Sanjiv Itani
Sam Birch
Calin Belta

We revisit the problem of automatic deployment of robotic teams from temporal logic specifications over regions of interests in the environment. In our previous work, we developed an algorithm that could accommodate arbitrary communication constraints, but had two main limitations: (1) it only allowed for communicating robots to move, and (2) it was computationally very expensive. In this paper, we present two approaches to address these limitations. First, we show that if identical robots are allowed to communicate for all times, then the computation is cheaper. Second, we develop an algorithm to test if a given global specification can be implemented by the robots without the move-only-when-communicate constraint.

IROS Conference 2010 Conference Paper

Optimal path planning under temporal logic constraints

Stephen L. Smith 0001
Jana Tumova
Calin Belta
Daniela Rus

In this paper we present a method for automatically generating optimal robot trajectories satisfying high level mission specifications. The motion of the robot in the environment is modeled as a weighted transition system. The mission is specified by a general linear temporal logic formula. In addition, we require that an optimizing proposition must be repeatedly satisfied. The cost function that we seek to minimize is the maximum time between satisfying instances of the optimizing proposition. For every environment model, and for every formula, our method computes a robot trajectory which minimizes the cost function. The problem is motivated by robotic monitoring and data gathering. In this setting, the optimizing proposition is satisfied at locations where data can be uploaded, and the formula specifies a an infinite horizon data collection mission. Our method utilizes Büchi automata to produce an automaton (which can be thought of as a graph) whose runs satisfy the temporal logic formula. We then present a graph algorithm which computes a path corresponding to the optimal robot trajectory. We also present an implementation for a robot performing a data gathering mission.

ICRA Conference 2009 Conference Paper

Automatic deployment of autonomous cars in a Robotic Urban-Like Environment (RULE)

Morteza Lahijanian
Marius Kloetzer
Sara Itani
Calin Belta
Sean B. Andersson

We present a computational framework and experimental setup for deployment of autonomous cars in a miniature Robotic Urban-Like Environment (RULE). The specifications are given in rich, human-like language as temporal logic statements about roads, intersections, and parking spaces. We use transition systems to model the motion and sensing capabilities of the robots and the topology of the environment and use tools resembling model checking to generate robot control strategies and to verify the correctness of the solution. The experimental setup is based on Khepera III robots, which move autonomously on streets while observing traffic rules.

ICRA Conference 2008 Conference Paper

Distributed implementations of global temporal logic motion specifications

Marius Kloetzer
Calin Belta

We present a computational framework for automatic synthesis of decentralized communication and control strategies for a robotic team from global specifications given as temporal and logic statements about visiting regions of interest in a partitioned environment. We consider a purely discrete scenario where the robots move among the vertices of a graph. However, by employing recent results on invariance and facet reachability for dynamical system in environments with polyhedral partitions, the framework from this paper can be directly implemented for robots with nontrivial dynamics. While providing a rich specification language and guaranteeing the correctness of the solution, our approach is conservative, in the sense that we might not find a solution even if one exists. The overall amount of required computation is large. However, most of it is performed off-line before the deployment.

ICRA Conference 2007 Conference Paper

Managing non-determinism in symbolic robot motion planning and control

Marius Kloetzer
Calin Belta

We study the problem of designing control strategies for non-deterministic transitions systems enforcing the satisfaction of linear temporal logic (LTL) formulas over their set of states. We focus on finite transition systems with inputs, which are often encountered when solving motion planning problems by using discrete quotients induced by a given partition of the state space. Our approach solves the problem conservatively using LTL games, and consists of the following three steps: (1) the original transition system is transformed into a transition system on which an LTL game can be played, (2) a solution of the LTL game on the new transition system is obtained, and (3) an interface between this solution and the initial transition system is constructed. The correctness of the method is ensured by design. The advantages and conservativeness of our approach are discussed and illustrated by simple examples.

IROS Conference 2006 Conference Paper

A Framework for Automatic Deployment of Robots in 2D and 3D Environments

Marius Kloetzer
Calin Belta

We present a computational framework for automatic deployment of robots in 2D and 3D rectangular environments with polytopal obstacles. The results are derived for polytopal robots that can only translate with velocities restricted to polyhedral sets. Our approach consists of three steps: (1) constructing a discrete representation of the problem by using hierarchical partitions in the form of quad-trees and oct-trees, (2) planning the motion in the finite dimensional quotient produced by the partition, and (3) generating provably correct robot feedback control laws by constructing a hybrid system. Given the environment and robot geometry and constraints, generation of control laws is completely automated. The computation consists of polyhedral operations and searches on graphs

ICRA Conference 2006 Conference Paper

Controlling three Dimensional Swarms of Robots

Nathan Michael
Calin Belta
Vijay Kumar 0001

We address the problem of modeling and controlling a swarm of fully actuated point-like robots in three dimensions by generalizing the planar framework from (C. Belta and V. Kumar, 2004). We define a nine-dimensional abstraction of the swarm that has a product structure of the six-dimensional Euclidean group and a three-dimensional shape, and is independent of the number of robots. The group captures the pose of an ellipsoid spanning the swarm with semiaxes given by the shape variables. The overall abstract description is invariant to robot permutations. In addition, the shape is also invariant to left actions of the group. This description allows one to define and control the behavior of the swarm at a high level, with automatic generation of individual robot control laws. We present simulation results for controlling swarms of rotorcrafts

ICRA Conference 2006 Conference Paper

Hierarchical Abstractions for Robotic Swarms

Marius Kloetzer
Calin Belta

We develop a hierarchical framework for planning and control of arbitrarily large groups of fully actuated robots with polyhedral velocity bounds (swarm) moving in polygonal environments with polygonal obstacles. At the first level of hierarchy, we aggregate the high dimensional control system of the swarm into a small dimensional control system capturing its essential features. These features describe the position of the swarm in the world and its size. At the second level, we reduce the problem of controlling the essential features of the swarm to a model checking problem. In the obtained hierarchical framework, high level specifications given in natural language such as linear temporal logic formulas over linear predicates in the essential features are automatically mapped to probably correct robot control laws

IROS Conference 2004 Conference Paper

Hybrid control for visibility-based pursuit-evasion games

Volkan Isler
Calin Belta
Kostas Daniilidis
George J. Pappas

Pursuit-evasion games in complex environments have a rich but disconnected history. Continuous or differential pursuit-evasion games focus on optimal control methods, and rely on very intense computations in order to provide locally optimal controls. Discrete pursuit-evasion games on graphs are algorithmically much more appealing, but completely ignore the physical dynamics of the players, resulting in possibly infeasible motions. In this paper, we present a provable and algorithmically feasible solution for visibility-based pursuit-evasion games in simply-connected environments, for players with dynamic constraints. This is achieved by combining two recent but distant results.

ICRA Conference 2004 Conference Paper

On Controlling Aircraft and Underwater Vehicles

Calin Belta

In this paper we make the important observation that the attitude and angular velocity control systems for gas-jet aircraft and underwater vehicles are of a special form: they are affine control systems with constant control distributions and multi-affine drifts. For this general class of systems, we can construct (and check the existence of) bounded controls driving the system from initial to final regions of the state space. This can be used for tasks requiring repositioning or changing the velocity of the vehicle under constraints on both controls and state. We illustrate the procedure by solving the problem of changing the angular velocity of a parallelepiped aircraft under velocity and control constraints imposed by the task. The method should be seen as a "maneuver" procedure, allowing automatic generation of control laws for bringing the system in a desired region of its state space. If stabilization to a point is required, then locally stabilizing control laws can be used after the maneuver.

ICRA Conference 2003 Conference Paper

Abstraction and control for groups of fully-actuated planar robots

Calin Belta
Vijay Kumar 0001

This paper shows how a large number of robots can be coordinated by designing control laws on a small dimensional manifold, independent on the number and ordering of the robots. The small dimensional description of the team has a product structure of a Lie group, which captures the dependence of the ensemble on world frame, and a shape manifold, which is an intrinsic description of the team. We design decoupled controls for group and shape. The individual control laws which are mapped to the desired collective behavior can be realized by feedback depending only on the current state of the robot and the state on the small dimensional manifold, so that the robots have to broadcast their states and only have to listen to some coordinating agent with small bandwidth.

ICRA Conference 2002 Conference Paper

Trajectory Design for Formations of Robots by Kinetic Energy Shaping

Calin Belta
Vijay Kumar 0001

We develop a method for generating smooth trajectories for a set of mobile robots. Given two end configurations, by tuning one parameter, the user can choose an interpolating trajectory from a continuum of curves varying from that corresponding to maintaining a rigid formation to motion of the robots toward each other The idea behind our method is to change the original constant kinetic energy metric in the configuration space and can be summarized into three steps. First, the energy of the motion as a rigid structure is decoupled from the energy of motion along directions that violate the rigid constraints. Next, the metric is "shaped" by assigning different weights to each term. Finally, geodesic flow is constructed for the modified metric. The optimal motions generated on the manifolds of rigid body displacements in 3D space or in plane, and the uniform rectilinear motion of each robot corresponding to a totally uncorrelated approach are particular cases of our general treatment.

ICRA Conference 2001 Conference Paper

Motion Generation for Formations of Robots a Geometric Approach

Calin Belta
Vijay Kumar 0001

Develops a method for generating smooth trajectories for mobile robots in formation. The problem of trajectory generation is cast in terms of designing optimal curves on the Euclidean group, SE(3). Specifically, the method generates the trajectory that minimizes the total energy associated with the translations and rotations of the robots, while maintaining a rigid formation. When the mobile robots are nonholonomic, trajectories that allow rigid formations to be maintained must satisfy appropriate constraints. An efficient non-iterative algorithm to obtain near-optimal trajectories is described. Finally, the approach is illustrated with examples involving formations of aircrafts.