## 3 Backward Reachability-Based Schedulability Test
### Backward Reachability-Based Case Analysis
Each case can be described in terms of execution times and deadlines of these picture jobs. We say that _the case is safe_ if there are  
Figure 1: Backward reachability-based case analysis. some states in the picture case that are unreachable from the initial state of \(M^{T}\). Otherwise, _the case is unsafe_. The first eight pictures in Figure 1 show the cases where the red task \(i\) is the last task: \(i=n\). The last release of the red task before the bad state is in state \(r^{i}\) and none of the other tasks completes its job before \(b^{i}\). Between \(r^{i}\) and \(b^{i}\), the remaining execution time \(C^{\prime}_{i}\) is stable and equal to \(C_{i}\), but the time until deadline \(D^{\prime}_{i}\) decreases. **Case 1. **  
\(i>j\) and \(i>k\): \(re^{k}\preceq re^{i}\preceq r^{i}\preceq b^{i}\)--all jobs are released before the last release of the red job. This case is unsafe. Every task \(j<i\) can start its job before (or in) state \(r^{i}\), since there are \(m\) processors. Since none of them complete their job before \(b^{i}\), \(i\)-job goes into the bad state due to its late release. The condition for this picture is \(\forall j\
eq i:\ D_{i}<C_{j}\). **Case 2. **  
\(i>j\) and \(i>k\): \(re^{k}\preceq r^{j}_{p}\preceq r^{i}\preceq c^{j}_{p}\preceq re^{j}\preceq b^{i}\)--the green job is released after the last release of the red job. This case is safe. Task \(j>i\) releases and starts its job in state \(re^{j}\) between \(r^{i}\) and \(b^{i}\). To prevent \(i\)-job from running in the state \(prev(re^{j})\) that precedes state \(re^{j}\), task \(j\) must also run its job in that state. Therefore, \(prev(re^{j})_{j}=(j,1,1,\mathbf{0})\) due to the period restriction \(P_{j}=D_{j}\). Consider the state \(e^{j}_{p}\) which is in \(C_{j}\) transitions before \(re^{j}\). This state is the beginning of the previous execution of \(j\)-job. During the path \(\pi(e^{j}_{p},re^{j})\), \(D^{\prime}_{j}=C^{\prime}_{j}\) due to the definition of relation \(R^{T}\) (non-preemptively). In \(D_{j}-C_{j}\) transitions before \(e^{j}_{p}\), state \(r^{j}_{p}\) keeps the previous release of \(j\)-job. On the path \(\pi(r^{j}_{p},e^{j}_{p})\), \(C^{\prime}_{j}\) is stable: \(C^{\prime}_{j}=C_{j}\) due to \(D^{\prime}_{j}=C^{\prime}_{j}=C_{j}\) at state \(e^{j}_{p}\). Let the other \(m-1\) blue tasks start their jobs before \(r^{j}_{p}\) (other cases are in items 5-8 of this list). The last release of the red job may occur before or after \(e^{j}_{p}\). The latter case is described in items 3, 4, and 6-8 of this list. The release of the red task before \(e^{j}_{p}\) corresponds to the state where the green task \(j\) and the red task \(i\) do not execute their tasks, despite the fact that one processor is free (the others are busy with other tasks). This state is unreachable from the initial state due to the transition relation \(R^{T}\). The condition for this picture is \(\exists j\
eq i:\ (D_{i}\geq 2\cdot C_{j}\wedge(\forall k\
eq j\wedge k\
eq i: \ C_{k}\geq D_{j}+C_{j}))\). **Case 3. **  
\(i>j\) and \(i>k\): \((re^{k}\sim e^{i}_{p})\preceq r^{j}_{p}\preceq(e^{j}_{p}=f^{i}_{p})\preceq r ^{i}\preceq re^{j}\preceq b^{i}\)--as Case 2--but the last red release occurs after the previous green execution state, and the previous red completion occurs in the previous green execution state. This case is unsafe. Here, we consider the last red release \(r^{i}\) between the green release \(re^{i}\) and the state \(e^{j}_{p}\), after which the green job is executed. Certainly, the red task can start and then complete its job at \(e^{j}_{p}\) to prevent the green task from starting (the other \(m-1\) blue tasks start their job before \(r^{j}_{p}\)). Therefore, there is a sequence of releases from the initial state that leads to the bad state. The condition for this picture is \(\exists j\
eq i:\ (C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}>D_{j}-C_{j}\wedge( \forall k\
eq j\wedge k\
eq i:\ C_{k}\geq D_{j}+C_{j}))\). **Case 4.