We propose a method to decompose signal temporal logic tasks for multi-agent systems under communication constraints. Specifically, given a task graph representing task dependencies among couples of agents in the system, we propose to decompose tasks assigned to couples of agents not connected in the communication graph by a set of sub-tasks assigned to couples of communicating agents over the communication graph. To this end, we parameterize the predicates' level set of tasks to be decomposed as hyper-rectangles with parametric centres and dimensions. Convex optimization is then leveraged to find optimal parameters maximising the volume of the predicate's level sets. Moreover, a formal treatment of conflicting conjunctions of formulas in the considered STL fragment is introduced, including sufficient conditions to avoid the insurgence of such conflicts in the final decomposition.

This paper proposes a novel control framework for handling (potentially coupled) multiple time-varying output constraints for uncertain nonlinear systems. First, it is shown that the satisfaction of multiple output constraints boils down to ensuring the positiveness of a scalar variable (the signed distance from the time-varying output-constrained set’s boundary). Next, a single funnel constraint is designed properly, whose satisfaction ensures convergence to and invariance of the time-varying output-constrained set. Then a robust and low-complexity funnel-based feedback controller is designed employing the prescribed performance control method. Finally, a simulation example clarifies and verifies the proposed approach 

This brief presents the implementation and experimental results of two frameworks for multi-agent systems under temporal logic tasks, which we have recently proposed. Each agent is subject to either a local linear temporal logic (LTL) or a local signal temporal logic (STL) task where each task may further be coupled, i.e., the satisfaction of a task may depend on more than one agent. The agents are represented by mobile robots with different sensing and actuation capabilities. We propose to combine the two aforementioned frameworks to use the strengths of both LTL and STL. For the implementation, we take into account practical issues, such as collision avoidance, and, in particular, for the STL framework, input saturation, the digital implementation of continuous-time feedback control laws, and a controllability assumption that was made in the original work. The experimental results contain three scenarios that show a wide variety of tasks.

Temporal logics have lately proven to be a valuable tool for various control applications by providing a rich specification language. Existing temporal logic-based control strategies discretize the underlying dynamical system in space and/or time. We will not use such an abstraction and consider continuous-time systems under a fragment of signal temporal logic specifications by using the associated robust semantics. In particular, this paper provides computationally-efficient funnel-based feedback control laws for a class of systems that are, in a sense, feedback equivalent to single integrator systems, but where the dynamics are partially unknown for the control design so that some degree of robustness is obtained. We first leverage the transient properties of a funnel-based feedback control strategy to maximize the robust semantics of some atomic temporal logic formulas. We then guarantee the satisfaction for specifications consisting of conjunctions of such atomic temporal logic formulas with overlapping time intervals by a suitable switched control system. The result is a framework that satisfies temporal logic specifications with a user-defined robustness when the specification is satisfiable. When the specification is not satisfiable, a least violating solution can be found. The theoretical findings are demonstrated in simulations of the nonlinear Lotka–Volterra equations for predator–prey models.

Motivated by the recent interest in cyber-physicaland autonomous robotic systems, we study the problem ofdynamically coupled multi-agent systems under a set of signaltemporal logic tasks. In particular, the satisfaction of each ofthese signal temporal logic tasks depends on the behavior of adistinct set of agents. Instead of abstracting the agent dynamicsand the temporal logic tasks into a discrete domain and solvingthe problem therein or using optimization-based methods, wederive collaborative feedback control laws. These control laws arebased on a decentralized control barrier function condition thatresults in discontinuous control laws, as opposed to a centralizedcondition resembling the single-agent case. The benefits of ourapproach are inherent robustness properties typically present infeedback control as well as satisfaction guarantees for continuous-time multi-agent systems. More specifically, time-varying controlbarrier functions are used that account for the semantics of thesignal temporal logic tasks at hand. For a certain fragment ofsignal temporal logic tasks, we further propose a systematic wayto construct such control barrier functions. Finally, we showthe efficacy and robustness of our framework in an experimentincluding a group of three omnidirectional robots

