Zur Software-Modell-Prüfung sowie zum Modell basiertem Testen als auch bei der Codegenerierung sind die Größe und Komplexität von Modellen entscheidende influssfaktoren. Ich untersuche Modelle in Form von symbolischen Kellersystemen, da diese in der Lage sind, Rekursion exakt nachzubilden. Für diese symbolischen Kellersysteme abe ich verschiedene Modellanalysen und Modellreduktionstechniken in einem Tool HalSPSI implementiert, welche die Software-Modell-Prüfung in meinen Tests für den Modellprüfer Moped erheblich beschleunigen bzw. die Modellprüfung erst ermöglichen oder sogar erübrigen. Letzteres ist z.B. dann der Fall, wenn durch statische Modellanalysen meines Tool HalSPSI die nicht Erreichbarkeit von Fehlerkonfigurationen nachgewiesen werden kann.