We address the problem of decomposing a global task assigned to a multi-agent system, where the task is expressed using a fragment of Signal Temporal Logic (STL) and communication among agents is range-limited. The global task is expressed as the conjunction of local tasks over individual and relative agent's states, thus naturally inducing the definition of a task graph. Due to the limited communication range, inconsistencies among the edges of the communication and task graph prevent the application of previously derived state feedback control laws for the satisfaction of global STL tasks. To resolve this issue, we propose a task decomposition mechanism reassigning tasks between non-communicating agents to communicating ones, thus ensuring consistency between task and communication graphs. By assuming that the STL tasks are defined over concave predicate functions with polytopic super-level sets, the decomposition can be framed as a parameter optimization problem, solvable via decentralized convex optimization. To guarantee the soundness of our approach, we present various conditions under which the tasks defined in the applied STL fragment are unsatisfiable, and we derive sufficient conditions such that our decomposition approach yields satisfiable global tasks after decomposition.

Over the past decade, the rapid growth of computational power available in embedded systems has fueled increasing interest in autonomous systems with real-time planning and control capabilities, aimed at satisfying spatially and temporally defined goals. Many such systems have already become part of everyday life—for example, robotic vacuum cleaners, drone deliveries, and autonomous taxis. In this context, the control and robotics community has devoted significant effort to developing formal frameworks for rigorously defining system-level specifications and verifying progress toward their satisfaction. More specifically, when dealing with systems composed of possibly heterogeneous autonomous agents, the development of scalable and reliable coordination algorithms that can drive the agents toward the satisfaction of common objectives, while operating under limited communication capabilities, is of pivotal importance.

The work presented in this thesis lies at the intersection of multi-agent coordination and formal verification. The overarching goal is to develop task assignment, planning, and control algorithms for coordinating multi-agent systems subject to sparse communication topologies, with the objective of satisfying system-wide spatio-temporal goals. To this end, we adopt Signal Temporal Logic (STL) as the primary modeling framework, providing a precise and unambiguous language for specifying system-level objectives. In parallel, we leverage the framework of Control Barrier Functions (CBFs) to bridge high-level specifications with low-level control objectives, which can then be approached using tools from nonlinear and non-smooth analysis.

Building on this foundation, the first part of the thesis introduces a novel framework for representing inter-agent task dependencies through a task graph, where edges capture collaborative tasks among agents. Based on this representation, we design algorithms that allow task dependencies between non-communicating agents to be decomposed (or rerouted) through agents that are instead connected via communication links. This decomposition serves as a key enabler for feedback-based control approaches to achieve system-wide objectives in a scalable and reactive manner, by ensuring consistency between the given tasks and the communication dependencies imposed by the network topology.

The second part of the thesis presents a control architecture for driving a multi-agent system toward the satisfaction of a system-wide task, under the assumption that the associated task graph is acyclic. The controller we propose is implemented in a sampled-data fashion, as is typical in embedded systems, while we provide analytical results that guarantee task satisfaction in continuous time. This dual perspective bridges the gap between the digital nature of embedded control and the continuous-time dynamics of the physical system.

The third and final part of the thesis departs slightly from the content of the first two by focusing on trajectory synthesis. Specifically, we develop a sampling-based planning algorithm for generating trajectories that satisfy spatio-temporal goals for systems with linear dynamics. We will then address the extension of the proposed framework to multi-agent settings in future research endeavors.

Under det senaste decenniet har den snabba tillväxten av beräkningskraft i inbyggda system drivit på ett växande intresse för autonoma system med realtidsplanering och styrförmåga, avsedda att uppfylla rumsligt och tidsmässigt definierade mål. Många sådana system har redan blivit en del av vardagen—till exempel robotdammsugare, drönarleveranser och självkörande taxibilar. I detta sammanhang har regler- och robotikforskarsamhällena lagt ned betydande ansträngningar på att utveckla formella ramverk som gör det möjligt att specificera mål på ett stringent sätt och att verifiera systemens framsteg mot att uppfylla dessa. Mer specifikt, när det gäller system bestående av, möjligen heterogena, autonoma agenter, är utvecklingen av skalbara och tillförlitliga koordineringsalgoritmer som kan driva agenterna mot gemensamma mål, samtidigt som de verkar under begränsade kommunikationsmöjligheter, av avgörande betydelse.

