## 2 A Real-Time Kripke Model for a Real-Time System with a Dynamic NP-GFP Scheduler
\(t_{i}=(i,C_{i}-1,D_{i}-1,P_{i}-1,\mathbf{1},\mathbf{0})\), and \(go(i,s,t)\)--task \(i\) releases a job and the job is immediately started; 2. \(s_{i}=(i,C_{i}^{\prime},D_{i}^{\prime},P_{i}^{\prime},\mathbf{1},\mathbf{0})\), \(t_{i}=(i,C_{i}^{\prime},D_{i}^{\prime}-1,P_{i}^{\prime}-1,\mathbf{1},\mathbf{0})\) with \(s.D_{i}^{\prime}>0\), and \(\
eg go(i,s,t)\)--task \(i\) is waiting for permission to run its job; 3. \(s_{i}=(i,C_{i}^{\prime},D_{i}^{\prime},P_{i}^{\prime},\mathbf{1},\mathbf{0})\), \(t_{i}=(i,C_{i}^{\prime}-1,D_{i}^{\prime}-1,P_{i}^{\prime}-1,\mathbf{1},\mathbf{0})\) with \(0<s.C_{i}^{\prime}<C_{i}\), \(0<s.D_{i}^{\prime}<D_{i}\), \(s.C_{i}^{\prime}\leq s.D_{i}^{\prime}\), and \(go(i,s,t)\)--task \(i\) executes its job; 4. \(s_{i}=(i,0,D_{i}^{\prime},P_{i}^{\prime},\mathbf{1},\mathbf{0})\), or \(s_{i}=(i,C_{i},D_{i}^{\prime},P_{i}^{\prime},\mathbf{0},\mathbf{0})\), or \(s_{i}=(i,C_{i},D_{i},P_{i}^{\prime},\mathbf{0},\mathbf{0})\), and 1. if \(s.P_{i}^{\prime}=0\) 1. \(t_{i}=(i,C_{i}-1,D_{i}-1,P_{i}-1,\mathbf{1},\mathbf{0})\), and \(go(i,s,t)\)--task \(i\) completes its job normally, and it releases a new job, that starts immediately; 2. \(t_{i}=(i,C_{i},D_{i}-1,P_{i}-1,\mathbf{1},\mathbf{0})\), and \(\
eg go(i,s,t)\)--task \(i\) completes its job normally, and it is releases a new job that does not start immediately; 3. \(t_{i}=(i,C_{i},D_{i},P_{i},\mathbf{0},\mathbf{0})\)--task \(i\) completes its job normally, and it is does not release a new job; 4. if \(s.D_{i}^{\prime}=0\) and \(s.P_{i}^{\prime}>0\), then \(t_{i}=(i,C_{i},D_{i},P_{i}^{\prime}-1,\mathbf{0},\mathbf{0})\)--task \(i\) completes its job normally and waits for the next release; 5. \(s_{i}=(i,C_{i}^{\prime},C_{i}^{\prime}-1,P_{i}^{\prime},\mathbf{1},\mathbf{0})\) and \(t_{i}=(i,C_{i}^{\prime},C_{i}^{\prime}-1,P_{i}^{\prime},\mathbf{0},\mathbf{1})\)--a job of task \(i\). Task \(i\) will definitely miss the deadline, so task \(i\) goes to the \"bad\" state; 6. \(s_{i}=(i,C_{i}^{\prime},C_{i}^{\prime}-1,P_{i}^{\prime},\mathbf{0},\mathbf{1})\) and \(t_{i}=(i,C_{i}^{\prime},C_{i}^{\prime}-1,P_{i}^{\prime},\mathbf{0},\mathbf{1})\)--task \(i\) is in this \"bad\" state forever. * The evaluation function \(L:Prop\longrightarrow 2^{S^{T}}\) is standard: it assigns comparison propositions to those states in which they are true. In \(M^{T}\), _a path_\(\pi=s_{0},s_{1},\ldots\) is a sequence of states \(s_{i}\in S^{T}\) such that \(\forall i\geq 0\ (s_{i},s_{i+1})\in R^{T}\). An _initial path_ starts from the initial state. A path can be finite or infinite. We denote the finite path \(\pi=s_{0},\ldots,s_{n}\) as \(\pi(s_{0},s_{n})\). We refer to the state of the real-time system \(T\) in which \(D_{i}^{\prime}=C_{i}^{\prime}-1\) for some tasks \(i\) as _a bad state_, since there is no time left for task \(i\) to meet its deadline. Bad states in the Kripke model \(M^{T}\) are the set \(Bad_{\_States}=\{s\in S^{T}\mid\exists i\in[1..n]:\ s.bad_{i}=\mathbf{1}\}\). The proposition \(Bad=\bigvee_{i=0}^{n}(s.bad_{i}=\mathbf{1})\) describes this set of states. In these settings, the exact schedulability test for the real-time system \(T\) is to satisfiability check the LTL formula \(\Phi_{T}=\mathbf{G}(\
eg Bad)\) in the real-time Kripke model \(M^{T}\): the real-time system never reaches a state in which some tasks are in their bad state.