A Formal Framework for Multi-Agent Task Planning

IEEE TRANSACTIONS ON AUTOMATIC CONTROL 1 A Formal Framework for Multi-Agent Task Planning Anatoli A. Tziola and Savvas G. Loizou, Member, IEEE Abstract— This paper presents a solution to the task planning problem for multi-agent systems. A formal framework is developed based on the Nondeterministic Finite Automata with ϵ-transitions, where given the capabilities, constraints and failure modes of the agents involved, an initial state of the system and a task specification, an optimal solution is generated that satisfies the system constraints and the task specification. The resulting solution is guaranteed to be complete and optimal; moreover, a heuristic solution that offers significant reduction of the computational requirements while relaxing the completeness and optimality requirements is proposed. The constructed system model is independent from the initial condition and the task specification, alleviating the need to repeat the costly preprocessing step for solving other scenarios, while allowing the incorporation of failure modes on-the-fly. An analysis of the completeness and optimality properties as well as the class of addressable problems is provided. Index Terms— Discrete event systems, heterogeneous systems, multi-agent systems, task planning. I. INTRODUCTION Multi-agent systems operating autonomously in dynamical environments to perform complicated tasks have been one of the major areas of research interest during the last decade. High-level task planning using formal methods to define the system requirements is one of the promising approaches. Typical objectives arise from the multi-agent systems’ behavior and requirements, such as sequential or reactive tasks, control, coordination and motion and task planning. The main motivation for this work comes from the field of manufacturing logistics automation and the need to automate intrafactory logistics operations. Real world problems that can benefit from automatic task planning appear in multiple sectors, including logistics and supply chain management (e.g. vehicle routing, inventory management, warehouse operations), manufacturing and production (e.g. production scheduling, supply chain planning, maintenance scheduling, recycling planning), healthcare (e.g. patient scheduling, disaster response, drug development), transportation (e.g. air traffic control, public transportation, autonomous vehicle navigation), etc. Manuscript submitted November 28, 2023. Portions of this work appeared in [1], [2]. A scaled down version of the software developed for this work has been made publicly available at [3]. This work was partially supported by EU programs under grant agreements 951813 (Better Factory, H2020) and 101092295 (CIRCULOOS, Horizon Europe). The authors are with the Mechanical Engineering and Materials Science and Engineering Department of Cyprus University of Technology, Limassol, CYPRUS (e-mails: {anatoli.tziola, savvas.loizou}@cut.ac.cy). This work introduces a new framework for high-level task planning problems with respect to agent capabilities, constraints and failure modes. The initial concepts for this work were presented in [1], whereas the current provides all the missing analysis (proofs, class of addressable problems, extended literature analysis). This work builds on top of the work on motion task planning in [4], where module composition was used to automatically synthesize motion controllers defined by LTL specifications. While the current work generalizes the concept of motion tasks to general tasks and develops the formal machinery for their automatic synthesis, leveraging the agents’ capabilities and constraints, it significantly departs from [4] by addressing a more general problem in a unified manner without the need to resort to the formalism of hybrid systems and LTL. The problem formulation uses the global system model as the environment model composed by individual agents’ capabilities and constraints, considering the individual agent’s failure modes to determine the optimal task plan. The problem is posed as a special case of Module Composition Problem (MCP) [5] and then reduced to a combinatorial optimization problem of shortest dipath, which can be solved in polynomial time. The optimal module chain under a supervisory control framework enables the use of the generated module chain as a model system for building supervisory controllers, as demonstrated in [4]. In the sequel, the module chain with the supervisory controllers can e.g. be combined with Navigation Function based controllers [6] with time abstracting properties (i.e. guarantees on the required time for a task - see e.g. [7]), to synthesize control laws with performance guarantees that ensure compositionality for accomplishing individual and global tasks. The developed methodology provides the capability for on-the-fly incorporation of failure modes, however the supervisory control and navigation framework for reactive activation of failure modes during execution, and on-the-fly plan reconfiguration, are beyond the scope of the current work. Several proposed methodologies address the high-level task planning problem using formal languages to express autonomous systems behavior and synthesize the supervisory control architecture to achieve the given specifications [8], [9]. Some of the most common approaches include Linear Temporal Logic (LTL), Capability Temporal Logic (CaTL) [10], Petri nets [11], sampling-based approaches [12], [13] and domain definition languages. Many of the existing works use LTL formulas to develop bottom-up [14]–[17] and distributed [18] approaches, where local LTL expressions are assigned This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. 2 IEEE TRANSACTIONS ON AUTOMATIC CONTROL to robots, or top-down approaches [12], [19]–[22], where a global task is decomposed into independent sub-tasks that are treated separately by each agent. A descriptive overview of the literature using formal methods to accomplish high-level specifications can be found in [23]. There are several works addressing the (heterogeneous) multi-robot task allocation problem using LTL [24]–[26]. These approaches do not directly address the issue of inclusion of failure modes or on-the-fly re-planning. Other works tackle the task planning problem of heterogeneous multi-robot systems using CaTL [10], [27], [28], providing failure handling capabilities and on-the-fly re-planning. However partial agent failures (i.e. failure modes where an agent retains some functionality) are not directly addressed. Petri nets are a widely used modeling formalism for Discrete Event Systems (DES) [11], [29]. In [13], a sampling-based approach is proposed using directed trees to approximate the state space and transitions of synchronous product automata, providing probabilistic completeness and asymptotic optimality guarantees. Common among the works presented in the literature survey is the adoption of formal verification techniques for motion planning and controller synthesis. Several gaps in the existing literature are been addressed by our approach: (Gap. 1) To the best of our knowledge, none of the existing methodologies provides an effective modeling and execution framework capturing a heterogeneous multi-agents’ system individual and collective capabilities, constraints and failure modes. Planning Domain Definition Language (PDDL) implementations have exponential complexity and are not particularly suited to applications requiring on-line re-planning or reconfiguration. (Gap. 2) In LTL-based planners, the solution domain depends on the task specification. Every time the specification is changed a new solution domain needs to be created, incurring increased computational overhead in the case of re-tasking e.g. in the case of failures, modified objectives1or initial conditions. (Gap. 3) Increasing the objectives in a task specification, increases the computational complexity, particularly in LTLbased planners where the worst-case computational complexity is double exponential with respect to the length of the formula. (Gap. 4) Sampling-based approaches relax the properties of optimality and completeness in finite time. Some, like in [13], provide asymptotic guarantees as the computational resources asymptotically expand to capture the full state space. Motivated by the identified gaps in the literature, this work provides the following contributions: 1) A new system modeling framework that combines the agents’ capabilities and constraints both at the individual and the group levels, including failure modes (Gap. 1). 2) Determination of optimal task plans that satisfy any possible task specification from any initial condition, without the need to repeat the pre-processing step (Gap. 4). 1Note that in the current work we make a distinction between task specification and objective in the sense that the objective denotes the final state of a single agent while the task specification may encapsulate any number of objectives. Compared with the terminology used in the LTL literature, the evolution of the system is not part of the task specification but is encoded in the system’s capabilities and constraints. 3) Capability of incorporation of multiple objectives in the task specification, decreasing the time complexity while maintaining the space complexity (Gap. 3). 4) Determination of reduced complexity sub-optimal solutions for any task specification, while maintaining its space complexity (Gap. 2). 5) Capability of incorporation of failure modes on-the-fly for re-planning, without the need to repeat the costly pre-processing step (Gap. 1, Gap. 2). In the rest of the paper section II presents the preliminaries, section III the problem formulation, section IV casts the problem as a Module Composition one, section V analyses the performance of the methodology and section VI concludes the paper. II. PRELIMINARIES A. Definitions In this section, we introduce the necessary terminology and definitions for the development of our methodology. If Aand Bare sets, the cardinality of set Ais denoted as |A|. The union and intersection of sets are denoted as A∪B and A∩Bwhereas set subtraction of set Bfrom set Ais denoted as A\B. We use the ∧operator to denote conjunction. We will use the Deterministic Finite Automata (DFA) represented as the tuple G≜(XG, EG, fG,ΓG, x0,G, Xm,G)(see [30] for detailed definition) and the cost function gG(e)that maps each event to a corresponding cost defined as gG:EG→ R>0. Unless otherwise stated, subscripts of an (DFA or NFA) automaton’s tuple elements will refer to the corresponding automaton as above. We need to introduce a new framework of ϵ0-NFAs that allows the use of ϵ0-transitions by enabling transitions on an empty event only from the initial state. The introduction of these automata became necessary to enable closure under the newly introduced operations in Section IIB. In practical terms, this allows us to consistently setup our system to handle any initial condition. Definition 1 (ϵ0-NFA): An ϵ0-NFA is a Nondeterministic Finite Automaton with ϵ-transitions only from the initial state, defined as a six-tuple ϵ0G≜(XG∪ {x0}, EG∪ {ϵ},ϵ0 fG,ΓG, x0, Xm,G), where ϵ0 fG:XG∪ {x0} × EG∪ {ϵ} → 2XGsuch that ∀(x, e)∈XG×EG:ϵ0 fG(x, e) := fG(x, e), where x0/∈XGis the initial state with x0=x0,G. Corollary 1: If ϵ0Gis an ϵ0-NFA then it can be converted to the DFA Gby removing x0along with the associated ϵ transitions and assigning an x0,G ∈XGas an initial state. Proof: This can be trivially shown by observing that the six-tuple obtained by the operation is as the one in the definition of DFA. Based on the Corollary 1, we can construct the operator: Definition 2 (ϵ0-NFA Determinization): Let ϵ0Gbe an ϵ0NFA and x0,G ∈XGa state in XGthat we want to assign as an initial state. Then, ∆(ϵ0G, x0,G)≜Gwhere Gis the DFA and the determinization operator ∆performs the conversion as described in Corollary 1. In this case, the determinization operator converts the ϵ0Gto the DFA Gby removing the “virtual” starting state x0and the ϵ event, and assigning an element of XGas the new starting state This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. TZIOLA AND LOIZOU: A FORMAL FRAMEWORK FOR MULTI-AGENT TASK PLANNING 3 x0,G of the constructed DFA G. Compared with the standard determinization in automata theory, the determinization operator in our case, results in a state space equivalent to the state space of ϵ0-NFA, while the accommodation of ϵtransitions in the resulting DFA is not required. We define the inverse transition function as follows: Definition 3 (Inverse Transition Function): Let Gbe a DFA. Define f−1 G:XG×EG→XGto be the inverse transition function such that fG(xG, e) = yG∧f−1 G(yG, e) = xGfor some xG:e∈ΓG(xG), yG:e∈ΓG(f−1 G(yG, e)). Note that an inverse transition function as in Definition 3 cannot always be defined for DFAs. For DFAs where such inverse transition function can be defined, we introduce the following concept: Definition 4 (Compatible ϵ0-NFAs): Let ϵ0Gand ϵ0 Bbe ϵ0NFAs. Let EC:= EG∩EB. Then, the automata ϵ0Gand ϵ0 Bare compatible iff ∀e∈EC, it holds that2,fG(xG, e) = fB(xB, e)for some xG:e∈ΓG(xG), xB:e∈ ΓB(xB)and f−1 G(yG, e) = f−1 B(yB, e)for some yG:e∈ ΓG(f−1 G(yG, e)), yB:e∈ΓB(f−1 B(yB, e)). In such case, it will also be true that xG=xBand yG=yB. We denote such a compatibility relation as ϵ0G≍ϵ0B. Note that the above definition effectively forces the endpoints of common events to be common states. B. Operations on compatible automata Here we introduce a custom set of the basic operations on compatible ϵ0-NFAs: union, subtraction and concatenation. The introduced operations differ from the ones found in the automata literature and provide the necessary functionality for the subsequent developments. Definition 5 (Union of Compatible Automata): For the ϵ0NFAs ϵ0Gand ϵ0 B, assume ϵ0G≍ϵ0 B. Define the compatible ϵ0-NFAs union ϵ0P≜ϵ0G∪≍ϵ0 Bto be the six-tuple ϵ0P≜ (XP∪ {x0}, EP∪ {ϵ},ϵ0 fP,ΓP, x0, Xm,P), where XP:= XG∪XB,EP:= EG∪EB,ΓP:XP→2EP,x0/∈XP and Xm,P:= Xm,G ∪Xm,B. The transition function ϵ0 fP: XP∪{x0}×EP∪{ϵ} → 2XPis such that ∀(x, e)∈XG×EG: ϵ0 fP(x, e) := fG(x, e)and ∀(x, e)∈XB×EB:ϵ0 fP(x, e) := fB(x, e). Compared with the standard union operation on automata presented in the literature, the union operation of Definition 5 produces the union instead of the cartesian product state space. Definition 6 (Subtraction of Compatible Automata): For the ϵ0-NFAs ϵ0Gand ϵ0 B, assume ϵ0G≍ϵ0 B. Define the compatible ϵ0-NFAs subtraction ϵ0Θ≜ϵ0G\≍ϵ0Bto be the six-tuple ϵ0Θ≜(XΘ∪ {x0}, EΘ∪ {ϵ},ϵ0 fΘ,ΓΘ, x0, Xm,Θ), where XΘ:= XG,EΘ:= EG\EB,ΓΘ:XΘ→2EΘ and x0/∈XΘ,Xm,Θ:= Xm,G \Xm,B. The transition function ϵ0 fΘ:XΘ∪ {x0} × EΘ∪ {ϵ} → 2XΘis such that ∀(x, e)∈XΘ×EΘ:ϵ0 fΘ(x, e) := fΘ(x, e). Note that the subtraction operation of Definition 6 is more in line with the set difference operator than with the intersection with the language complement used in regular languages. 2Note that due to Corollary 1 we have that ϵ0fG(xG, e)≡fG(xG, e)and ϵ0fB(xB, e)≡fB(xB, e). Definition 7 (Concatenation of Compatible Automata): For the ϵ0-NFAs ϵ0Gand ϵ0 B, assume ϵ0G≍ϵ0 B. Define the compatible ϵ0-NFAs concatenation ϵ0Φ≜ϵ0G⊥⊥≍ϵ0 B to be the six-tuple ϵ0Φ≜(XΦ∪ {x0}, EΦ∪ {ϵ},ϵ0 fΦ,ΓΦ, x0, Xm,Φ), where XΦ:= {uv|u∈XG, v ∈ XB},EΦ:= EG∪EB,ΓΦ:XΦ→2EΦ,x0/∈XΦ, and Xm,Φ:= {uv|u∈Xm,G ∧v∈Xm,B}. The transition function ϵ0 fΦ:XΦ∪ {x0} × EΦ∪ {ϵ} → 2XΦis such that ∀(x, e)∈XΦ×EΦ:ϵ0 fΦ(x, e) := fΦ(x, e). Note that the operation of concatenation in Definition 7 above, is similar to the well known parallel composition operation but differs in that the event sets undergo a disjoint union in our case to ensure that only one event can be activated at a time (no synchronization on common events needed). The concept of compatible automata, allows us to recover the properties for the operations of Definitions 5, 6 and 7: Corollary 2: The automata resulting from the operations defined in Definitions 5, 6 and 7 are ϵ0-NFAs. Proof: This is established by first noting that for the operations in Definitions 5, 6 and 7, the resulting automata are six-tuples as in Definition 1. Now we need to show that the resulting transition function fRis partial in its domain. Assume that Ris the resulting automaton from the operation (union, subtraction or concatenation). We have the cases: 1. Union operation: Due to the properties of Definition 4, it will hold that ∀x∈XR, then ∀e∈ΓG(x)∩ΓB(x)it will hold that fG(x, e) = fB(x, e). 2. Subtraction operation: Due to the properties of Definition 4, it will hold that ∀x∈XR, then ∀e∈ΓR(x)it will hold that fR(x, e) = fG(x, e). 3. Concatenation operation: Due to the properties of Definition 4, it holds that ∀(x:= uv)∈XR, where u∈XGand v∈XB, then ∀e∈ΓR(x)it holds that: either fR(x, e) = fG(u, e), with e∈EG, or fR(x, e) = fB(v, e), with e∈EB. As can be seen, in all three operations, ∀x∈XRand for each e∈ΓR(x), the state fR(x, e)is a unique state in XRand hence, the resulting transition function is partial in its domain. Thus, Rwill be an ϵ0-NFA since it fulfills the requirements of Definition 1. We need to introduce the following operator that addresses individual states of the concatenated states of Definition 7. Definition 8 (Projection Operator): Let x∈XΦbe a concatenated state of nelements, where xidenotes the i′th element of x,i∈ {1, . . . , n}. Define the projector bas an n-bit binary and biits i’th bit. The projection operator is defined as the ordered set proj(x, b)≜{xi|bi= 1}. We will need some definitions from MCP literature as well as some new ones for our development. Using the module definition by [5], we state the module in an appropriate form for our development. Definition 9 (Single Port Module): Let Gbe a DFA. Consider the finite set of ports P=Pin ∪Pout, where Pin be a non-empty finite set of input ports and Pout be a non-empty finite set of output ports with P⊆XGand Pin ∩Pout =∅. We define the single input/single output port (I/O) module T as a 3-tuple of T≜{p, e, q}, where p∈Pin is the input port, e∈EG:fG(p, e) = qand q∈Pout is the output port. This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. 4 IEEE TRANSACTIONS ON AUTOMATIC CONTROL The cost associated with module Tis defined as c(T)≜ gG(e). We can define the inverted module T−1where its input becomes its output and vice versa such that Definition 3 holds. III. PROBLEM FORMULATION A. Problem statement Given a set of agents, their capabilities and constraints as individuals, their emerging capabilities and constraints when operating in teams, their failure modes, and a task specification defining the final state of at least one agent, determine (if any) the optimal sequence of actions that brings the system from any initial state, to a state satisfying the task specification. B. Agent Model Agents are considered as entities, such as robots, machines, humans, items or anything that it could change its status to act on or react to its surroundings during a process or trigger event. An agent is modeled as an ϵ0-NFA (see Definition 1) composed by the agent’s capabilities and constraints. Agent’s capabilities represent the allowed state transitions derived from the combination of individual capabilities and failure mode modeled as ϵ0-NFAs. Agent’s constraints express the forbidden state transitions derived from the union of individual’s constraints modeled as ϵ0-NFAs. The agent model is produced by the subtraction of the agent’s constraints from the agent’s capabilities. The ith agent, i∈ {1, . . . , n}, is modeled by the ϵ0-NFA ϵ0 Ai, and let ϵ0 Adenote the set of nagents. 1) Individual Agent Capabilities:Let κbe the total number of individual capabilities of agent ϵ0 Aiand let the ϵ0-NFA ϵ0 Mβ,i denote its β’th individual capability, where β∈ {1, . . . , κ}. 2) Individual Agent Failure Mode:Consider a state x′∈ XMβ,i . We define a failure mode of ϵ0 Aias the inability to complete the transition from some x∈XMβ,i to x′with an occurrence of event e∈EMβ,i . This describes a detected transition failure of ϵ0 Aiwhich renders fMβ,i (x, e) = x′ infeasible. This failure mode is modeled by the ϵ0-NFA ϵ0 Fi such that XFi={x, x′}and EFi={e}. We model the agent’s capabilities as the subtraction of the agent failure from the union of individual agent capabilities utilizing the union and the subtraction of compatible automata. 3) Agent Capabilities:Considering κcompatible ϵ0-NFAs such that ϵ0 Mα,i ≍ϵ0 Mβ,i,α=βwith α, β ∈ {1, . . . , κ} and ϵ0 Fi≍ϵ0 Mβ,i, the capabilities of ϵ0 Aiare modeled by the ϵ0-NFA ϵ0 Kias: ϵ0 Ki≜{κ ∪≍ β=1 ϵ0 Mβ,i}\≍ϵ0 Fi.(1) 4) Individual Agent Constraints:Let λbe the total number of individual constraints of agent ϵ0 Aiand let the ϵ0-NFA ϵ0 Nξ,i denote its ξ’th individual constraint, where ξ∈ {1, . . . , λ}. We model agent’s constraints as the union of individual agent constraints utilizing the union of compatible automata. 5) Agent Constraints:Considering λcompatible ϵ0-NFAs such that ϵ0 Nξ,i ≍ϵ0 Nη,i,ξ=ηwith η∈ {1, . . . , λ}, the constraints of ϵ0 Aiare modeled by the ϵ0-NFA ϵ0 Dias: ϵ0 Di≜{λ ∪≍ ξ=1 ϵ0 Nξ,i}.(2) Kn K2 K1Dn D2 D1 M  ,1 M M M M  ,2 M M M M  ,n M M M N  ,1 M M M N  ,2 M M M  ,n A1A2An . . . . . . . . . K1D1K2D2KnDn F1 M  ,1 F1M  ,2 F2M  ,n Fn F2Fn . . . . . . K1 K2 ... Kn D1 D2 ... Dn Union Subtraction Individual Capabilities Individual Constraints Individual Failure Mode Agent's Capabilities Agent's Constraints Agent's Model Environmental Capabilities Environmental Constraints Inter-Agent Constraints Inter-Agent Capabilities Concatenation Global Capabilities Global Constraints Environment Model Fig. 1. Flow diagram of the operations to produce models of agents ϵ0Aiand environment ϵ0S. Considering ϵ0 Ki≍ϵ0 Di, the ith agent is modeled by the ϵ0-NFA ϵ0 Aiafter subtracting ϵ0 Difrom ϵ0 Ki: ϵ0 Ai≜ϵ0 Ki\≍ϵ0 Di.(3) C. Environment Model Agents are acting in the environment to reach individual states while being influenced by state capabilities and constraints relating to other agents. Agents who rely on other agents to perform actions or reach goals are grouped into a team. The capabilities and constraints of the team are modeled as a combination of individual states of the members of the team. These capabilities and constraints are defined as interagent capabilities and constraints and express the allowed and not-permitted environment state transitions that emerge when the agents of team are present. Given the agents’ capabilities and constraints and the inter-agent capabilities and constraints as ϵ0-NFAs, the environment model expressed as an ϵ0-NFA captures the full behavior of the system using all the possible combinations of agents’ states. The procedure of constructing agents’ and environment models is illustrated in Fig. 1. We model the environmental capabilities as the concatenation of agents’ capabilities ϵ0-NFAs, formed as in (1), utilizing the concatenation operation of compatible automata to express the allowed environment state transitions. 1) Environmental Capabilities:For the ϵ0-NFAs ϵ0 Kiand ϵ0 Kj,i=jwith i, j ∈ {1, . . . , n}, let ϵ0 Ki≍ϵ0 Kj. The environmental capabilities are modeled by the ϵ0-NFA ϵ0 Kas: ϵ0 K≜n ⊥⊥≍ i=1 ϵ0 Ki.(4) We model the environmental constraints as the concatenation of agents’ constraints ϵ0-NFAs, formed as in (2), utilizing the concatenation operation of compatible automata to express the not-permitted environment state transitions. This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. TZIOLA AND LOIZOU: A FORMAL FRAMEWORK FOR MULTI-AGENT TASK PLANNING 5 2) Environmental Constraints:For the ϵ0-NFAs ϵ0 Diand ϵ0 Dj,i=jwith i, j ∈ {1, . . . , n}, let ϵ0 Di≍ϵ0 Dj. The environmental constraints are modeled by the ϵ0-NFA ϵ0Das: ϵ0D≜n ⊥⊥≍ i=1 ϵ0 Di.(5) Using the agents’ models formed as in (3), the inter-agents capabilities ϵ0-NFA and inter-agents constraints ϵ0-NFA are modeled as follows: 3) Inter-Agents Capabilities:Let co ⊆ϵ0 Awith |co| ≤ n be a set of compatible agent ϵ0-NFAs. Then, the ϵ0-NFA ϵ0 KA⊂ ⊥⊥≍i∈co ϵ0 Aidenotes the inter-agents capabilities3 between the members of co. 4) Inter-Agents Constraints:Let co ⊆ϵ0 Awith |co| ≤ n be a set of compatible agent ϵ0-NFAs. Then, the ϵ0-NFA ϵ0DA⊂ ⊥⊥≍i∈co ϵ0 Aidenotes the inter-agents constraints between the members of co. We model the global capabilities as the ϵ0-NFA derived from the union of environmental capabilities (formed as in (4)) with inter-agent capabilities. 5) Global Capabilities:For the ϵ0-NFAs ϵ0 Kand ϵ0KA, let ϵ0 K ≍ ϵ0KA. The global capabilities are modeled by the ϵ0NFA ϵ0e Kdefined as ϵ0e K≜ϵ0 K ∪≍ϵ0KA. We model the global constraints as the ϵ0-NFA derived from the union of environmental constraints (formed as in (5)) with inter-agent constraints. 6) Global Constraints:For the ϵ0-NFAs ϵ0Dand ϵ0 DA, let ϵ0D ≍ ϵ0 DA. The global constraints are modeled by the ϵ0NFA ϵ0e Ddefined as ϵ0e D≜ϵ0D ∪≍ϵ0 DA. Considering ϵ0e K ≍ ϵ0e D, the environment model is modeled by the ϵ0-NFA ϵ0 Safter subtracting ϵ0e Dfrom ϵ0e K: ϵ0 S≜ϵ0e K\≍ϵ0e D,(6) where the cardinality of XSis θ= n Q i=1 |XAi|. D. Task Specification Let bbe an n-bit binary indicating the states of the agents that we are interested in specifying. We define the task specification γas the tuple γ≜(φ, b). Let xd∈XS. Then, xdsatisfies the task specification γ, if proj(xd, b) := φ. Depending on the cardinality of φ(i.e. how many bits are active in b), single or multiple tasks (objectives) can be concurrently specified in γ. IV. FORMULATION AS A MODULE COMPOSITION PROBLEM Let us now consider the environment model ϵ0Sand assume that we would like to use x0,S∈XSas the initial state of our system. Thus, S= ∆(ϵ0S, x0,S)is the DFA description of the environment model. Let Pin ∈XSdenote the nonempty finite set of input ports and Pout ∈XSdenote the nonempty finite set of output ports, where P=Pin ∪Pout and Pin ∩Pout =∅. The module Tjis defined as Tj≜{pj, ej, qj}, 3Inter-Agents Failure Modes can be defined so as to restrict Inter-Agents Capabilities where pj∈Pin,ej∈ES,qj∈Pout and c(Tj)≜gES(ej)is the cost of implementing module Tj. Define the ith task module as T0,i ={x0,S, e0,i, xd,i}where proj(xd,i, b) := φ, xd,i ∈XSand e0,i a virtual transition from the initial to the final state. Observe that there are up to |φ|!potential solutions so i∈ {1,...,|φ|!}. To tackle the problem defined in the Problem Statement, we proceed to formulate our problem as a Module Composition Problem [5]. Since we are using single-port modules, we will have a special case of the MCP that is solvable in polynomial time. We define Tias the finite open module chain describing the task plan for a given task specification γdefined as Ti={T1,i, . . . , Tz,i}, where zi=|Ti|. We define ◦ Tias the finite closed module chain, containing T−1 0,i and task plan Ti, describing the sequential environment states transitions during the execution defined as ◦ Ti={T−1 0,i ,Ti}. In the sequel we will drop the index ifor notational brevity. Let tjdenote the number of instances of Tj,cj=c(Tj), then the discrete optimization problem can be posed as an integer programming problem as follows: min X j∈{1,...|ES|} cjtj,(7) subject to: t0= 1, tj∈Z+, σp=X q∈Pout wp,q,∀p∈Pin, µq=X p∈Pin wp,q,∀q∈Pout, where Z+denotes the non-negative integers, wp,q the number of connections between input port pand output port q,σp the number of modules with input port putilized and µqthe number of modules with output port qutilized. Since in the current work we have implemented only single port modules, the above integer programming problem can be reduced to the shortest directed path problem [5], that can be solved utilizing the Dijkstra’s shortest dipath algorithm. The optimal solution composes the Tthat minimizes the cost of states transitions in order to satisfy the task specification γ. The drawback of using singe port modules in the current work is that we are only limiting transitions to be performed by one agent at a time. Multi-port modules are currently being considered as a further research topic, to enable multiple agents to perform concurrent transitions and is beyond the scope of the current work. We have to also note here that the additional effort in casting the problem as a module composition one, enables us to seamlessly use the generated module chain as a model system for building supervisory controllers as in [4], and is currently under active research. V. ANALYSIS A. Pre-processing Analysis The pre-processing step includes the construction of the agents models and the environment model (see Fig.1) using This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. 6 IEEE TRANSACTIONS ON AUTOMATIC CONTROL the automata operations as described in sections III-B and IIIC. A polynomial amount of time on the number of agent states is required to construct the models of all agents and the environment model. More specifically, the model of agent ϵ0 Aiis derived from the subtraction of agent’s constraints from agent’s capabilities. Both operations, the union and the subtraction, require a total of O(|XAi|2)time to be performed. Thus, the complexity of the agent model construction is O(|XAi|2). On the other hand, the concatenation operation requires O(|XS|)time, where |XS|=Qn i=1 |XAi|, while both the union and subtraction operations require O(|XS|2). Hence, the time complexity for the construction of the environment model is O(|XS|2)in total. It is important to note here that the environment model ϵ0S is only needed to be constructed once and can be use thereafter for all possible task specifications and initial states. ϵ0Sis converted to a weighted directed graph HS= (VS,ES), where the set of nodes VScorresponds to the set of states XS, the set of edges ESis defined by fSassociated with its cost gS. HSis related to the directed graph produced by the module composition procedure, since by the definition of module Tj, edges in ESserve as vertices of the module composition graph. In addition, due to the compatibility relation requirements, the vertices of each edge in ESare unique, hence the directed graph produced by the module composition procedure is the Line graph L(HS)of HS. Any directed path, in HSwith its associated cost, has an equivalent path of the same cost and the same event sequence in L(HS). To see this consider that a path v1e1v2e2. . . vnenvn+1 in HSwill necessarily correspond to the path e1(q1p2)e2. . . (qn−1pn)enin L(HS) where (qipi+1)are the edges in L(HS)corresponding to the connection between output port qiand input port pi+1. Hence, solving a shortest directed path problem on HSis equivalent to solving the module composition problem. Regarding complexity, the adjacency matrix representation of HSis a 2-dimensional array XS×XS. Each element in the array stores the cost gSrelated to the edge fS(x∈ XS, e ∈ES). The amount of space required to store the array is O(|VS|2)in worst case. B. Analysis of the Complete Solution The problem solving phase encapsulates the synthesis of the optimal task plan and the integration of individual agent failure mode. The Dijkstra’s algorithm is implemented over the weighted graph HS(Algorithm 1, lines 8-15) to find the optimal task plan Tas given in Algorithm 1 in lines 21-23. In the case where a fault is detected for the transition from state xito xjof S(e.g. by some fault identification system) that affects agent ν, we can disable all the affected transitions by finding the set of states Xi′,Xj′, where proj(xi, bν)≡ proj(xi′∈Xi′, bν)and proj(xj, bν)≡proj(xj′∈Xj′, bν). Then, we eliminate the transitions from all xi′∈Xi′to all xj′∈Xj′. New failure modes can be incorporated on-the-fly into ϵ0Swithout the need to repeat the costly pre-processing step. The computational time required for this modification is θf=Qn i=1, i=ν|XAi|in the worst case. The task planning problem of minimizing the length of the plan is NP-complete. Let Pbe the solution to this problem found after running Dijkstra’s algorithm and let Pidenote it’s i’th element, i∈ {1,...,|P|} (Algorithm 1, lines 16-20). In Algorithm 2, the optimal solution can then be found by running the algorithm for all states that satisfy the task specification (Algorithm 2, lines 3-16), that is θ′=Qn i=1, i/∈σ|XAi| times in the worst case scenario, where σdenotes the set of agents that were used for the task specification γ. The running time for implementing Algorithm 1 with the “Complete” solution type (line 16-17), is O(θ′|ES|log(|VS|)), considering the complexity of Dijkstra’s algorithm. Considering that |ES|<|XS||ES|, that the event set is linear on the event sets of the individual agents, and that θ′<|XS|, the worst case computational complexity of Algorithm 1 is bounded above by O(|ES||XS|2log(|XS|)). Algorithm 1 Create module chain T. Require: ϵ0-NFA ϵ0S, initial state x0,S, task specification γ, solution type ST (“Complete” or “Heuristic”) Ensure: Module chain T 1: Initialize Ha zero matrix, Ean empty cell array, Tan empty set 2: S ←− ∆(ϵ0S, x0,S) 3: if proj(x0,S, b) := φ∧x0,S∈Xm,Sthen 4: return T 5: else 6: for i∈ {1,...,|XS|} do 7: for j∈ {1,...,|XS|} do 8: if ∃e∈ES:fS(xi, e) = xjthen 9: H[i][j]←− gS(e) 10: E{i}{j} ←− e 11: end if 12: end for 13: end for 14: if ST =“Complete” then 15: [P, cost] ←− COMPLETE(H,S,x0,S,γ) 16: else 17: [P, cost] ←− HEURISTIC(H,S, E, x0,S,γ) 18: end if 19: for i∈ {1,...,|P| − 1}do 20: T ←− T ∪ Pi, E{Pi}{Pi+1},Pi+1 21: end for 22: return T, cost 23: end if Algorithm 2 Complete Function. 1: function COMPLETE(H,S,x0,S,γ) 2: Initialize costmin ←− ∞ 3: for i∈ {1,...,|XS|} do 4: for j∈ {1,...,|XS|} do 5: if proj(xj, b) := φ∧xj∈Xm,Sthen 6: [P, cost] ←− Dijkstra(H, x0,S, xj) 7: if P=∅then 8: return Task infeasible. 9: end if 10: if cost < costmin then 11: costmin ←− cost 12: Poptimal ←− P 13: end if 14: end if 15: end for 16: end for 17: return Poptimal,costmin 18: end function C. Analysis of a Heuristic Solution In addition to the complete algorithm presented above, a heuristic approach is proposed in Algorithm 3 to reduce the computational time required to find a solution. By implementing Algorithm 1 with the proposed “Heuristic” solution type (line 19), reduces the complexity by only requiring a single This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. TZIOLA AND LOIZOU: A FORMAL FRAMEWORK FOR MULTI-AGENT TASK PLANNING 7 execution of Dijkstra’s algorithm, while sacrificing optimality and completeness. The computational time requirements of the proposed heuristic is O(|ES|log(|VS|)). Following similar arguments as in the complete solution, the worst case computational complexity of Algorithm 1 is bounded above by O(|ES||XS|log(|XS|)). The intuition for utilizing the “Heuristic” solution type (Algorithm 3), is to avoid having the agents that are not participating in the task specification to end up in configurations different from their initial ones. Hence, we set the goal state xdto be such that proj(xd, b) := φand proj(xd,b) = proj(x0,S, b) (Algorithm 3, line 3), where bdenotes the bitwise negation. To discard unnecessary transitions and reduce the cost (recovering partial optimality), we track the solution to the minimum element kwhere proj(Pk, b) := φand use the solution Ph={P1,...,Pk}(Algorithm 3, line 9-15). While not possessing the completeness property, there are some cases where the proposed heuristic fully recovers optimality. One such case is when bis only composed of ones, i.e. the full state vector of the goal state is specified. However, a classification of those cases and the conditions for feasibility of solutions is currently under consideration but is not part of the current work. Algorithm 3 Heuristic Function. 1: function HEURISTIC(H,S, E, x0,S,γ) 2: Initialize xdto an empty set 3: Find xd∈Xm,S:proj(xd, b) := φ∧proj(xd,b) = proj(x0,S, b) 4: Initialize ch←− 0 5: [P, cost] ←− Dijkstra(H, x0,S, xd) 6: if P=∅then 7: return No path to xd. 8: end if 9: for k∈ {2,...,|P|} do 10: ch←− ch+gS(E{Pk−1}{Pk}) 11: if proj(Pk, b) := φthen 12: Ph←− {P1,...,Pk} 13: return Ph, ch 14: end if 15: end for 16: end function D. Completeness and Optimality The principle of completeness asserts that the algorithm always returns a solution (if one exists), otherwise if there is no solution, the algorithm reports failure. We have the following results regarding the completeness of Algorithms 1, 2: Proposition 1: For a system constructed based on individual and inter-agent capabilities, constraints and failure modes of the multi-agent system as presented in Section III, the resulting environment model of (6) is complete, in the sense that it represents all and only those state transitions that are dictated by the automata capturing the individual and interagent capabilities, constraints and failure modes. Proof: To demonstrate the above claim we need to show that during the composition of ϵ0 S, no valid transitions or states are being removed from the system and no new states or transitions are being introduced. In particular: 1. No states removed or added: This can be shown by observing that from Corollary 2 the ϵ0-NFAs is closed under the operations of union, subtraction and concatenation. Union operation (Definition 5): This operates only on states defined in its arguments and the resulting states are the union of the argument’s states that are part of agents’ capabilities and constraints. Subtraction operation (Definition 6): This operation does not remove any states from the subtrahend argument. Concatenation operation (Definition 7): This operation creates the cross product state space of its argument. None of the operations introduces any state that does not already exist in their arguments. 2. No valid events are removed and no new transitions are introduced. Union and Concatenation operations: The resulting event set is the union of the operator argument events. No new events are introduced, that do not already exist in the arguments. Subtraction operation: The resulting event set includes only the events that are in the subtrahend and not in the subtractor’s event set without introducing any new event. In particular failure mode events are removed from individual agent’s capabilities with subtraction operation without affecting any other events. The event set of global constraints is removed from the global capabilities without affecting events that are not included in the global capabilities event set. Any event that is in the individual or inter-agent capabilities and is not in the failure modes, individual constraints or interagent constraints event sets will be included in the environment model. Any event that is in the failure modes event set (but not in the inter-agent capabilities) as well as any event in the individual or inter-agent constraint event set, will not appear in the environment model event set. Events that are not included in the individual and inter-agent capabilities will not appear in the environment model event set. Hence all and only transitions that are valid will appear in the environment model’s event set. With the completeness property in place we can state the result about the optimality properties of the proposed system: Proposition 2: For a system constructed based on individual and inter-agent capabilities, constraints and failure modes of the multi-agent system as presented in Section III, and assuming that only one agent is allowed to operate at any time instant, the solution of Algorithm 1 with the “Complete” solution type of Algorithm 2, produces the optimal sequence of actions that brings the system from any initial state to a state that satisfies the task specification γwhile minimizing the cost of the task plan T. Proof: Since according to Proposition 1 the environment model is complete, then all (if any) optimal solutions are encoded in the transition system imposed by the transition function of the environment model. The module composition problem is an integer optimization problem and in our case maps the task planning problem to the shortest directed path - a graph search problem. The implemented Dijkstra’s solution is both complete and is guaranteed to find an optimal solution if such a solution exists. E. Class of Addressable Problems To assess the expressiveness of the proposed framework we have the following result: Corollary 3: If Gis a DFA then it can be converted to the ϵ0-NFA ϵ0Gby introducing the state x0as the initial state of This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply. 8 IEEE TRANSACTIONS ON AUTOMATIC CONTROL ϵ0Galong with the associated ϵtransition to the starting state x0,G of G. Proof: This can be shown by observing that the six-tuple obtained by the operation is as the one in Definition 1. Based on Corollary 3, any DFA can be converted to ϵ0-NFA. Furthermore, gGthat is associated to EGrenders the ϵ0-NFAs to weighted automata. Hence, the proposed framework inherits the expressiveness of weighted automata. Remark 1: The LTL-based and weighted automata-based frameworks are complementary [31] since even though they have an intersection, each one addresses problems that the other cannot address. VI. CONCLUSIONS A framework and a methodology for a novel multi-agent task planner is proposed. Given the capabilities, constraints and failure modes of the agents under the framework of NFAs with ϵ-transitions, the proposed framework produces optimal solutions, providing the sequence of tasks for transporting the state of the environment from any initial to a destination state satisfying the task specification. The developed algorithms can provide a complete solution with optimality guarantees whenever a solution exists. By relaxing the completeness property requirement, a significant reduction in the computational requirements is achieved, that provides sub-optimal solutions through the use of efficient heuristics. Future research will focus on combining the proposed framework with supervisory control theory to enable reactive execution in dynamic environments, incorporating liveness properties, automatic system reconfiguration in the case of failures, enabling concurrent execution of modules, e.g. in a multi-port module setting, distributing task synthesis and improving the average computational complexity of both the pre-processing and planning phases. REFERENCES [1] A. A. Tziola and S. G. Loizou, “Autonomous task planning for heterogeneous multi-agent systems,” 2023 IEEE International Conference on Robotics and Automation (ICRA), pp. 3490–3496, 2023. [2] ——, “Autonomous task planning for heterogeneous multi-agent systems,” arXiv Preprint arXiv:2209.08611, 2022. [3] “Business process optimization (BPO) module,” https://github.com/ rcdslabcut/mod.sw.bpo, accessed: November 2023. [4] S. G. Loizou and K. J. Kyriakopoulos, “Automated planning of motion tasks for multi-robot systems,” in IEEE International Conference on Decision and Control, 2005, pp. 78–83. [5] S. Tripakis, “Automated module composition,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2003, pp. 347–362. [6] S. G. Loizou and E. D. Rimon, “Mobile robot navigation functions tuned by sensor readings in partially known environments,” IEEE Robotics and Automation Letters, vol. 7, no. 2, pp. 3803–3810, 2022. [7] S. G. Loizou, “The navigation transformation,” IEEE Transactions on Robotics, vol. 33, no. 6, pp. 1516–1523, 2017. [8] R. C. Hill and S. Lafortune, “Scaling formal synthesis of supervisory control for multiple robot systems,” in IEEE ACC, 2017, pp. 3840–3847. [9] J. Goryca and R. C. Hill, “Formal synthesis of supervisory control software for multiple robot systems,” in IEEE ACC, 2013, pp. 125–131. [10] G. A. Cardona and C.-I. Vasile, “Planning for heterogeneous teams of robots with temporal logic, capability, and resource constraints,” Int. Journal of Robotics Research, vol. 43, no. 13, pp. 2089–2111, 2024. [11] S. Hustiu, C. Mahulea, M. Kloetzer, and J.-J. Lesage, “On multi-robot path planning based on Petri net models and LTL specifications,” IEEE Transactions on Automatic Control, pp. 1–8, 2024. [12] Y. Kantaros and M. M. Zavlanos, “Sampling-based optimal control synthesis for multirobot systems under global temporal tasks,” IEEE Transactions on Automatic Control, vol. 64, no. 5, pp. 1916–1931, 2018. [13] ——, “STyLuS*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,” The International Journal of Robotics Research, pp. 812–836, 39(7), 2020. [14] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Where’s waldo? sensor-based temporal logic motion planning,” in IEEE International Conference on Robotics and Automation, 2007, pp. 3116–3121. [15] ——, “Temporal-logic-based reactive mission and motion planning,” IEEE Transactions on Robotics, vol. 25, no. 6, pp. 1370–1381, 2009. [16] M. Guo and D. V. Dimarogonas, “Task and motion coordination for heterogeneous multiagent systems with loosely coupled local tasks,” IEEE Trans. on Automation Science and Eng., vol. 14(2), 797–808, 2016. [17] S. L. Smith, J. T˘ umov´ a, C. Belta, and D. Rus, “Optimal path planning for surveillance with temporal-logic constraints,” The International Journal of Robotics Research, vol. 30, no. 14, pp. 1695–1708, 2011. [18] N. Xu, T. Peng, D. Liu, and J. Li, “Temporal logic control synthesis for distributed multi-agent cooperative tasking,” Journal of Physics: Conference Series, vol. 2216, no. 1, p. 012061, 2022. [19] Y. Chen, X. C. Ding, A. Stefanescu, and C. Belta, “A formal approach to deployment of robotic teams in urban-like environment,” in Distributed Autonomous Robotic Systems. Springer, 2013, pp. 313–327. [20] M. Karimadini and H. Lin, “Guaranteed global performance through local coordinations,” Automatica, vol. 47, no. 5, pp. 890–898, 2011. [21] J. Tumova and D. V. Dimarogonas, “Multi-agent planning under local LTL specifications and event-based synchronization,” Automatica, vol. 70, pp. 239–248, 2016. [22] P. Schillinger, M. B¨ urger, and D. V. Dimarogonas, “Decomposition of finite ltl specifications for efficient multi-agent planning,” in Distributed Autonomous Robotic Systems. Springer, 2018, pp. 253–267. [23] H. Lin, “Mission accomplished: An introduction to formal methods in mobile robot motion planning and control,” Unmanned Systems, vol. 2, no. 02, pp. 201–216, 2014. [24] P. Schillinger, M. B¨ urger, and D. V. Dimarogonas, “Simultaneous task allocation and planning for temporal logic goals in heterogeneous multirobot systems,” The Int. J. of Robotics Res., vol. 37(7), 818–838, 2018. [25] M. Kloetzer and C. Mahulea, “Multi-robot path planning for syntactically co-safe LTL specifications,” in 13th International Workshop on Discrete Event Systems (WODES). IEEE, 2016, pp. 452–458. [26] X. Luo and M. M. Zavlanos, “Temporal logic task allocation in heterogeneous multirobot systems,” IEEE Transactions on Robotics, vol. 38, no. 6, pp. 3602–3621, 2022. [27] K. Leahy, Z. Serlin, C.-I. Vasile, A. Schoer, A. M. Jones, R. Tron, and C. Belta, “Scalable and robust algorithms for task-based coordination from high-level specifications (ScRATCHeS),” IEEE Transactions on Robotics, vol. 38, no. 4, pp. 2516–2535, 2021. [28] Z. Chen and Z. Kan, “Real-time reactive task allocation and planning of large heterogeneous multi-robot systems with temporal logic specifications,” The International Journal of Robotics Research, 2024. [29] S. Lafortune, “Discrete event systems: Modeling, observation, and control,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 141–159, 2019. [30] C. G. Cassandras and S. Lafortune, Introduction to discrete event systems. Springer Science & Business Media, 2009. [31] M. Lahijanian, S. B. Andersson, and C. Belta, “Formal verification and synthesis for discrete-time stochastic systems,” IEEE Transactions on Automatic Control, vol. 60, no. 8, pp. 2031–2045, 2015. This article has been accepted for publication in IEEE Transactions on Automatic Control. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/TAC.2025.3601769 © 2025 IEEE. All rights reserved, including rights for text and data mining and training of artificial intelligence and similar technologies. Personal use is permitted, but republication/redistribution requires IEEE permission. See https://www.ieee.org/publications/rights/index.html for more information. Authorized licensed use limited to: Cyprus University of Technology. Downloaded on October 16,2025 at 06:59:26 UTC from IEEE Xplore. Restrictions apply.