Arbetet som presenteras i denna avhandling befinner sig i skärningspunkten mellan koordination av multiagentsystem och formell verifiering. Det övergripande målet är att utveckla uppdragsallokerings-, planerings- och styralgoritmer för att koordinera multiagentsystem under glesa kommunikationstopologier, med syftet att uppfylla systemövergripande spatio-temporala mål. För detta ändamål använder vi Signal Temporal Logic (STL) som det primära modelleringsramverket, vilket ger ett precist och entydigt språk för att specificera systemnivåns mål. Parallellt utnyttjar vi ramverket Control Barrier Functions (CBFs) för att överbrygga gapet mellan hög nivå-specifikationer och låg nivå-styrmål, vilka sedan kan angripas med hjälp av verktyg från icke-linjär och icke-slät analys.

Med denna grund introducerar den första delen av avhandlingen ett nytt ramverk för att representera uppgiftsberoenden mellan agenter genom en uppgiftsgraf, där kanterna beskriver samarbetsuppgifter mellan agenter. Baserat på denna representation utformar vi algoritmer som gör det möjligt att bryta ned eller omdirigera uppgiftsberoenden mellan agenter som saknar direkt kommunikation, via agenter som delar kommunikationslänkar. Denna nedbrytning utgör en central möjliggörare för återkopplingsbaserade styrmetoder som kan uppfylla systemövergripande mål på ett skalbart och reaktivt sätt, genom att säkerställa överensstämmelse mellan givna uppgifter och de kommunikationsberoenden som nätverkets topologi medför.

Den andra delen av avhandlingen presenterar en styrarkitektur för att driva ett multiagentsystem mot uppfyllelsen av ett systemövergripande mål, under antagandet att den associerade uppgiftsgrafen är acyklisk. Det föreslagna reglersystemet implementeras i sampled-data-form, vilket är typiskt för inbyggda system, samtidigt som vi tillhandahåller analytiska resultat som garanterar måluppfyllelse i kontinuerlig tid. Detta dubbla perspektiv överbrygger gapet mellan den digitala naturen hos inbyggd styrning och den kontinuerliga tidens dynamik i det fysiska systemet.

Den tredje och sista delen av avhandlingen avviker något från innehållet i de två första genom att fokusera på trajektoriesyntes. Mer specifikt utvecklar vi en sampling-baserad planeringsalgoritm för att generera banor som uppfyller spatio-temporala mål för system med linjär dynamik. Vi kommer vidare att behandla utvidgningen av det föreslagna ramverket till multiagentinställningar som framtida forskning.

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.

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.

We introduce a novel distributed sampled-data control method tailored for heterogeneous multi-agent systems under a global spatio-temporal task with acyclic dependencies. Specifically, we consider the global task as a conjunction of independent and collaborative tasks, defined over the absolute and relative states of agent pairs. Task dependencies in this form are then represented by a task graph, which we assume to be acyclic. From the given task graph, we provide an algorithmic approach to define a distributed sampled-data controller prioritizing the fulfilment of collaborative tasks as the primary objective, while fulfilling independent tasks unless they conflict with collaborative ones. Moreover, communication maintenance among collaborating agents is seamlessly enforced within the proposed control framework. A numerical simulation is provided to showcase the potential of our control framework.

We introduce a novel distributed sampled-data control method tailored for heterogeneous multi-agent systems under a global spatio-temporal task with acyclic dependencies. Specifically, we consider the global task as a conjunction of independent and collaborative tasks, defined over the absolute and relative states of agent pairs. Task dependencies in this form are then represented by a task graph, which we assume to be acyclic. From the given task graph, we provide an algorithmic approach to define a distributed sampled-data controller prioritizing the fulfilment of collaborative tasks as the primary objective, while fulfilling independent tasks unless they conflict with collaborative ones. Moreover, communication maintenance among collaborating agents is seamlessly enforced within the proposed control framework. A numerical simulation is provided to showcase the potential of our control framework.

In this work, we propose an extension of the previously introduced Corridor Model Predictive Control scheme for high-order and distributed systems, with an application for on-orbit inspection. To this end, we leverage high-order control barrier function (HOCBF) constraints as a suitable control approach to maintain each agent in the formation within a safe corridor from its reference trajectory. Recursive feasibility of the designed MPC scheme is tested numerically, while suitable modifications of the classical HOCBF constraints definition are introduced such that safety is guaranteed both in sampled and continuous time. The designed controller is validated through computer simulation in a realistic inspection scenario of the International Space Station.

In this work, we propose an extension of the pre-viously introduced Corridor Model Predictive Control scheme for high-order and distributed systems, with an application for on-orbit inspection. To this end, we leverage high order control barrier function (HOCBF) constraints as a suitable control approach to maintain each agent in the formation within a safe corridor from its reference trajectory. The recursive feasibility of the designed MPC scheme is tested numerically, while suitable modifications of the classical HOCBF constraint definition are introduced such that safety is guaranteed both in sampled and continuous time. The designed controller is validated through computer simulation in a realistic inspection scenario of the International Space Station.