## 2 A Real-Time Kripke Model for a Real-Time System with a Dynamic NP-GFP Scheduler
For every task \(i\in T\), let tuple \(s_{i}=(i,C_{i}^{\prime},D_{i}^{\prime},P_{i}^{\prime},rel_{i},bad_{i})\) be _a state of task \(i\)_, where  
* \(C_{i}^{\prime}\leq C_{i}\) is the time remaining until the job of this task is completed;
* \(D_{i}^{\prime}\leq D_{i}\) is the time until the deadline for completing a job of this task;
* \(P_{i}^{\prime}\leq P_{i}\) is the time until the next permissible release of a job of the task;
* \(rel_{i}\in\mathbb{B}\) is a Boolean variable that indicates a job release: it becomes _true_ when task \(i\) releases a job, and it becomes _false_ when the job is completed. * \(bad_{i}\in\mathbb{B}\) is a Boolean variable that indicates that a job is about to miss its deadline: it is _false_ if \(C_{i}^{\prime}\leq D_{i}^{\prime}\), and it becomes _true_ otherwise. For brevity, we refer to the Boolean constants _true_ and _false_ as **1** and **0**, respectively. For representing the processors' load, we introduce variable \(busy\): a number of jobs that are currently being executed (\(busy\leq m\)). Every global state \(s\) of our model is composed of tasks' states and the state for the processors' load. For global state \(s\), let \(s.C_{i}^{\prime}\), \(s.D_{i}^{\prime}\), \(s.P_{i}^{\prime}\), \(s.rel_{i}\), \(s.bad_{i}\), and \(s.busy\) be projections of \(s\) on its components for every \(i\in[1..n]\). In our Kripke model, for the dynamic non-preemptive GFP-scheduler, we use a predicate \(go(i,s,t)\) that is _true_ if task \(i\) starts to execute the job at the \(s\)-successor state \(t\), and \(false\) otherwise: \(go(i,s,t)\equiv(|Maj_{i}|+s.busy<m)\lor s.C_{i}^{\prime}<C_{i}\), where \(Maj_{i}=\{j\in[1..n]\mid j<i\wedge t.rel_{j}\wedge t.C_{j}^{\prime}=t.C_{j}\}\) is the set of released jobs with higher GFP priority that have not yet started execution. Note that when \(s.C_{i}^{\prime}<C_{i}\), the job of task \(i\) is executed and since in this case \(go(i,s,t)=true\), it continues to execute, i.e., it is not preempted. To estimate the change in the processor load \(busy\), we need to compute the amount of change \(cl(s,t)\). This number takes into account the number of tasks whose jobs have just been approved for execution by the scheduler and the number of tasks whose jobs have just completed. To compute \(cl(s,t)\), we introduce predicate \(fin(i,s)\) for just completed jobs that is _true_ if task \(i\) completes its job in state \(s\), and \(false\) otherwise: \(fin(i,s)\equiv s.C_{i}^{\prime}=0\wedge s.rel_{i}\)We treat \(go(i,s,t)\) and \(fin(i,s)\) as integer numbers (1 for \(true\) and 0 for \(false\)), so \(cl(s,t)=\sum_{i=1}^{n}(go(i,s,t)-fin(i,s))\). Let \(Prop\) be a set of propositions consisting of arithmetic comparisons of current values of tasks' parameters and propositions about a number of running jobs. We define the real-time system \(T\) with a dynamic non-preemptive GFP-scheduler as _the real-time Kripke model_\(M^{T}=(S^{T},s_{0}^{T},R^{T},L^{T})\), where  
* The finite set of states \(S^{T}=\prod_{i=1}^{n}(\{i\}\times[0..C_{i}]\times[0..D_{i}]\times[0..P_{i}] \times\mathbb{B}\times\mathbb{B})\times[0..m]\) for global state \(s\in S^{T}\), \(s_{i}=(i,C_{i}^{\prime},D_{i}^{\prime},P_{i}^{\prime},rel_{i},bad_{i})\) is a projection of \(s\) on task \(i\);
* The initial state \(s_{0}^{T}=\prod_{i=1}^{n}(\{i,C_{i},D_{i},P_{i},\mathbf{0},\mathbf{0}\})\times\{0\}\) represents the one-element set of initial states;
* The total transition relation \(R^{T}\in S^{T}\times S^{T}\) is defined by composing relations for \(i\)-task projections of global states \(s\) and \(t\) as follows. \((s,t)\in R^{T}\) if \(t.busy=s.busy+cl(s,t)\) and one of the following points holds: 1. \(s_{i}=(i,C_{i},D_{i},P_{i},\mathbf{0},\mathbf{0})\), and 1. \(t_{i}=(i,C_{i},D_{i},P_{i},\mathbf{0},\mathbf{0})\)--task \(i\) does nothing; 2. \(t_{i}=(i,C_{i},D_{i}-1,P_{i}-1,\mathbf{1},\mathbf{0})\), and \(\
eg go(i,s,t)\)--task \(i\) releases a job and the job is not started; 3.