## 2 A Real-Time Kripke Model for a Real-Time System with a Dynamic NP-GFP Scheduler  
We consider that _a real-time system_ is a set of tasks \(T=(T_{1},...,T_{n})\), where each _task_\(T_{i}=(C_{i},D_{i},P_{i})\) has _an execution time_\(C_{i}\), _a relative deadline_\(D_{i}\), and _a minimum period_\(P_{i}\). Each task \(T_{i}\in T\) can generate a potentially infinite number of _jobs_, each of which requires \(C_{i}\) units of time. These jobs must be completed before \(D_{i}\) time units after the release time. Release time instants are separated by at least \(P_{i}\) time units. If there are no other restrictions on the jobs' releases, these tasks are referred to as _sporadic tasks_. In this paper, we study the base case of real-time systems in which all task parameters are integers and \(C_{i}<D_{i}\leq P_{i}\). All jobs are executed on _m processors_. If the number of processors is less then the number of tasks (\(m<n\)), we need _a scheduler_ to decide which job to run next. We assume that scheduling decisions are taken at discrete time instants, starting from 0. The _schedulability test problem_ is used to detect whether each job of each task in a real-time system is completed before its deadline. We say that _a real-time system is safe (schedulable)_ if the schedulability test gives a positive verdict for it. If the schedulability test gives a negative verdict for a real-time system, then this system is _unsafe (infeasible)_. In the rest of the paper, we fix the real-time system \(T\) described above. The scheduler must specify the conditions under which jobs are allowed to run on available processors. There are many types of schedulers that use different conditions and combinations of them. Some of the conditions are listed below. * Global Fixed Priority (GFP). The set of tasks is ordered: \(T_{1}\) has the highest priority, \(T_{n}\) has the lowest priority, and a job of a task with a lower number takes precedence over a job of a task with a higher number. * Early Deadline-First (EDF). The job with an earlier deadline has a higher priority. This priority is dynamic, because tasks (and their jobs) can have different priorities at different points in time. * Non-preemption. No job can be preempted by another job. * Preemption. A job may be interrupted by another job with a higher priority. * Dynamic scheduling. In a multiprocessor system, the jobs of each task can be executed on different processors (including the part of the job remaining after preemption). * Static scheduling. In a multiprocessor system, all the jobs of each task are executed on one predetermined processor. In our work, we focus on _a dynamic scheduler with global fixed priority for non-preemptive jobs (NP-GFP)_.  
Kripke models are used, in particular, in formal methods for model checking programs and systems [29]. In this paper, we apply them to formalize the schedulability test problem as a problem of the (un)reachability of missed deadline states. Recall the definition of a Kripke model. Let a set of atomic propositions \(Prop\) be given. _A Kripke model_ is a tuple \(M=(S,S_{0},R,L)\), where  
* \(S\) is a finite set of states of \(S\);
* \(S_{0}\subseteq S\) is a set of initial states;
* \(R\subseteq S\times S\) is a total transition relation between states;
* \(L:Prop\longrightarrow 2^{S}\) is an evaluation function that connects the states of the model and the truth of atomic propositions. Inspired by paper [4], we introduce the current values of the tasks' parameters as follows.