En este documento, desarrollamos una prueba exacta de planificabilidad y una prueba de infeasibilidad suficiente para la planificación de prioridades fijas en plataformas multiprocesador. Nos basamos en presentar sistemas en tiempo real como un modelo de Kripke para sistemas en tiempo real dinámicos con tareas esporádicas no preemptibles que se ejecutan en una plataforma multiprocesador y un planificador en línea que utiliza prioridades fijas globales. Este modelo incluye estados y transiciones entre estos estados, lo que nos permite justificar formalmente un algoritmo de tiempo polinómico para una prueba exacta de planificabilidad utilizando la idea de alcanzabilidad hacia atrás. Utilizando este algoritmo, realizamos la prueba exacta de planificabilidad para los sistemas en tiempo real mencionados anteriormente, en los que hay una tarea más que procesadores. La principal ventaja de este algoritmo es su complejidad polinómica, mientras que, en general, el problema de la prueba exacta de planificabilidad de sistemas en tiempo real en plataformas multiprocesador es NP-duro. La prueba de infactibilidad utiliza el mismo algoritmo para una relación arbitraria de tareas a procesadores, proporcionando una condición de infeasibilidad suficiente: si el sistema en tiempo real bajo prueba no es planificable en algunos casos, el algoritmo detecta esto. Realizamos un estudio experimental de nuestros algoritmos en los conjuntos de datos generados con diferentes valores de utilización y los comparamos con varias pruebas de planificabilidad de vanguardia. Los experimentos muestran que el rendimiento de nuestro algoritmo supera al de sus análogos mientras que su precisión es similar.