Motivated by the recent interest in cyber-physical and autonomous robotic systems, we study the problem of dynamically coupled multi-agent systems under a set of signal temporal logic tasks. In particular, the satisfaction of each of these signal temporal logic tasks depends on the behavior of a distinct set of agents. Instead of abstracting the agent dynamics and the temporal logic tasks into a discrete domain and solving the problem therein or using optimization-based methods, we derive collaborative feedback control laws. These control laws are based on a decentralized control barrier function condition that results in discontinuous control laws, as opposed to a centralized condition resembling the single-agent case. The benefits of our approach are inherent robustness properties typically present in feedback control as well as satisfaction guarantees for continuous-time multi-agent systems. More specifically, time-varying control barrier functions are used that account for the semantics of the signal temporal logic tasks at hand. For a certain fragment of signal temporal logic tasks, we further propose a systematic way to construct such control barrier functions. Finally, we show the efficacy and robustness of our framework in an experiment including a group of three omnidirectional robots.
Recent work has shown that stabilizing an affine control system to a desired state while optimizing a quadratic cost subject to state and control constraints can be reduced to a sequence of Quadratic Programs (QPs) by using Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs). In our own recent work, we defined High Order CBFs (HOCBFs) for systems and constraints with arbitrary relative degrees. In this paper, in order to accommodate initial states that do not satisfy the state constraints and constraints with arbitrary relative degree, we generalize HOCBFs to High Order Cont…
University of Modena and Reggio Emilia（摩德纳-雷焦艾米利亚大学）；École Polytechnique de Montréal（蒙特利尔理工学院）
Connectivity maintenance is crucial for the real world deployment of multi-robot systems, as it ultimately allows the robots to communicate, coordinate and perform tasks in a collaborative way. A connectivity maintenance controller must keep the multi-robot system connected independently from the system's mission and in the presence of undesired real world effects such as communication delays, model errors, and computational time delays, among others. In this paper we present the implementation, on a real robotic setup, of a connectivity maintenance control strategy based on Control Barrier Fu…
In this work we formulate the satisfaction of a (syntactically co-safe) linear temporal logic specification on a physical plant through a recent hybrid dynamical systems formalism. In order to solve this problem, we introduce an extension to such a hybrid system framework of the so-called eventuality property, which matches suitably the condition for the satisfaction of such a temporal logic specification. The eventuality property can be established through barrier certificates, which we derive for the considered hybrid system framework. Using a hybrid barrier certificate, we propose a solutio…
We study the problem of controlling multi-agent systems under a set of signal temporal logic tasks. Signal temporal logic is a formalism that is used to express time and space constraints for dynamical systems. Recent methods to solve the control synthesis problem for single-agent systems under signal temporal logic tasks are, however, subject to a high computational complexity. Methods for multi-agent systems scale at least linearly with the number of agents and induce even higher computational burdens. We propose a computationally-efficient control strategy to solve the multi-agent control s…
We propose control barrier functions (CBFs) for a family of dynamical systems to satisfy a broad fragment of Signal Temporal Logic (STL) specifications, which may include subtasks with nested temporal operators or conflicting requirements (e.g., achieving multiple subtasks within the same time interval). The proposed CBFs take into account the actuation limits of the dynamical system as well as a feasible sequence of subtasks, and they define time-varying feasible sets of states the system must always stay inside. We show some theoretical results on the correctness of the proposed method. We i…
We present a compositional control synthesis method based on assume-guarantee contracts with application to correct-by-construction design of vehicular mission plans. In our approach, a mission-level specification expressed in a fragment of signal temporal logic (STL) is decomposed into predicates defined on non-overlapping time intervals. The STL predicates are then mapped to an aggregation of contracts associated with continuously differentiable time-varying control barrier functions. The barrier functions are used to constrain the lower-level control synthesis problem, which is solved via q…
This paper investigates a collaborative rover-copter path planning and exploration with temporal logic specifications under uncertain environments. The objective of the rover is to complete a mission expressed by a syntactically co-safe linear temporal logic (scLTL) formula, while the objective of the copter is to actively explore the environment and reduce its uncertainties, aiming at assisting the rover and enhancing the efficiency of the mission completion. To formalize our approach, we first capture the environmental uncertainties by environmental beliefs of the atomic propositions, under …
Temporal logic has been widely used to express complex task specifications for cyber-physical systems (CPSs). One way to synthesize a controller for CPS under temporal logic constraints is to first abstract the CPS as a discrete transition system, and then apply formal methods. This approach, however, is computationally demanding and its scalability suffers due to the curse of dimensionality. In this paper, we propose a control barrier function (CBF) approach to abstraction-free control synthesis under a linear temporal logic (LTL) constraint. We first construct the deterministic Rabin automat…
For a class of spatio-temporal tasks defined by a fragment of Signal Temporal Logic (STL), we construct a nonsmooth time-varying control barrier function (CBF) and develop a controller based on a set of simple optimization problems. Each of the optimization problems invokes constraints that allow to exploit the piece-wise smoothness of the CBF for optimization additionally to the common gradient constraint in the context of CBFs. In this way, the conservativeness of the control approach is reduced in those points where the CBF is nonsmooth. Thereby, nonsmooth CBFs become applicable to time-var…
This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discrete-time dynamics. The temporal logic specification is given in safe-LTL_F, a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zero-sum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximized the p…
A successful defensive strategy in ice hockey games is often designed empirically by an experienced professional. The majority of previous work on automating the strategy focuses on analyzing spatial data to decide the most optimal formation and action but cannot generalize the system to real games with real-time capabilities. We propose a novel control logic for generating real-time ice hockey defensive motion based on a control barrier function (CBF) and coverage control to extend our antecessors' logic that succeeds in duplicating ideal formations for specific scenes. To this end, we first …
Patching Control Lyapunov Barrier Functions for Temporal Logic Specifications with Bounded Controls
Massachusetts Institute of Technology（麻省理工学院）；University of Waterloo（滑铁卢大学）；MacLean Engineering & Marketing Co. Limited（麦克林工程与营销有限公司）；Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
Feasibility-aware Learning of Robust Temporal Logic Controllers using BarrierNet
Amazon Robotics（亚马逊机器人）；Department of Mechanical Engineering（机械工程系）；Worcester Polytechnic Institute（沃斯堡技术学院）；Department of Electrical and Computer Engineering and the Department of Computer Science（电气与计算机工程系和计算机科学系）
The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our approach combines automata-based verification and the use of barrier certificates. It relies on decomposing the automaton associated with the negation of specification into a sequence of simpler reachabi…
This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our proposed methodology involves decomposition of interconnected systems into smaller subsystems and leverages the notion of control sub-barrier certificates of subsystems, enabling one to construct control barrier certificates of interconnected systems by employing some max-type small-gain conditions. The main goal is to synthesize hybrid controllers enforcing com…
This paper presents control strategies based on time-varying convergent higher order control barrier functions for a class of leader-follower multi-agent systems under signal temporal logic (STL) tasks. Each agent is assigned a local STL task which may be dependent on the behavior of agents involved in other tasks. The leader has knowledge on the associated tasks and controls the performance of the subgroup involved agents. Robust solutions for the task satisfaction, based on the leader's accessibility to the follower agents' states are suggested. Our approach finds solutions to guarantee the …
University of Genova（热那亚大学）；Italian Institute of Technology（意大利理工学院）
As robotic technology advances, the barriers to the coexistence of humans and robots are slowly coming down. Application domains like elderly care, collaborative manufacturing, collaborative manipulation, etc., are considered the need of the hour, and progress in robotics holds the potential to address many societal challenges. The future socio-technical systems constitute of blended workforce with a symbiotic relationship between human and robot partners working collaboratively. This thesis attempts to address some of the research challenges in enabling human-robot collaboration. In particula…
Road intersections are widely recognized as a lead cause for accidents and traffic delays. In a future scenario with a significant adoption of Cooperative Autonomous Vehicles, solutions based on fully automatic, signage-less Intersection Control would become viable. Such a solution, however, requires communication between vehicles and, possibly, the infrastructure over wireless networks. This increases the attack surface available to a malicious actor, which could lead to dangerous situations. In this paper, we address the safety of Intersection Control algorithms, and design a Sliding-Mode-Ob…
In this paper, we study formal synthesis of control policies for partially observed jump-diffusion systems against complex logic specifications. Given a state estimator, we utilize a discretization-free approach for formal synthesis of control policies by using a notation of control barrier functions without requiring any knowledge of the estimation accuracy. Our goal is to synthesize an offline control policy providing (potentially maximizing) a lower bound on the probability that the trajectories of the partially observed jump-diffusion system satisfy some complex specifications expressed by…
Multi-agent partially observable Markov decision processes (MPOMDPs) provide a framework to represent heterogeneous autonomous agents subject to uncertainty and partial observation. In this paper, given a nominal policy provided by a human operator or a conventional planning method, we propose a technique based on barrier functions to design a minimally interfering safety-shield ensuring satisfaction of high-level specifications in terms of linear distribution temporal logic (LDTL). To this end, we use sufficient and necessary conditions for the invariance of a given set based on discrete-time…
This paper presents a control strategy based on a new notion of time-varying fixed-time convergent control barrier functions (TFCBFs) for a class of coupled multi-agent systems under signal temporal logic (STL) tasks. In this framework, each agent is assigned a local STL task regradless of the tasks of other agents. Each task may be dependent on the behavior of other agents which may cause conflicts on the satisfaction of all tasks. Our approach finds a robust solution to guarantee the fixed-time satisfaction of STL tasks in a least violating way and independent of the agents' initial conditio…
In this work, we propose a compositional framework for the construction of control barrier functions for networks of continuous-time stochastic hybrid systems enforcing complex logic specifications expressed by finite-state automata. The proposed scheme is based on a notion of so-called pseudo-barrier functions computed for subsystems, by employing which one can synthesize hybrid controllers for interconnected systems enforcing complex specifications over a finite-time horizon. Particularly, we first leverage sufficient small-gain type conditions to compositionally construct control barrier fu…
In this paper we study the problem of synthesizing optimal control policies for uncertain continuous-time nonlinear systems from syntactically co-safe linear temporal logic (scLTL) formulas. We formulate this problem as a sequence of reach-avoid optimal control sub-problems. We show that the resulting hybrid optimal control policy guarantees the satisfaction of a given scLTL formula by constructing a barrier certificate. Since solving each optimal control problem may be computationally intractable, we take a learning-based approach to approximately solve this sequence of optimal control proble…
This letter offers a novel approach to Test and Evaluation of pre-existing controllers from a control barrier function and dynamics perspective. More aptly, prior Test and Evaluation techniques tend to require apriori knowledge of a space of allowable disturbances. Our work, however, determines a two-norm disturbance-bound rejectable by a system's controller without requiring specific knowledge of these disturbances beforehand. The authors posit that determination of such a disturbance bound offers a better understanding of the robustness with which a given controller achieves a specified task…
In this paper, we develop safe reinforcement-learning-based controllers for systems tasked with accomplishing complex missions that can be expressed as linear temporal logic specifications, similar to those required by search-and-rescue missions. We decompose the original mission into a sequence of tracking sub-problems under safety constraints. We impose the safety conditions by utilizing barrier functions to map the constrained optimal tracking problem in the physical space to an unconstrained one in the transformed space. Furthermore, we develop policies that intermittently update the contr…
Control Synthesis for Multi-Agent Systems under Metric Interval Temporal Logic Specifications
ACCESS Linnaeus Center, School of Electrical Engineering and KTH Center for Autonomous Systems, KTH Royal Institute of Technology（林奈 ACCESS 中心、电气工程学院及 KTH 自主系统中心，KTH 皇家理工学院）
