## 3 Backward Reachability-Based Schedulability Test
### Algorithms for Schedulability and Infeasibility Tests  
Summarizing Lemmas 1 and 2, we formulate a general criterion for checking the safety (schedulability) and unsafety (infeasibility) for real-time systems with \(n\) tasks executed on \(n-1\) processors:  
**Theorem 1**.: _The real-time system \(T\) with \(n\) tasks executed on \(n-1\) processors is unsafe (infeasible) if there exists task \(i\), such that_  
* \(\forall j\
eq i\ (D_{i}<C_{j})\)_, or_
* \(\exists j<i\ (C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}>D_{j}-C_{j})\)_._  
Algorithm 1 is based on this theorem. It returns \"NO\" if an input real-time system is unsafe (infeasible) and \"YES\" if this system is schedulable. Obviously, the time complexity of this algorithm is \(\mathcal{O}(n^{2})\), which makes our schedulability test using this algorithm faster than any state-of-the-art exact schedulability test for a real-time system with the non-preemptive global fixed-priority scheduler running on a multiprocessor platform.  
```
0: real-time system \(T\) with \(n\) tasks and \(n-1\) processors.
0: YES/NO
1:for\(i=1\) to \(n\)do
2:if\(\forall j\
eq i\ (D_{i}<C_{j})\)then return NO
3:endif
4:if\(\exists j<i\ (C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}>D_{j}-C_{j})\)then return NO
5:endif
6:endfor
7:return YES
```  
**Algorithm 1** The base algorithm for the exact schedulability test  
It is easy to see that if we add several tasks to the system \(T\), the above unsafety criteria remain the same but the safety criteria (pictures with bright green lines) do not work in the new settings, since they are based on the absence of tasks for the full load of processors, and in the presence of additional tasks, this assumption is violated. In this case, Algorithm 1 can be redefined as Algorithm 2 in order to perform a pessimistic sufficient infeasibility test for a real-time system. Algorithm 2 returns \"NO\" if an input real-time system is unsafe (infeasible) and \"UNKNOWN\" if the unsafety criterion is false. It recognizes real-time systems that are unschedulable even if the number of processors is just one less than the number of tasks.  
```
0: real-time system \(T\) with \(n\) tasks and \(m\) processors (\(m<n-1\)).
0: NO/UNKNOWN
1:for\(i=1\) to \(n\)do
2:if\(\forall j\
eq i\) (\(D_{i}<C_{j}\)) then return NO
3:endif
4:if\(\exists j<i\) (\(C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}>D_{j}-C_{j}\)) then return NO
5:endif
6:endfor
7:returnUNKNOWN
```  
**Algorithm 2** The algorithm for the sufficient infeasibility test  
Note that both algorithms have quadratic time complexity with respect to the number of tasks, since they contain two nested loops that iterate and pairwise compare all the tasks of the input system in turn. The outer loop is specified by the \"for\" statement, and the two successive inner loops are specified by the universal and existential quantifiers. Our algorithms do not use backward reachability as such. Backward reachability is necessary for analyzing cases 1-14 of the bad state reachability. The combinatorial nature of backward reachability in our work disappears due to the condition of the number of tasks and processors \(n=m+1\): under this restriction, the backward paths from bad states are uniquely defined by inequalities on the values of the time parameters of the system's tasks. These inequalities are provided for each of the cases 1-14. These cases generalize into the inequalities of Theorem 1, which are used in Algorithms 1 and 2 and are computed in constant time.