Aus der Kombination eines Pfadquantors mit einem temporalen Operator ergeben sich die acht dargestellten Ausdrücke, die jeweils auf Mengen oder auf durch boolesche Operatoren miteinander verknüpfte Mengen angewendet werden. Die Mengen beschreiben Mengen von Zuständen im Zustandsraum. Insofern befasst sich das Model-Checking mit der Erreichbarkeitsanalyse im Zustandsraum.