Auswertungsproblem (Prädikatenlogik)

Das Problem (Model Checking), zu einer gegebenen endlichen Struktur $\mathcal{A}$ und einer Formel $\phi$ zu entscheiden, ob $\mathcal{A}\models \phi$ gilt.
Komplexität:

• Datenkomplexität (Formel fest, Struktur variabel): Polynomiell in der Größe der Struktur ($|\mathcal{A}{|}^{|\phi |}$).
• Kombinierte Komplexität (beides variabel): PSPACE-vollständig.
• Zeit: Exponentiell in der Formellänge.
• Platz: Polynomiell in der Strukturgröße (bei Top-Down).