Temporal logics provide a formalism for expressing complex system specifications. A large body of literature has addressed the verification and the control synthesis problem for deterministic systems under such specifications. For stochastic systems or systems operating in unknown environments, however, only the probability of satisfying a specification has been considered so far, neglecting the risk of not satisfying the specification. Towards addressing this shortcoming, we consider, for the first time, risk metrics, such as (but not limited to) the Conditional Value-at-Risk, and propose risk signal temporal logic. Specifically, we compose risk metrics with stochastic predicates to consider the risk of violating certain spatial specifications. As a particular instance of such stochasticity, we consider control systems in unknown environments and present a determinization of the risk signal temporal logic specification to transform the stochastic control problem into a deterministic one. For unicycle-like dynamics, we then extend our previous work on deterministic time-varying control barrier functions.

We present a general framework for risk semantics on Signal Temporal Logic (STL) specifications for stochastic dynamical systems using axiomatic risk theory. We show that under our recursive risk semantics, risk constraints on STL formulas can be expressed in terms of risk constraints on atomic predicates. We then show how this allows a (stochastic) STL risk constraint to be transformed into a risk-tightened deterministic STL constraint on a related deterministic nominal system, enabling the application of existing STL methods. For affine predicate functions and a (coherent) Distributionally Robust Value at Risk measure, we show how risk constraints on atomic predicates can be reformulated as tightened deterministic affine constraints. We demonstrate the framework using a Model Predictive Control (MPC) design with an STL risk constraint.

The use of spatio-temporal logics in control is motivated by the need to impose complex spatial and temporal behavior on dynamical systems, and to control these systems accordingly. Synthesizing correct-by-design control laws is a challenging task resulting in computationally demanding methods. We consider efficient automata-based planning for continuous-time systems under signal interval temporal logic specifications, an expressive fragment of signal temporal logic. The planning is based on recent results for automata-based verification of metric interval temporal logic. A timed signal transducer is obtained accepting all Boolean signals that satisfy a metric interval temporal logic specification, which is abstracted from the signal interval temporal logic specification at hand. This transducer is modified to account for the spatial properties of the signal interval temporal logic specification, characterizing all real-valued signals that satisfy this specification. Using logic-based feedback control laws, such as the ones we have presented in earlier works, we then provide an abstraction of the system that, in a suitable way, aligns with the modified timed signal transducer. This allows to avoid the state space explosion that is typically induced by forming a product automaton between an abstraction of the system and the specification.

Inspired by the success of imitation and inverse reinforcement learning in replicating expert behavior through optimal control, we propose a learning based approach to safe controller synthesis based on control barrier functions (CBFs). We consider the setting of a known nonlinear control affine dynamical system and assume that we have access to safe trajectories generated by an expert - a practical example of such a setting would be a kinematic model of a self-driving vehicle with safe trajectories (e.g., trajectories that avoid collisions with obstacles in the environment) generated by a human driver. We then propose and analyze an optimization based approach to learning a CBF that enjoys provable safety guarantees under suitable Lipschitz smoothness assumptions on the underlying dynamical system. A strength of our approach is that it is agnostic to the parameterization used to represent the CBF, assuming only that the Lipschitz constant of such functions can be efficiently bounded. Furthermore, if the CBF parameterization is convex, then under mild assumptions, so is our learning process. We end with extensive numerical evaluations of our results on both planar and realistic examples, using both random feature and deep neural network parameterizations of the CBF. To the best of our knowledge, these are the first results that learn provably safe control barrier functions from data.

Motivated by the lack of systematic tools to obtain safe control laws for hybrid systems, we propose an optimization-based framework for learning certifiably safe control laws from data. In particular, we assume a setting in which the system dynamics are known and in which data exhibiting safe system behavior is available. We propose hybrid control barrier functions for hybrid systems as a means to synthesize safe control inputs. Based on this notion, we present an optimization-based framework to learn such hybrid control barrier functions from data. Importantly, we identify sufficient conditions on the data such that feasibility of the optimization problem ensures correctness of the learned hybrid control barrier functions, and hence the safety of the system. We illustrate our findings in two simulations studies, including a compass gait walker.