# Multi-Satellite Task Parallelism via Priority-Aware Decomposition and Dynamic Resource Mapping
## 4 Methodology
### Dynamic Scheduling and Task Dependency Constraint Handling Based on Temporal Logic  
In the multi-satellite cooperative computing system, the dynamic nature of task execution and the complexity of task dependencies necessitate a robust scheduling mechanism. In the dynamic scheduling process, it is essential to consider not only the task dependencies but also how these dependencies evolve in real time as the system state changes. By using Linear Temporal Logic (LTL), we can express the timing and sequence constraints that govern the relationships between tasks. This formal framework ensures that the execution order of tasks adheres to the precedence relationships dictated by their dependencies. Furthermore, the dynamic nature of task execution requires continuous adjustments based on the current system state and task progress. As the system evolves, the scheduling process needs to re-evaluate task dependencies and resource availability to maintain optimal execution. This is achieved by using MINLP, which provides a flexible and adaptive framework for real-time scheduling. This section proposes a dynamic scheduling strategy using temporal logic and MINLP to handle the constraints imposed by task dependencies. Temporal logic provides a formal framework to model the sequential relationships between tasks. To accurately represent the task dependencies in a multi-satellite environment, we use LTL to express the sequence and timing constraints among tasks. Each task \(T_{ij}\) is associated with an LTL formula that defines its start and end conditions based on other dependent tasks:  
\[\mathbf{G}(\mathbf{F}\;T_{ik}\rightarrow\mathbf{F}\;T_{ij}), \tag{31}\]  
where \(\mathbf{G}\) denotes the \"globally\" operator, ensuring that the task relationship holds at all times, and \(\mathbf{F}\) represents the \"eventually\" operator, indicating that \(T_{ij}\) can only start after the completion of \(T_{ik}\). This formalism allows the encoding of complex task dependencies and timing constraints into the scheduling model. We define the decision variables \(x_{ij}(t)\) as binary variables indicating whether task \(T_{ij}\) is executed at time \(t\):  
\[x_{ij}(t)= \begin{cases}1,&\text{if $T_{ij}$ is executed at time $t$},\\ 0,&\text{otherwise}\end{cases}  \tag{32}\]  
The objective function aims to minimize the total execution time while satisfying the LTL constraints. The formulation includes constraints for task dependencies, resource limitations, and time windows. For example, the dependency constraint between tasks \(T_{ij}\) and \(T_{ik}\) can be formulated as  
\[\sum_{t=1}^{T}t\cdot x_{ij}(t)\geq\sum_{t=1}^{T}t\cdot x_{ik}(t)+\tau_{ik}, \tag{33}\]  
where \(\tau_{ik}\) represents the minimum time delay required between the completion of task \(T_{ik}\) and the start of task \(T_{ij}\). Theorem 3.1: _Given a set of task dependencies modeled by LTL formulas and the available resources of the multi-satellite system, the dynamic scheduling problem has a feasible solution if the MINLP formulation satisfies all temporal logic constraints and resource limitations._  
Proof: We first encode each LTL dependency of the form  
\[\varphi_{ik\to ij}=G(F\,T_{ik}\to F\,T_{ij}).\]  
By discretizing time into slots \(t=1,\ldots,T\). We define the binary decision variables as follows:  
\[x_{ij}(t)\in\{0,1\},\quad\forall T_{ij},\;t=1,\ldots,T,\]  
Let the start time of task \(T_{ij}\) be given by  
\[t_{ij}=\sum_{t=1}^{T}t\,x_{ij}(t). \tag{34}\]  
For every dependency pair \((T_{ik},T_{ij})\) with a required minimum delay \(\tau_{ik}\), introduce an auxiliary binary variable \(z_{ijk}\in\{0,1\}\) and enforce the constraints  
\[t_{ij}\geq t_{ik}+\tau_{ik}-M\,(1-z_{ijk}), \tag{35}\]  
\[\sum_{t=1}^{T}x_{ik}(t)\leq T\,z_{ijk},\quad\sum_{t=1}^{T}x_{ik}(t)\geq z_{ijk}, \tag{36}\]  
where \(M\) is a sufficiently large constant ensuring that when \(z_{ijk}=0\), the constraint (35) is inactive.